src/HOL/UNITY/Simple/Mutex.thy
 author paulson Mon, 05 Mar 2001 15:47:11 +0100 changeset 11195 65ede8dfe304 child 11701 3d51fbf81c17 permissions -rw-r--r--
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
```
(*  Title:      HOL/UNITY/Mutex.thy
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
*)

Mutex = SubstAx +

record state =
p :: bool
m :: int
n :: int
u :: bool
v :: bool

types command = "(state*state) set"

constdefs

(** The program for process U **)

U0 :: command
"U0 == {(s,s'). s' = s (|u:=True, m:=#1|) & m s = #0}"

U1 :: command
"U1 == {(s,s'). s' = s (|p:= v s, m:=#2|) & m s = #1}"

U2 :: command
"U2 == {(s,s'). s' = s (|m:=#3|) & ~ p s & m s = #2}"

U3 :: command
"U3 == {(s,s'). s' = s (|u:=False, m:=#4|) & m s = #3}"

U4 :: command
"U4 == {(s,s'). s' = s (|p:=True, m:=#0|) & m s = #4}"

(** The program for process V **)

V0 :: command
"V0 == {(s,s'). s' = s (|v:=True, n:=#1|) & n s = #0}"

V1 :: command
"V1 == {(s,s'). s' = s (|p:= ~ u s, n:=#2|) & n s = #1}"

V2 :: command
"V2 == {(s,s'). s' = s (|n:=#3|) & p s & n s = #2}"

V3 :: command
"V3 == {(s,s'). s' = s (|v:=False, n:=#4|) & n s = #3}"

V4 :: command
"V4 == {(s,s'). s' = s (|p:=False, n:=#0|) & n s = #4}"

Mutex :: state program
"Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
{U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
UNIV)"

(** The correct invariants **)

IU :: state set
"IU == {s. (u s = (#1 <= m s & m s <= #3)) & (m s = #3 --> ~ p s)}"

IV :: state set
"IV == {s. (v s = (#1 <= n s & n s <= #3)) & (n s = #3 --> p s)}"

(** The faulty invariant (for U alone) **)