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