author | paulson |
Thu, 11 Nov 1999 10:25:17 +0100 | |
changeset 8005 | b64d86018785 |
parent 6570 | a7d7985050a9 |
child 10064 | 1a77667b21ef |
permissions | -rw-r--r-- |
4776 | 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 |
||
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
9 |
Mutex = SubstAx + |
4776 | 10 |
|
5232 | 11 |
record state = |
6565 | 12 |
p :: bool |
13 |
m :: int |
|
14 |
n :: int |
|
15 |
u :: bool |
|
16 |
v :: bool |
|
17 |
||
18 |
types command = "(state*state) set" |
|
4776 | 19 |
|
20 |
constdefs |
|
5253 | 21 |
|
22 |
(** The program for process U **) |
|
23 |
||
6565 | 24 |
U0 :: command |
25 |
"U0 == {(s,s'). s' = s (|u:=True, m:=#1|) & m s = #0}" |
|
5232 | 26 |
|
6565 | 27 |
U1 :: command |
28 |
"U1 == {(s,s'). s' = s (|p:= v s, m:=#2|) & m s = #1}" |
|
4776 | 29 |
|
6565 | 30 |
U2 :: command |
31 |
"U2 == {(s,s'). s' = s (|m:=#3|) & ~ p s & m s = #2}" |
|
4776 | 32 |
|
6565 | 33 |
U3 :: command |
34 |
"U3 == {(s,s'). s' = s (|u:=False, m:=#4|) & m s = #3}" |
|
5232 | 35 |
|
6565 | 36 |
U4 :: command |
37 |
"U4 == {(s,s'). s' = s (|p:=True, m:=#0|) & m s = #4}" |
|
4776 | 38 |
|
5253 | 39 |
(** The program for process V **) |
40 |
||
6565 | 41 |
V0 :: command |
42 |
"V0 == {(s,s'). s' = s (|v:=True, n:=#1|) & n s = #0}" |
|
5232 | 43 |
|
6565 | 44 |
V1 :: command |
45 |
"V1 == {(s,s'). s' = s (|p:= ~ u s, n:=#2|) & n s = #1}" |
|
4776 | 46 |
|
6565 | 47 |
V2 :: command |
48 |
"V2 == {(s,s'). s' = s (|n:=#3|) & p s & n s = #2}" |
|
4776 | 49 |
|
6565 | 50 |
V3 :: command |
51 |
"V3 == {(s,s'). s' = s (|v:=False, n:=#4|) & n s = #3}" |
|
5232 | 52 |
|
6565 | 53 |
V4 :: command |
54 |
"V4 == {(s,s'). s' = s (|p:=False, n:=#0|) & n s = #4}" |
|
4776 | 55 |
|
6565 | 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})" |
|
5253 | 59 |
|
5232 | 60 |
|
61 |
(** The correct invariants **) |
|
62 |
||
6570 | 63 |
IU :: state set |
64 |
"IU == {s. (u s = (#1 <= m s & m s <= #3)) & (m s = #3 --> ~ p s)}" |
|
5232 | 65 |
|
6570 | 66 |
IV :: state set |
67 |
"IV == {s. (v s = (#1 <= n s & n s <= #3)) & (n s = #3 --> p s)}" |
|
5232 | 68 |
|
69 |
(** The faulty invariant (for U alone) **) |
|
70 |
||
6570 | 71 |
bad_IU :: state set |
72 |
"bad_IU == {s. (u s = (#1 <= m s & m s <= #3)) & |
|
73 |
(#3 <= m s & m s <= #4 --> ~ p s)}" |
|
4776 | 74 |
|
75 |
end |