src/HOL/UNITY/Token.thy
author paulson
Thu Oct 15 11:35:07 1998 +0200 (1998-10-15)
changeset 5648 fe887910e32e
parent 5608 a82a038a3e7a
child 5782 7559f116cb10
permissions -rw-r--r--
specifications as sets of programs
     1 (*  Title:      HOL/UNITY/Token
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 The Token Ring.
     7 
     8 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
     9 *)
    10 
    11 
    12 Token = WFair + 
    13 
    14 (*process states*)
    15 datatype pstate = Hungry | Eating | Thinking
    16 
    17 record state =
    18   token :: nat
    19   proc  :: nat => pstate
    20 
    21 
    22 constdefs
    23   HasTok :: nat => state set
    24     "HasTok i == {s. token s = i}"
    25 
    26   H :: nat => state set
    27     "H i == {s. proc s i = Hungry}"
    28 
    29   E :: nat => state set
    30     "E i == {s. proc s i = Eating}"
    31 
    32   T :: nat => state set
    33     "T i == {s. proc s i = Thinking}"
    34 
    35 
    36 locale Token =
    37   fixes
    38     N         :: nat	 (*number of nodes in the ring*)
    39     F         :: state program
    40     nodeOrder :: "nat => (nat*nat)set"
    41     next      :: nat => nat
    42 
    43   assumes
    44     N_positive "0<N"
    45 
    46     TR2  "!!i. F : constrains (T i) (T i Un H i)"
    47 
    48     TR3  "!!i. F : constrains (H i) (H i Un E i)"
    49 
    50     TR4  "!!i. F : constrains (H i - HasTok i) (H i)"
    51 
    52     TR5  "!!i. F : constrains (HasTok i) (HasTok i Un Compl(E i))"
    53 
    54     TR6  "!!i. F : leadsTo (H i Int HasTok i) (E i)"
    55 
    56     TR7  "!!i. F : leadsTo (HasTok i) (HasTok (next i))"
    57 
    58   defines
    59     nodeOrder_def
    60       "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    61 		      (lessThan N Times lessThan N)"
    62 
    63     next_def
    64       "next i == (Suc i) mod N"
    65 
    66 end