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 |
|
|
12 |
Token = WFair +
|
|
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 |
|
|
47 |
skip "id: Acts"
|
|
48 |
|
|
49 |
TR2 "constrains Acts (T i) (T i Un H i)"
|
|
50 |
|
|
51 |
TR3 "constrains Acts (H i) (H i Un E i)"
|
|
52 |
|
|
53 |
TR4 "constrains Acts (H i - HasTok i) (H i)"
|
|
54 |
|
|
55 |
TR5 "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"
|
|
56 |
|
|
57 |
TR6 "leadsTo Acts (H i Int HasTok i) (E i)"
|
|
58 |
|
|
59 |
TR7 "leadsTo Acts (HasTok i) (HasTok (next i))"
|
|
60 |
|
|
61 |
end
|