src/HOL/UNITY/Token.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Token.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,71 @@
+(*  Title:      HOL/UNITY/Token
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+The Token Ring.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
+*)
+
+
+Token = WFair +
+
+(*process states*)
+datatype pstate = Hungry | Eating | Thinking | Pnum nat
+
+types state = nat => pstate
+
+consts
+  N :: nat	(*number of nodes in the ring*)
+
+constdefs
+  nodeOrder :: "nat => (nat*nat)set"
+    "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
+                    (lessThan N Times lessThan N)"
+
+  next      :: nat => nat
+    "next i == (Suc i) mod N"
+
+  WellTyped :: state set
+    "WellTyped == {s. ALL i j. s (Suc i) ~= Pnum j}"
+
+  Token :: state => nat
+    "Token s == case s 0 of 
+                    Hungry => 0
+                  | Eating => 0
+                  | Thinking => 0
+                  | Pnum i => i"
+
+  HasTok :: nat => state set
+    "HasTok i == Token -`` {i}"
+
+  H :: nat => state set
+    "H i == {s. s (Suc i) = Hungry}"
+
+  E :: nat => state set
+    "E i == {s. s (Suc i) = Eating}"
+
+  T :: nat => state set
+    "T i == {s. s (Suc i) = Thinking}"
+
+rules
+  N_positive "0<N"
+
+  stable_WT  "stable Acts WellTyped"
+
+  skip "id: Acts"
+
+  TR2  "constrains Acts (T i) (T i Un H i)"
+
+  TR3  "constrains Acts (H i) (H i Un E i)"
+
+  TR4  "constrains Acts (H i - HasTok i) (H i)"
+
+  TR5  "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"
+
+  TR6  "leadsTo Acts (H i Int HasTok i) (E i)"
+
+  TR7  "leadsTo Acts (HasTok i) (HasTok (next i))"
+
+end