src/HOL/UNITY/Simple/Mutex.thy
changeset 11195 65ede8dfe304
child 11701 3d51fbf81c17
equal deleted inserted replaced
11194:ea13ff5a26d1 11195:65ede8dfe304
       
     1 (*  Title:      HOL/UNITY/Mutex.thy
       
     2     ID:         $Id$
       
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
       
     4     Copyright   1998  University of Cambridge
       
     5 
       
     6 Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
       
     7 *)
       
     8 
       
     9 Mutex = SubstAx +
       
    10 
       
    11 record state =
       
    12   p :: bool
       
    13   m :: int
       
    14   n :: int
       
    15   u :: bool
       
    16   v :: bool
       
    17 
       
    18 types command = "(state*state) set"
       
    19 
       
    20 constdefs
       
    21   
       
    22   (** The program for process U **)
       
    23   
       
    24   U0 :: command
       
    25     "U0 == {(s,s'). s' = s (|u:=True, m:=#1|) & m s = #0}"
       
    26 
       
    27   U1 :: command
       
    28     "U1 == {(s,s'). s' = s (|p:= v s, m:=#2|) & m s = #1}"
       
    29 
       
    30   U2 :: command
       
    31     "U2 == {(s,s'). s' = s (|m:=#3|) & ~ p s & m s = #2}"
       
    32 
       
    33   U3 :: command
       
    34     "U3 == {(s,s'). s' = s (|u:=False, m:=#4|) & m s = #3}"
       
    35 
       
    36   U4 :: command
       
    37     "U4 == {(s,s'). s' = s (|p:=True, m:=#0|) & m s = #4}"
       
    38 
       
    39   (** The program for process V **)
       
    40   
       
    41   V0 :: command
       
    42     "V0 == {(s,s'). s' = s (|v:=True, n:=#1|) & n s = #0}"
       
    43 
       
    44   V1 :: command
       
    45     "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=#2|) & n s = #1}"
       
    46 
       
    47   V2 :: command
       
    48     "V2 == {(s,s'). s' = s (|n:=#3|) & p s & n s = #2}"
       
    49 
       
    50   V3 :: command
       
    51     "V3 == {(s,s'). s' = s (|v:=False, n:=#4|) & n s = #3}"
       
    52 
       
    53   V4 :: command
       
    54     "V4 == {(s,s'). s' = s (|p:=False, n:=#0|) & n s = #4}"
       
    55 
       
    56   Mutex :: state program
       
    57     "Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
       
    58 		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
       
    59 			  UNIV)"
       
    60 
       
    61 
       
    62   (** The correct invariants **)
       
    63 
       
    64   IU :: state set
       
    65     "IU == {s. (u s = (#1 <= m s & m s <= #3)) & (m s = #3 --> ~ p s)}"
       
    66 
       
    67   IV :: state set
       
    68     "IV == {s. (v s = (#1 <= n s & n s <= #3)) & (n s = #3 --> p s)}"
       
    69 
       
    70   (** The faulty invariant (for U alone) **)
       
    71 
       
    72   bad_IU :: state set
       
    73     "bad_IU == {s. (u s = (#1 <= m s & m s <= #3)) &
       
    74 	           (#3 <= m s & m s <= #4 --> ~ p s)}"
       
    75 
       
    76 end