7 *) |
7 *) |
8 |
8 |
9 Mutex = SubstAx + |
9 Mutex = SubstAx + |
10 |
10 |
11 record state = |
11 record state = |
12 PP :: bool |
12 p :: bool |
13 MM :: int |
13 m :: int |
14 NN :: int |
14 n :: int |
15 UU :: bool |
15 u :: bool |
16 VV :: bool |
16 v :: bool |
|
17 |
|
18 types command = "(state*state) set" |
17 |
19 |
18 constdefs |
20 constdefs |
19 |
21 |
20 (** The program for process U **) |
22 (** The program for process U **) |
21 |
23 |
22 cmd0U :: "(state*state) set" |
24 U0 :: command |
23 "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=#1|) & MM s = #0}" |
25 "U0 == {(s,s'). s' = s (|u:=True, m:=#1|) & m s = #0}" |
24 |
26 |
25 cmd1U :: "(state*state) set" |
27 U1 :: command |
26 "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=#2|) & MM s = #1}" |
28 "U1 == {(s,s'). s' = s (|p:= v s, m:=#2|) & m s = #1}" |
27 |
29 |
28 cmd2U :: "(state*state) set" |
30 U2 :: command |
29 "cmd2U == {(s,s'). s' = s (|MM:=#3|) & ~ PP s & MM s = #2}" |
31 "U2 == {(s,s'). s' = s (|m:=#3|) & ~ p s & m s = #2}" |
30 |
32 |
31 cmd3U :: "(state*state) set" |
33 U3 :: command |
32 "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=#4|) & MM s = #3}" |
34 "U3 == {(s,s'). s' = s (|u:=False, m:=#4|) & m s = #3}" |
33 |
35 |
34 cmd4U :: "(state*state) set" |
36 U4 :: command |
35 "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=#0|) & MM s = #4}" |
37 "U4 == {(s,s'). s' = s (|p:=True, m:=#0|) & m s = #4}" |
36 |
38 |
37 (** The program for process V **) |
39 (** The program for process V **) |
38 |
40 |
39 cmd0V :: "(state*state) set" |
41 V0 :: command |
40 "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=#1|) & NN s = #0}" |
42 "V0 == {(s,s'). s' = s (|v:=True, n:=#1|) & n s = #0}" |
41 |
43 |
42 cmd1V :: "(state*state) set" |
44 V1 :: command |
43 "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=#2|) & NN s = #1}" |
45 "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=#2|) & n s = #1}" |
44 |
46 |
45 cmd2V :: "(state*state) set" |
47 V2 :: command |
46 "cmd2V == {(s,s'). s' = s (|NN:=#3|) & PP s & NN s = #2}" |
48 "V2 == {(s,s'). s' = s (|n:=#3|) & p s & n s = #2}" |
47 |
49 |
48 cmd3V :: "(state*state) set" |
50 V3 :: command |
49 "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=#4|) & NN s = #3}" |
51 "V3 == {(s,s'). s' = s (|v:=False, n:=#4|) & n s = #3}" |
50 |
52 |
51 cmd4V :: "(state*state) set" |
53 V4 :: command |
52 "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=#0|) & NN s = #4}" |
54 "V4 == {(s,s'). s' = s (|p:=False, n:=#0|) & n s = #4}" |
53 |
55 |
54 Mprg :: state program |
56 Mutex :: state program |
55 "Mprg == mk_program ({s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0}, |
57 "Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0}, |
56 {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, |
58 {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4})" |
57 cmd0V, cmd1V, cmd2V, cmd3V, cmd4V})" |
|
58 |
59 |
59 |
60 |
60 (** The correct invariants **) |
61 (** The correct invariants **) |
61 |
62 |
62 invariantU :: "state set" |
63 invariantU :: state set |
63 "invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) & |
64 "invariantU == {s. (u s = (#1 <= m s & m s <= #3)) & |
64 (MM s = #3 --> ~ PP s)}" |
65 (m s = #3 --> ~ p s)}" |
65 |
66 |
66 invariantV :: "state set" |
67 invariantV :: state set |
67 "invariantV == {s. (VV s = (#1 <= NN s & NN s <= #3)) & |
68 "invariantV == {s. (v s = (#1 <= n s & n s <= #3)) & |
68 (NN s = #3 --> PP s)}" |
69 (n s = #3 --> p s)}" |
69 |
70 |
70 (** The faulty invariant (for U alone) **) |
71 (** The faulty invariant (for U alone) **) |
71 |
72 |
72 bad_invariantU :: "state set" |
73 bad_invariantU :: state set |
73 "bad_invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) & |
74 "bad_invariantU == {s. (u s = (#1 <= m s & m s <= #3)) & |
74 (#3 <= MM s & MM s <= #4 --> ~ PP s)}" |
75 (#3 <= m s & m s <= #4 --> ~ p s)}" |
75 |
76 |
76 end |
77 end |