src/HOL/UNITY/Simple/Mutex.thy
changeset 11701 3d51fbf81c17
parent 11195 65ede8dfe304
child 11704 3c50a2cd6f00
equal deleted inserted replaced
11700:a0e6bda62b7b 11701:3d51fbf81c17
    20 constdefs
    20 constdefs
    21   
    21   
    22   (** The program for process U **)
    22   (** The program for process U **)
    23   
    23   
    24   U0 :: command
    24   U0 :: command
    25     "U0 == {(s,s'). s' = s (|u:=True, m:=#1|) & m s = #0}"
    25     "U0 == {(s,s'). s' = s (|u:=True, m:=Numeral1|) & m s = Numeral0}"
    26 
    26 
    27   U1 :: command
    27   U1 :: command
    28     "U1 == {(s,s'). s' = s (|p:= v s, m:=#2|) & m s = #1}"
    28     "U1 == {(s,s'). s' = s (|p:= v s, m:=# 2|) & m s = Numeral1}"
    29 
    29 
    30   U2 :: command
    30   U2 :: command
    31     "U2 == {(s,s'). s' = s (|m:=#3|) & ~ p s & m s = #2}"
    31     "U2 == {(s,s'). s' = s (|m:=# 3|) & ~ p s & m s = # 2}"
    32 
    32 
    33   U3 :: command
    33   U3 :: command
    34     "U3 == {(s,s'). s' = s (|u:=False, m:=#4|) & m s = #3}"
    34     "U3 == {(s,s'). s' = s (|u:=False, m:=# 4|) & m s = # 3}"
    35 
    35 
    36   U4 :: command
    36   U4 :: command
    37     "U4 == {(s,s'). s' = s (|p:=True, m:=#0|) & m s = #4}"
    37     "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = # 4}"
    38 
    38 
    39   (** The program for process V **)
    39   (** The program for process V **)
    40   
    40   
    41   V0 :: command
    41   V0 :: command
    42     "V0 == {(s,s'). s' = s (|v:=True, n:=#1|) & n s = #0}"
    42     "V0 == {(s,s'). s' = s (|v:=True, n:=Numeral1|) & n s = Numeral0}"
    43 
    43 
    44   V1 :: command
    44   V1 :: command
    45     "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=#2|) & n s = #1}"
    45     "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=# 2|) & n s = Numeral1}"
    46 
    46 
    47   V2 :: command
    47   V2 :: command
    48     "V2 == {(s,s'). s' = s (|n:=#3|) & p s & n s = #2}"
    48     "V2 == {(s,s'). s' = s (|n:=# 3|) & p s & n s = # 2}"
    49 
    49 
    50   V3 :: command
    50   V3 :: command
    51     "V3 == {(s,s'). s' = s (|v:=False, n:=#4|) & n s = #3}"
    51     "V3 == {(s,s'). s' = s (|v:=False, n:=# 4|) & n s = # 3}"
    52 
    52 
    53   V4 :: command
    53   V4 :: command
    54     "V4 == {(s,s'). s' = s (|p:=False, n:=#0|) & n s = #4}"
    54     "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = # 4}"
    55 
    55 
    56   Mutex :: state program
    56   Mutex :: state program
    57     "Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
    57     "Mutex == mk_program ({s. ~ u s & ~ v s & m s = Numeral0 & n s = Numeral0},
    58 		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
    58 		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
    59 			  UNIV)"
    59 			  UNIV)"
    60 
    60 
    61 
    61 
    62   (** The correct invariants **)
    62   (** The correct invariants **)
    63 
    63 
    64   IU :: state set
    64   IU :: state set
    65     "IU == {s. (u s = (#1 <= m s & m s <= #3)) & (m s = #3 --> ~ p s)}"
    65     "IU == {s. (u s = (Numeral1 <= m s & m s <= # 3)) & (m s = # 3 --> ~ p s)}"
    66 
    66 
    67   IV :: state set
    67   IV :: state set
    68     "IV == {s. (v s = (#1 <= n s & n s <= #3)) & (n s = #3 --> p s)}"
    68     "IV == {s. (v s = (Numeral1 <= n s & n s <= # 3)) & (n s = # 3 --> p s)}"
    69 
    69 
    70   (** The faulty invariant (for U alone) **)
    70   (** The faulty invariant (for U alone) **)
    71 
    71 
    72   bad_IU :: state set
    72   bad_IU :: state set
    73     "bad_IU == {s. (u s = (#1 <= m s & m s <= #3)) &
    73     "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= # 3)) &
    74 	           (#3 <= m s & m s <= #4 --> ~ p s)}"
    74 	           (# 3 <= m s & m s <= # 4 --> ~ p s)}"
    75 
    75 
    76 end
    76 end