src/HOL/UNITY/Mutex.thy
 changeset 4776 1f9362e769c1 child 4896 4727272f3db6
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/UNITY/Mutex.thy	Fri Apr 03 12:34:33 1998 +0200
1.3 @@ -0,0 +1,74 @@
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 = Update + UNITY + Traces + SubstAx +
1.13 +
1.14 +(*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
1.15 +syntax
1.16 +  "3"       :: nat                ("3")
1.17 +  "4"       :: nat                ("4")
1.18 +
1.19 +translations
1.20 +   "3"  == "Suc 2"
1.21 +   "4"  == "Suc 3"
1.22 +
1.23 +
1.24 +(*program variables*)
1.25 +datatype pvar = PP | MM | NN | UU | VV
1.26 +
1.27 +(*No booleans; instead True=1 and False=0*)
1.28 +types state = pvar => nat
1.29 +
1.30 +constdefs
1.31 +  cmd0 :: "[pvar,pvar] => (state*state) set"
1.32 +    "cmd0 u m == {(s,s'). s' = s[u|->1][m|->1] & s m = 0}"
1.33 +
1.34 +  cmd1u :: "(state*state) set"
1.35 +    "cmd1u == {(s,s'). s' = s[PP|-> s VV][MM|->2] & s MM = 1}"
1.36 +
1.37 +  cmd1v :: "(state*state) set"
1.38 +    "cmd1v == {(s,s'). s' = s[PP|-> 1 - s UU][NN|->2] & s NN = 1}"
1.39 +
1.40 +  (*Put pv=0 for u's program and pv=1 for v's program*)
1.41 +  cmd2 :: "[nat,pvar] => (state*state) set"
1.42 +    "cmd2 pv m == {(s,s'). s' = s[m|->3] & s PP = pv & s m = 2}"
1.43 +
1.44 +  cmd3 :: "[pvar,pvar] => (state*state) set"
1.45 +    "cmd3 u m == {(s,s'). s' = s[u|->0][m|->4] & s m = 3}"
1.46 +
1.47 +  (*Put pv=1 for u's program and pv=0 for v's program*)
1.48 +  cmd4 :: "[nat,pvar] => (state*state) set"
1.49 +    "cmd4 pv m == {(s,s'). s' = s[PP|->pv][m|->0] & s m = 4}"
1.50 +
1.51 +  mutex :: "(state*state) set set"
1.52 +    "mutex == {id,
1.53 +	       cmd0 UU MM, cmd0 VV NN,
1.54 +	       cmd1u, cmd1v,
1.55 +	       cmd2 0 MM, cmd2 1 NN,
1.56 +	       cmd3 UU MM, cmd3 VV NN,
1.57 +	       cmd4 1 MM, cmd4 0 NN}"
1.58 +
1.59 +  MInit :: "state set"
1.60 +    "MInit == {s. s PP < 2 & s UU = 0 & s VV = 0 & s MM = 0 & s NN = 0}"
1.61 +
1.62 +  boolVars :: "state set"
1.63 +    "boolVars == {s. s PP<2 & s UU < 2 & s VV < 2}"
1.64 +
1.65 +  (*Put pv=0 for u's program and pv=1 for v's program*)
1.66 +  invariant :: "[nat,pvar,pvar] => state set"
1.67 +    "invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
1.68 +			     (s m = 3 --> s PP = pv)}"
1.69 +
1.70 +  bad_invariant :: "[nat,pvar,pvar] => state set"
1.71 +    "bad_invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
1.72 +			         (3 <= s m & s m <= 4 --> s PP = pv)}"
1.73 +
1.74 +
1.75 +
1.76 +
1.77 +end
```