14 u :: bool |
14 u :: bool |
15 v :: bool |
15 v :: bool |
16 |
16 |
17 types command = "(state*state) set" |
17 types command = "(state*state) set" |
18 |
18 |
19 constdefs |
19 |
20 |
|
21 (** The program for process U **) |
20 (** The program for process U **) |
22 |
21 |
23 U0 :: command |
22 definition U0 :: command |
24 "U0 == {(s,s'). s' = s (|u:=True, m:=1|) & m s = 0}" |
23 where "U0 = {(s,s'). s' = s (|u:=True, m:=1|) & m s = 0}" |
25 |
24 |
26 U1 :: command |
25 definition U1 :: command |
27 "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = 1}" |
26 where "U1 = {(s,s'). s' = s (|p:= v s, m:=2|) & m s = 1}" |
28 |
27 |
29 U2 :: command |
28 definition U2 :: command |
30 "U2 == {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}" |
29 where "U2 = {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}" |
31 |
30 |
32 U3 :: command |
31 definition U3 :: command |
33 "U3 == {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}" |
32 where "U3 = {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}" |
34 |
33 |
35 U4 :: command |
34 definition U4 :: command |
36 "U4 == {(s,s'). s' = s (|p:=True, m:=0|) & m s = 4}" |
35 where "U4 = {(s,s'). s' = s (|p:=True, m:=0|) & m s = 4}" |
37 |
36 |
38 (** The program for process V **) |
37 (** The program for process V **) |
39 |
38 |
40 V0 :: command |
39 definition V0 :: command |
41 "V0 == {(s,s'). s' = s (|v:=True, n:=1|) & n s = 0}" |
40 where "V0 = {(s,s'). s' = s (|v:=True, n:=1|) & n s = 0}" |
42 |
41 |
43 V1 :: command |
42 definition V1 :: command |
44 "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = 1}" |
43 where "V1 = {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = 1}" |
45 |
44 |
46 V2 :: command |
45 definition V2 :: command |
47 "V2 == {(s,s'). s' = s (|n:=3|) & p s & n s = 2}" |
46 where "V2 = {(s,s'). s' = s (|n:=3|) & p s & n s = 2}" |
48 |
47 |
49 V3 :: command |
48 definition V3 :: command |
50 "V3 == {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}" |
49 where "V3 = {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}" |
51 |
50 |
52 V4 :: command |
51 definition V4 :: command |
53 "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}" |
52 where "V4 = {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}" |
54 |
53 |
55 Mutex :: "state program" |
54 definition Mutex :: "state program" |
56 "Mutex == mk_total_program |
55 where "Mutex = mk_total_program |
57 ({s. ~ u s & ~ v s & m s = 0 & n s = 0}, |
56 ({s. ~ u s & ~ v s & m s = 0 & n s = 0}, |
58 {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, |
57 {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, |
59 UNIV)" |
58 UNIV)" |
60 |
59 |
61 |
60 |
62 (** The correct invariants **) |
61 (** The correct invariants **) |
63 |
62 |
64 IU :: "state set" |
63 definition IU :: "state set" |
65 "IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}" |
64 where "IU = {s. (u s = (1 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}" |
66 |
65 |
67 IV :: "state set" |
66 definition IV :: "state set" |
68 "IV == {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}" |
67 where "IV = {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}" |
69 |
68 |
70 (** The faulty invariant (for U alone) **) |
69 (** The faulty invariant (for U alone) **) |
71 |
70 |
72 bad_IU :: "state set" |
71 definition bad_IU :: "state set" |
73 "bad_IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) & |
72 where "bad_IU = {s. (u s = (1 \<le> m s & m s \<le> 3)) & |
74 (3 \<le> m s & m s \<le> 4 --> ~ p s)}" |
73 (3 \<le> m s & m s \<le> 4 --> ~ p s)}" |
75 |
74 |
76 |
75 |
77 declare Mutex_def [THEN def_prg_Init, simp] |
76 declare Mutex_def [THEN def_prg_Init, simp] |
78 |
77 |