34 u_type: "type_of(u)=bool \<and> default_val(u)=0" and |
34 u_type: "type_of(u)=bool \<and> default_val(u)=0" and |
35 v_type: "type_of(v)=bool \<and> default_val(v)=0" |
35 v_type: "type_of(v)=bool \<and> default_val(v)=0" |
36 |
36 |
37 definition |
37 definition |
38 (** The program for process U **) |
38 (** The program for process U **) |
39 "U0 \<equiv> {<s,t>:state*state. t = s(u:=1, m:=#1) \<and> s`m = #0}" |
39 "U0 \<equiv> {\<langle>s,t\<rangle>:state*state. t = s(u:=1, m:=#1) \<and> s`m = #0}" |
40 |
40 |
41 definition |
41 definition |
42 "U1 \<equiv> {<s,t>:state*state. t = s(p:= s`v, m:=#2) \<and> s`m = #1}" |
42 "U1 \<equiv> {\<langle>s,t\<rangle>:state*state. t = s(p:= s`v, m:=#2) \<and> s`m = #1}" |
43 |
43 |
44 definition |
44 definition |
45 "U2 \<equiv> {<s,t>:state*state. t = s(m:=#3) \<and> s`p=0 \<and> s`m = #2}" |
45 "U2 \<equiv> {\<langle>s,t\<rangle>:state*state. t = s(m:=#3) \<and> s`p=0 \<and> s`m = #2}" |
46 |
46 |
47 definition |
47 definition |
48 "U3 \<equiv> {<s,t>:state*state. t=s(u:=0, m:=#4) \<and> s`m = #3}" |
48 "U3 \<equiv> {\<langle>s,t\<rangle>:state*state. t=s(u:=0, m:=#4) \<and> s`m = #3}" |
49 |
49 |
50 definition |
50 definition |
51 "U4 \<equiv> {<s,t>:state*state. t = s(p:=1, m:=#0) \<and> s`m = #4}" |
51 "U4 \<equiv> {\<langle>s,t\<rangle>:state*state. t = s(p:=1, m:=#0) \<and> s`m = #4}" |
52 |
52 |
53 |
53 |
54 (** The program for process V **) |
54 (** The program for process V **) |
55 |
55 |
56 definition |
56 definition |
57 "V0 \<equiv> {<s,t>:state*state. t = s (v:=1, n:=#1) \<and> s`n = #0}" |
57 "V0 \<equiv> {\<langle>s,t\<rangle>:state*state. t = s (v:=1, n:=#1) \<and> s`n = #0}" |
58 |
58 |
59 definition |
59 definition |
60 "V1 \<equiv> {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) \<and> s`n = #1}" |
60 "V1 \<equiv> {\<langle>s,t\<rangle>:state*state. t = s(p:=not(s`u), n:=#2) \<and> s`n = #1}" |
61 |
61 |
62 definition |
62 definition |
63 "V2 \<equiv> {<s,t>:state*state. t = s(n:=#3) \<and> s`p=1 \<and> s`n = #2}" |
63 "V2 \<equiv> {\<langle>s,t\<rangle>:state*state. t = s(n:=#3) \<and> s`p=1 \<and> s`n = #2}" |
64 |
64 |
65 definition |
65 definition |
66 "V3 \<equiv> {<s,t>:state*state. t = s (v:=0, n:=#4) \<and> s`n = #3}" |
66 "V3 \<equiv> {\<langle>s,t\<rangle>:state*state. t = s (v:=0, n:=#4) \<and> s`n = #3}" |
67 |
67 |
68 definition |
68 definition |
69 "V4 \<equiv> {<s,t>:state*state. t = s (p:=0, n:=#0) \<and> s`n = #4}" |
69 "V4 \<equiv> {\<langle>s,t\<rangle>:state*state. t = s (p:=0, n:=#0) \<and> s`n = #4}" |
70 |
70 |
71 definition |
71 definition |
72 "Mutex \<equiv> mk_program({s:state. s`u=0 \<and> s`v=0 \<and> s`m = #0 \<and> s`n = #0}, |
72 "Mutex \<equiv> mk_program({s:state. s`u=0 \<and> s`v=0 \<and> s`m = #0 \<and> s`n = #0}, |
73 {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, Pow(state*state))" |
73 {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, Pow(state*state))" |
74 |
74 |