src/HOL/UNITY/Token.thy
changeset 4776 1f9362e769c1
child 5232 e5a7cdd07ea5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Token.thy	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,71 @@
     1.4 +(*  Title:      HOL/UNITY/Token
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +The Token Ring.
    1.10 +
    1.11 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
    1.12 +*)
    1.13 +
    1.14 +
    1.15 +Token = WFair +
    1.16 +
    1.17 +(*process states*)
    1.18 +datatype pstate = Hungry | Eating | Thinking | Pnum nat
    1.19 +
    1.20 +types state = nat => pstate
    1.21 +
    1.22 +consts
    1.23 +  N :: nat	(*number of nodes in the ring*)
    1.24 +
    1.25 +constdefs
    1.26 +  nodeOrder :: "nat => (nat*nat)set"
    1.27 +    "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    1.28 +                    (lessThan N Times lessThan N)"
    1.29 +
    1.30 +  next      :: nat => nat
    1.31 +    "next i == (Suc i) mod N"
    1.32 +
    1.33 +  WellTyped :: state set
    1.34 +    "WellTyped == {s. ALL i j. s (Suc i) ~= Pnum j}"
    1.35 +
    1.36 +  Token :: state => nat
    1.37 +    "Token s == case s 0 of 
    1.38 +                    Hungry => 0
    1.39 +                  | Eating => 0
    1.40 +                  | Thinking => 0
    1.41 +                  | Pnum i => i"
    1.42 +
    1.43 +  HasTok :: nat => state set
    1.44 +    "HasTok i == Token -`` {i}"
    1.45 +
    1.46 +  H :: nat => state set
    1.47 +    "H i == {s. s (Suc i) = Hungry}"
    1.48 +
    1.49 +  E :: nat => state set
    1.50 +    "E i == {s. s (Suc i) = Eating}"
    1.51 +
    1.52 +  T :: nat => state set
    1.53 +    "T i == {s. s (Suc i) = Thinking}"
    1.54 +
    1.55 +rules
    1.56 +  N_positive "0<N"
    1.57 +
    1.58 +  stable_WT  "stable Acts WellTyped"
    1.59 +
    1.60 +  skip "id: Acts"
    1.61 +
    1.62 +  TR2  "constrains Acts (T i) (T i Un H i)"
    1.63 +
    1.64 +  TR3  "constrains Acts (H i) (H i Un E i)"
    1.65 +
    1.66 +  TR4  "constrains Acts (H i - HasTok i) (H i)"
    1.67 +
    1.68 +  TR5  "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"
    1.69 +
    1.70 +  TR6  "leadsTo Acts (H i Int HasTok i) (E i)"
    1.71 +
    1.72 +  TR7  "leadsTo Acts (HasTok i) (HasTok (next i))"
    1.73 +
    1.74 +end