16 translations |
16 translations |
17 "3" == "Suc 2" |
17 "3" == "Suc 2" |
18 "4" == "Suc 3" |
18 "4" == "Suc 3" |
19 |
19 |
20 |
20 |
21 (*program variables*) |
21 record state = |
22 datatype pvar = PP | MM | NN | UU | VV |
22 PP :: bool |
23 |
23 MM :: nat |
24 (*No booleans; instead True=1 and False=0*) |
24 NN :: nat |
25 types state = pvar => nat |
25 UU :: bool |
|
26 VV :: bool |
26 |
27 |
27 constdefs |
28 constdefs |
28 cmd0 :: "[pvar,pvar] => (state*state) set" |
29 cmd0U :: "(state*state) set" |
29 "cmd0 u m == {(s,s'). s' = s(u:=1,m:=1) & s m = 0}" |
30 "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=1|) & MM s = 0}" |
30 |
31 |
31 cmd1u :: "(state*state) set" |
32 cmd1U :: "(state*state) set" |
32 "cmd1u == {(s,s'). s' = s(PP:= s VV,MM:=2) & s MM = 1}" |
33 "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=2|) & MM s = 1}" |
33 |
34 |
34 cmd1v :: "(state*state) set" |
35 cmd2U :: "(state*state) set" |
35 "cmd1v == {(s,s'). s' = s(PP:= 1 - s UU,NN:=2) & s NN = 1}" |
36 "cmd2U == {(s,s'). s' = s (|MM:=3|) & ~ PP s & MM s = 2}" |
36 |
37 |
37 (*Put pv=0 for u's program and pv=1 for v's program*) |
38 cmd3U :: "(state*state) set" |
38 cmd2 :: "[nat,pvar] => (state*state) set" |
39 "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=4|) & MM s = 3}" |
39 "cmd2 pv m == {(s,s'). s' = s(m:=3) & s PP = pv & s m = 2}" |
|
40 |
40 |
41 cmd3 :: "[pvar,pvar] => (state*state) set" |
41 cmd4U :: "(state*state) set" |
42 "cmd3 u m == {(s,s'). s' = s(u:=0,m:=4) & s m = 3}" |
42 "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=0|) & MM s = 4}" |
43 |
43 |
44 (*Put pv=1 for u's program and pv=0 for v's program*) |
44 cmd0V :: "(state*state) set" |
45 cmd4 :: "[nat,pvar] => (state*state) set" |
45 "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=1|) & NN s = 0}" |
46 "cmd4 pv m == {(s,s'). s' = s(PP:=pv,m:=0) & s m = 4}" |
46 |
|
47 cmd1V :: "(state*state) set" |
|
48 "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=2|) & NN s = 1}" |
|
49 |
|
50 cmd2V :: "(state*state) set" |
|
51 "cmd2V == {(s,s'). s' = s (|NN:=3|) & PP s & NN s = 2}" |
|
52 |
|
53 cmd3V :: "(state*state) set" |
|
54 "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=4|) & NN s = 3}" |
|
55 |
|
56 cmd4V :: "(state*state) set" |
|
57 "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=0|) & NN s = 4}" |
47 |
58 |
48 mutex :: "(state*state) set set" |
59 mutex :: "(state*state) set set" |
49 "mutex == {id, |
60 "mutex == {id, |
50 cmd0 UU MM, cmd0 VV NN, |
61 cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, |
51 cmd1u, cmd1v, |
62 cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}" |
52 cmd2 0 MM, cmd2 1 NN, |
63 |
53 cmd3 UU MM, cmd3 VV NN, |
64 (** The correct invariants **) |
54 cmd4 1 MM, cmd4 0 NN}" |
65 |
|
66 invariantU :: "state set" |
|
67 "invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) & |
|
68 (MM s = 3 --> ~ PP s)}" |
|
69 |
|
70 invariantV :: "state set" |
|
71 "invariantV == {s. (VV s = (1 <= NN s & NN s <= 3)) & |
|
72 (NN s = 3 --> PP s)}" |
|
73 |
|
74 (** The faulty invariant (for U alone) **) |
|
75 |
|
76 bad_invariantU :: "state set" |
|
77 "bad_invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) & |
|
78 (3 <= MM s & MM s <= 4 --> ~ PP s)}" |
55 |
79 |
56 MInit :: "state set" |
80 MInit :: "state set" |
57 "MInit == {s. s PP < 2 & s UU = 0 & s VV = 0 & s MM = 0 & s NN = 0}" |
81 "MInit == {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0}" |
58 |
|
59 boolVars :: "state set" |
|
60 "boolVars == {s. s PP<2 & s UU < 2 & s VV < 2}" |
|
61 |
|
62 (*Put pv=0 for u's program and pv=1 for v's program*) |
|
63 invariant :: "[nat,pvar,pvar] => state set" |
|
64 "invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) & |
|
65 (s m = 3 --> s PP = pv)}" |
|
66 |
|
67 bad_invariant :: "[nat,pvar,pvar] => state set" |
|
68 "bad_invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) & |
|
69 (3 <= s m & s m <= 4 --> s PP = pv)}" |
|
70 |
|
71 |
|
72 |
|
73 |
82 |
74 end |
83 end |