author | paulson |
Wed, 18 Nov 1998 15:10:46 +0100 | |
changeset 5931 | 325300576da7 |
parent 5782 | 7559f116cb10 |
child 6536 | 281d44905cab |
permissions | -rw-r--r-- |
4776 | 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 |
||
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
12 |
Token = WFair + |
4776 | 13 |
|
14 |
(*process states*) |
|
5232 | 15 |
datatype pstate = Hungry | Eating | Thinking |
4776 | 16 |
|
5232 | 17 |
record state = |
18 |
token :: nat |
|
19 |
proc :: nat => pstate |
|
4776 | 20 |
|
21 |
||
22 |
constdefs |
|
23 |
HasTok :: nat => state set |
|
5232 | 24 |
"HasTok i == {s. token s = i}" |
4776 | 25 |
|
26 |
H :: nat => state set |
|
5232 | 27 |
"H i == {s. proc s i = Hungry}" |
4776 | 28 |
|
29 |
E :: nat => state set |
|
5232 | 30 |
"E i == {s. proc s i = Eating}" |
4776 | 31 |
|
32 |
T :: nat => state set |
|
5232 | 33 |
"T i == {s. proc s i = Thinking}" |
4776 | 34 |
|
35 |
||
5420 | 36 |
locale Token = |
37 |
fixes |
|
38 |
N :: nat (*number of nodes in the ring*) |
|
5648 | 39 |
F :: state program |
5420 | 40 |
nodeOrder :: "nat => (nat*nat)set" |
41 |
next :: nat => nat |
|
4776 | 42 |
|
5420 | 43 |
assumes |
44 |
N_positive "0<N" |
|
45 |
||
5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
46 |
TR2 "F : constrains (T i) (T i Un H i)" |
5420 | 47 |
|
5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
48 |
TR3 "F : constrains (H i) (H i Un E i)" |
4776 | 49 |
|
5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
50 |
TR4 "F : constrains (H i - HasTok i) (H i)" |
5420 | 51 |
|
5931 | 52 |
TR5 "F : constrains (HasTok i) (HasTok i Un -(E i))" |
5420 | 53 |
|
5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
54 |
TR6 "F : leadsTo (H i Int HasTok i) (E i)" |
4776 | 55 |
|
5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
56 |
TR7 "F : leadsTo (HasTok i) (HasTok (next i))" |
4776 | 57 |
|
5420 | 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)" |
|
4776 | 62 |
|
5420 | 63 |
next_def |
64 |
"next i == (Suc i) mod N" |
|
4776 | 65 |
|
66 |
end |