src/HOL/UNITY/Simple/Mutex.thy
 changeset 11195 65ede8dfe304 child 11701 3d51fbf81c17
1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy	Mon Mar 05 15:47:11 2001 +0100
1.3 @@ -0,0 +1,76 @@
1.4 +(*  Title:      HOL/UNITY/Mutex.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 +    Copyright   1998  University of Cambridge
1.8 +
1.9 +Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
1.10 +*)
1.11 +
1.12 +Mutex = SubstAx +
1.13 +
1.14 +record state =
1.15 +  p :: bool
1.16 +  m :: int
1.17 +  n :: int
1.18 +  u :: bool
1.19 +  v :: bool
1.20 +
1.21 +types command = "(state*state) set"
1.22 +
1.23 +constdefs
1.24 +
1.25 +  (** The program for process U **)
1.26 +
1.27 +  U0 :: command
1.28 +    "U0 == {(s,s'). s' = s (|u:=True, m:=#1|) & m s = #0}"
1.29 +
1.30 +  U1 :: command
1.31 +    "U1 == {(s,s'). s' = s (|p:= v s, m:=#2|) & m s = #1}"
1.32 +
1.33 +  U2 :: command
1.34 +    "U2 == {(s,s'). s' = s (|m:=#3|) & ~ p s & m s = #2}"
1.35 +
1.36 +  U3 :: command
1.37 +    "U3 == {(s,s'). s' = s (|u:=False, m:=#4|) & m s = #3}"
1.38 +
1.39 +  U4 :: command
1.40 +    "U4 == {(s,s'). s' = s (|p:=True, m:=#0|) & m s = #4}"
1.41 +
1.42 +  (** The program for process V **)
1.43 +
1.44 +  V0 :: command
1.45 +    "V0 == {(s,s'). s' = s (|v:=True, n:=#1|) & n s = #0}"
1.46 +
1.47 +  V1 :: command
1.48 +    "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=#2|) & n s = #1}"
1.49 +
1.50 +  V2 :: command
1.51 +    "V2 == {(s,s'). s' = s (|n:=#3|) & p s & n s = #2}"
1.52 +
1.53 +  V3 :: command
1.54 +    "V3 == {(s,s'). s' = s (|v:=False, n:=#4|) & n s = #3}"
1.55 +
1.56 +  V4 :: command
1.57 +    "V4 == {(s,s'). s' = s (|p:=False, n:=#0|) & n s = #4}"
1.58 +
1.59 +  Mutex :: state program
1.60 +    "Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
1.61 +		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
1.62 +			  UNIV)"
1.63 +
1.64 +
1.65 +  (** The correct invariants **)
1.66 +
1.67 +  IU :: state set
1.68 +    "IU == {s. (u s = (#1 <= m s & m s <= #3)) & (m s = #3 --> ~ p s)}"
1.69 +
1.70 +  IV :: state set
1.71 +    "IV == {s. (v s = (#1 <= n s & n s <= #3)) & (n s = #3 --> p s)}"
1.72 +
1.73 +  (** The faulty invariant (for U alone) **)
1.74 +
1.75 +  bad_IU :: state set
1.76 +    "bad_IU == {s. (u s = (#1 <= m s & m s <= #3)) &
1.77 +	           (#3 <= m s & m s <= #4 --> ~ p s)}"
1.78 +
1.79 +end