author | paulson |
Thu, 15 Oct 1998 11:35:07 +0200 | |
changeset 5648 | fe887910e32e |
parent 5608 | a82a038a3e7a |
child 5782 | 7559f116cb10 |
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 |
||
5648 | 46 |
TR2 "!!i. F : constrains (T i) (T i Un H i)" |
5420 | 47 |
|
5648 | 48 |
TR3 "!!i. F : constrains (H i) (H i Un E i)" |
4776 | 49 |
|
5648 | 50 |
TR4 "!!i. F : constrains (H i - HasTok i) (H i)" |
5420 | 51 |
|
5648 | 52 |
TR5 "!!i. F : constrains (HasTok i) (HasTok i Un Compl(E i))" |
5420 | 53 |
|
5648 | 54 |
TR6 "!!i. F : leadsTo (H i Int HasTok i) (E i)" |
4776 | 55 |
|
5648 | 56 |
TR7 "!!i. 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 |