--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Mutex.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,86 @@
+(* Title: ZF/UNITY/Mutex.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+
+Variables' types are introduced globally so that type verification of
+UNITY programs/specifications reduce to the usual ZF typechecking.
+An ill-tyed expression will reduce to the empty set.
+*)
+
+Mutex = SubstAx +
+consts
+ p, m, n, u, v :: i
+
+translations
+ "p" == "Var([])"
+ "m" == "Var([0])"
+ "n" == "Var([1])"
+ "u" == "Var([1,0])"
+ "v" == "Var([1,1])"
+
+rules (** Type declarations **)
+ p_type "type_of(p)=bool"
+ m_type "type_of(m)=int"
+ n_type "type_of(n)=int"
+ u_type "type_of(u)=bool"
+ v_type "type_of(v)=bool"
+
+constdefs
+ (** The program for process U **)
+ U0 :: i
+ "U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}"
+
+ U1 :: i
+ "U1 == {<s,t>:state*state. t = s(p:= s`v, m:=#2) & s`m = #1}"
+
+ U2 :: i
+ "U2 == {<s,t>:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}"
+
+ U3 :: i
+ "U3 == {<s,t>:state*state. t=s(u:=0, m:=#4) & s`m = #3}"
+
+ U4 :: i
+ "U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}"
+
+
+ (** The program for process V **)
+
+ V0 :: i
+ "V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}"
+
+ V1 :: i
+ "V1 == {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}"
+
+ V2 :: i
+ "V2 == {<s,t>:state*state. t = s(n:=#3) & s`p=1 & s`n = #2}"
+
+ V3 :: i
+ "V3 == {<s,t>:state*state. t = s (v:=0, n:=#4) & s`n = #3}"
+
+ V4 :: i
+ "V4 == {<s,t>:state*state. t = s (p:=0, n:=#0) & s`n = #4}"
+
+ Mutex :: i
+ "Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0},
+ {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, action)"
+
+ (** The correct invariants **)
+
+ IU :: i
+ "IU == {s:state. (s`u = 1<->(#1 $<= s`m & s`m $<= #3))
+ & (s`m = #3 --> s`p=0)}"
+
+ IV :: i
+ "IV == {s:state. (s`v = 1 <-> (#1 $<= s`n & s`n $<= #3))
+ & (s`n = #3 --> s`p=1)}"
+
+ (** The faulty invariant (for U alone) **)
+
+ bad_IU :: i
+ "bad_IU == {s:state. (s`u = 1 <-> (#1 $<= s`m & s`m $<= #3))&
+ (#3 $<= s`m & s`m $<= #4 --> s`p=0)}"
+
+end
\ No newline at end of file