6 Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra |
6 Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra |
7 *) |
7 *) |
8 |
8 |
9 Mutex = SubstAx + |
9 Mutex = SubstAx + |
10 |
10 |
11 (*WE NEED A GENERAL TREATMENT OF NUMBERS!!*) |
|
12 syntax |
|
13 "3" :: nat ("3") |
|
14 "4" :: nat ("4") |
|
15 |
|
16 translations |
|
17 "3" == "Suc 2" |
|
18 "4" == "Suc 3" |
|
19 |
|
20 |
|
21 record state = |
11 record state = |
22 PP :: bool |
12 PP :: bool |
23 MM :: nat |
13 MM :: int |
24 NN :: nat |
14 NN :: int |
25 UU :: bool |
15 UU :: bool |
26 VV :: bool |
16 VV :: bool |
27 |
17 |
28 constdefs |
18 constdefs |
29 |
19 |
30 (** The program for process U **) |
20 (** The program for process U **) |
31 |
21 |
32 cmd0U :: "(state*state) set" |
22 cmd0U :: "(state*state) set" |
33 "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=1|) & MM s = 0}" |
23 "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=#1|) & MM s = #0}" |
34 |
24 |
35 cmd1U :: "(state*state) set" |
25 cmd1U :: "(state*state) set" |
36 "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=2|) & MM s = 1}" |
26 "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=#2|) & MM s = #1}" |
37 |
27 |
38 cmd2U :: "(state*state) set" |
28 cmd2U :: "(state*state) set" |
39 "cmd2U == {(s,s'). s' = s (|MM:=3|) & ~ PP s & MM s = 2}" |
29 "cmd2U == {(s,s'). s' = s (|MM:=#3|) & ~ PP s & MM s = #2}" |
40 |
30 |
41 cmd3U :: "(state*state) set" |
31 cmd3U :: "(state*state) set" |
42 "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=4|) & MM s = 3}" |
32 "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=#4|) & MM s = #3}" |
43 |
33 |
44 cmd4U :: "(state*state) set" |
34 cmd4U :: "(state*state) set" |
45 "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=0|) & MM s = 4}" |
35 "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=#0|) & MM s = #4}" |
46 |
36 |
47 (** The program for process V **) |
37 (** The program for process V **) |
48 |
38 |
49 cmd0V :: "(state*state) set" |
39 cmd0V :: "(state*state) set" |
50 "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=1|) & NN s = 0}" |
40 "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=#1|) & NN s = #0}" |
51 |
41 |
52 cmd1V :: "(state*state) set" |
42 cmd1V :: "(state*state) set" |
53 "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=2|) & NN s = 1}" |
43 "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=#2|) & NN s = #1}" |
54 |
44 |
55 cmd2V :: "(state*state) set" |
45 cmd2V :: "(state*state) set" |
56 "cmd2V == {(s,s'). s' = s (|NN:=3|) & PP s & NN s = 2}" |
46 "cmd2V == {(s,s'). s' = s (|NN:=#3|) & PP s & NN s = #2}" |
57 |
47 |
58 cmd3V :: "(state*state) set" |
48 cmd3V :: "(state*state) set" |
59 "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=4|) & NN s = 3}" |
49 "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=#4|) & NN s = #3}" |
60 |
50 |
61 cmd4V :: "(state*state) set" |
51 cmd4V :: "(state*state) set" |
62 "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=0|) & NN s = 4}" |
52 "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=#0|) & NN s = #4}" |
63 |
53 |
64 Mprg :: state program |
54 Mprg :: state program |
65 "Mprg == (|Init = {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0}, |
55 "Mprg == mk_program ({s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0}, |
66 Acts0 = {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, |
56 {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, |
67 cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}|)" |
57 cmd0V, cmd1V, cmd2V, cmd3V, cmd4V})" |
68 |
58 |
69 |
59 |
70 (** The correct invariants **) |
60 (** The correct invariants **) |
71 |
61 |
72 invariantU :: "state set" |
62 invariantU :: "state set" |
73 "invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) & |
63 "invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) & |
74 (MM s = 3 --> ~ PP s)}" |
64 (MM s = #3 --> ~ PP s)}" |
75 |
65 |
76 invariantV :: "state set" |
66 invariantV :: "state set" |
77 "invariantV == {s. (VV s = (1 <= NN s & NN s <= 3)) & |
67 "invariantV == {s. (VV s = (#1 <= NN s & NN s <= #3)) & |
78 (NN s = 3 --> PP s)}" |
68 (NN s = #3 --> PP s)}" |
79 |
69 |
80 (** The faulty invariant (for U alone) **) |
70 (** The faulty invariant (for U alone) **) |
81 |
71 |
82 bad_invariantU :: "state set" |
72 bad_invariantU :: "state set" |
83 "bad_invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) & |
73 "bad_invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) & |
84 (3 <= MM s & MM s <= 4 --> ~ PP s)}" |
74 (#3 <= MM s & MM s <= #4 --> ~ PP s)}" |
85 |
75 |
86 end |
76 end |