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