equal
deleted
inserted
replaced
16 |
16 |
17 record state = |
17 record state = |
18 token :: nat |
18 token :: nat |
19 proc :: nat => pstate |
19 proc :: nat => pstate |
20 |
20 |
21 consts |
|
22 N :: nat (*number of nodes in the ring*) |
|
23 |
21 |
24 constdefs |
22 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 |
23 HasTok :: nat => state set |
33 "HasTok i == {s. token s = i}" |
24 "HasTok i == {s. token s = i}" |
34 |
25 |
35 H :: nat => state set |
26 H :: nat => state set |
36 "H i == {s. proc s i = Hungry}" |
27 "H i == {s. proc s i = Hungry}" |
39 "E i == {s. proc s i = Eating}" |
30 "E i == {s. proc s i = Eating}" |
40 |
31 |
41 T :: nat => state set |
32 T :: nat => state set |
42 "T i == {s. proc s i = Thinking}" |
33 "T i == {s. proc s i = Thinking}" |
43 |
34 |
44 rules |
|
45 N_positive "0<N" |
|
46 |
35 |
47 skip "id: acts" |
36 locale Token = |
|
37 fixes |
|
38 N :: nat (*number of nodes in the ring*) |
|
39 acts :: "(state*state)set set" |
|
40 nodeOrder :: "nat => (nat*nat)set" |
|
41 next :: nat => nat |
48 |
42 |
49 TR2 "constrains acts (T i) (T i Un H i)" |
43 assumes |
|
44 N_positive "0<N" |
50 |
45 |
51 TR3 "constrains acts (H i) (H i Un E i)" |
46 skip "id: acts" |
52 |
47 |
53 TR4 "constrains acts (H i - HasTok i) (H i)" |
48 TR2 "!!i. constrains acts (T i) (T i Un H i)" |
54 |
49 |
55 TR5 "constrains acts (HasTok i) (HasTok i Un Compl(E i))" |
50 TR3 "!!i. constrains acts (H i) (H i Un E i)" |
56 |
51 |
57 TR6 "leadsTo acts (H i Int HasTok i) (E i)" |
52 TR4 "!!i. constrains acts (H i - HasTok i) (H i)" |
58 |
53 |
59 TR7 "leadsTo acts (HasTok i) (HasTok (next i))" |
54 TR5 "!!i. constrains acts (HasTok i) (HasTok i Un Compl(E i))" |
|
55 |
|
56 TR6 "!!i. leadsTo acts (H i Int HasTok i) (E i)" |
|
57 |
|
58 TR7 "!!i. leadsTo acts (HasTok i) (HasTok (next i))" |
|
59 |
|
60 defines |
|
61 nodeOrder_def |
|
62 "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int |
|
63 (lessThan N Times lessThan N)" |
|
64 |
|
65 next_def |
|
66 "next i == (Suc i) mod N" |
60 |
67 |
61 end |
68 end |