author | paulson |
Thu, 13 Aug 1998 18:06:40 +0200 | |
changeset 5313 | 1861a564d7e2 |
parent 5277 | e4297d03e5d2 |
child 5420 | b48ab3281944 |
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 |
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 |
|
5232 | 33 |
"HasTok i == {s. token s = i}" |
4776 | 34 |
|
35 |
H :: nat => state set |
|
5232 | 36 |
"H i == {s. proc s i = Hungry}" |
4776 | 37 |
|
38 |
E :: nat => state set |
|
5232 | 39 |
"E i == {s. proc s i = Eating}" |
4776 | 40 |
|
41 |
T :: nat => state set |
|
5232 | 42 |
"T i == {s. proc s i = Thinking}" |
4776 | 43 |
|
44 |
rules |
|
45 |
N_positive "0<N" |
|
46 |
||
5253 | 47 |
skip "id: acts" |
4776 | 48 |
|
5253 | 49 |
TR2 "constrains acts (T i) (T i Un H i)" |
4776 | 50 |
|
5253 | 51 |
TR3 "constrains acts (H i) (H i Un E i)" |
4776 | 52 |
|
5253 | 53 |
TR4 "constrains acts (H i - HasTok i) (H i)" |
4776 | 54 |
|
5253 | 55 |
TR5 "constrains acts (HasTok i) (HasTok i Un Compl(E i))" |
4776 | 56 |
|
5253 | 57 |
TR6 "leadsTo acts (H i Int HasTok i) (E i)" |
4776 | 58 |
|
5253 | 59 |
TR7 "leadsTo acts (HasTok i) (HasTok (next i))" |
4776 | 60 |
|
61 |
end |