src/HOL/UNITY/Token.thy
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5232 e5a7cdd07ea5
permissions -rw-r--r--
New UNITY theory
     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 | Pnum nat
    16 
    17 types state = nat => pstate
    18 
    19 consts
    20   N :: nat	(*number of nodes in the ring*)
    21 
    22 constdefs
    23   nodeOrder :: "nat => (nat*nat)set"
    24     "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    25                     (lessThan N Times lessThan N)"
    26 
    27   next      :: nat => nat
    28     "next i == (Suc i) mod N"
    29 
    30   WellTyped :: state set
    31     "WellTyped == {s. ALL i j. s (Suc i) ~= Pnum j}"
    32 
    33   Token :: state => nat
    34     "Token s == case s 0 of 
    35                     Hungry => 0
    36                   | Eating => 0
    37                   | Thinking => 0
    38                   | Pnum i => i"
    39 
    40   HasTok :: nat => state set
    41     "HasTok i == Token -`` {i}"
    42 
    43   H :: nat => state set
    44     "H i == {s. s (Suc i) = Hungry}"
    45 
    46   E :: nat => state set
    47     "E i == {s. s (Suc i) = Eating}"
    48 
    49   T :: nat => state set
    50     "T i == {s. s (Suc i) = Thinking}"
    51 
    52 rules
    53   N_positive "0<N"
    54 
    55   stable_WT  "stable Acts WellTyped"
    56 
    57   skip "id: Acts"
    58 
    59   TR2  "constrains Acts (T i) (T i Un H i)"
    60 
    61   TR3  "constrains Acts (H i) (H i Un E i)"
    62 
    63   TR4  "constrains Acts (H i - HasTok i) (H i)"
    64 
    65   TR5  "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"
    66 
    67   TR6  "leadsTo Acts (H i Int HasTok i) (E i)"
    68 
    69   TR7  "leadsTo Acts (HasTok i) (HasTok (next i))"
    70 
    71 end