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