src/HOL/UNITY/Token.thy
author paulson
Thu Aug 06 15:47:26 1998 +0200 (1998-08-06)
changeset 5277 e4297d03e5d2
parent 5253 82a5ca6290aa
child 5420 b48ab3281944
permissions -rw-r--r--
A higher-level treatment of LeadsTo, minimizing use of "reachable"
     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 consts
    22   N :: nat	(*number of nodes in the ring*)
    23 
    24 constdefs
    25   nodeOrder :: "nat => (nat*nat)set"
    26     "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    27                     (lessThan N Times lessThan N)"
    28 
    29   next      :: nat => nat
    30     "next i == (Suc i) mod N"
    31 
    32   HasTok :: nat => state set
    33     "HasTok i == {s. token s = i}"
    34 
    35   H :: nat => state set
    36     "H i == {s. proc s i = Hungry}"
    37 
    38   E :: nat => state set
    39     "E i == {s. proc s i = Eating}"
    40 
    41   T :: nat => state set
    42     "T i == {s. proc s i = Thinking}"
    43 
    44 rules
    45   N_positive "0<N"
    46 
    47   skip "id: acts"
    48 
    49   TR2  "constrains acts (T i) (T i Un H i)"
    50 
    51   TR3  "constrains acts (H i) (H i Un E i)"
    52 
    53   TR4  "constrains acts (H i - HasTok i) (H i)"
    54 
    55   TR5  "constrains acts (HasTok i) (HasTok i Un Compl(E i))"
    56 
    57   TR6  "leadsTo acts (H i Int HasTok i) (E i)"
    58 
    59   TR7  "leadsTo acts (HasTok i) (HasTok (next i))"
    60 
    61 end