author | paulson |
Wed, 18 Nov 1998 15:10:46 +0100 | |
changeset 5931 | 325300576da7 |
parent 5596 | b29d18d8c4d2 |
child 6012 | 1894bfc4aee9 |
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 = |
12 |
PP :: bool |
|
5596 | 13 |
MM :: int |
14 |
NN :: int |
|
5232 | 15 |
UU :: bool |
16 |
VV :: bool |
|
4776 | 17 |
|
18 |
constdefs |
|
5253 | 19 |
|
20 |
(** The program for process U **) |
|
21 |
||
5232 | 22 |
cmd0U :: "(state*state) set" |
5596 | 23 |
"cmd0U == {(s,s'). s' = s (|UU:=True, MM:=#1|) & MM s = #0}" |
5232 | 24 |
|
25 |
cmd1U :: "(state*state) set" |
|
5596 | 26 |
"cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=#2|) & MM s = #1}" |
4776 | 27 |
|
5232 | 28 |
cmd2U :: "(state*state) set" |
5596 | 29 |
"cmd2U == {(s,s'). s' = s (|MM:=#3|) & ~ PP s & MM s = #2}" |
4776 | 30 |
|
5232 | 31 |
cmd3U :: "(state*state) set" |
5596 | 32 |
"cmd3U == {(s,s'). s' = s (|UU:=False, MM:=#4|) & MM s = #3}" |
5232 | 33 |
|
34 |
cmd4U :: "(state*state) set" |
|
5596 | 35 |
"cmd4U == {(s,s'). s' = s (|PP:=True, MM:=#0|) & MM s = #4}" |
4776 | 36 |
|
5253 | 37 |
(** The program for process V **) |
38 |
||
5232 | 39 |
cmd0V :: "(state*state) set" |
5596 | 40 |
"cmd0V == {(s,s'). s' = s (|VV:=True, NN:=#1|) & NN s = #0}" |
5232 | 41 |
|
42 |
cmd1V :: "(state*state) set" |
|
5596 | 43 |
"cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=#2|) & NN s = #1}" |
4776 | 44 |
|
5232 | 45 |
cmd2V :: "(state*state) set" |
5596 | 46 |
"cmd2V == {(s,s'). s' = s (|NN:=#3|) & PP s & NN s = #2}" |
4776 | 47 |
|
5232 | 48 |
cmd3V :: "(state*state) set" |
5596 | 49 |
"cmd3V == {(s,s'). s' = s (|VV:=False, NN:=#4|) & NN s = #3}" |
5232 | 50 |
|
51 |
cmd4V :: "(state*state) set" |
|
5596 | 52 |
"cmd4V == {(s,s'). s' = s (|PP:=False, NN:=#0|) & NN s = #4}" |
4776 | 53 |
|
5253 | 54 |
Mprg :: state program |
5596 | 55 |
"Mprg == mk_program ({s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0}, |
56 |
{cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, |
|
57 |
cmd0V, cmd1V, cmd2V, cmd3V, cmd4V})" |
|
5253 | 58 |
|
5232 | 59 |
|
60 |
(** The correct invariants **) |
|
61 |
||
62 |
invariantU :: "state set" |
|
5596 | 63 |
"invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) & |
64 |
(MM s = #3 --> ~ PP s)}" |
|
5232 | 65 |
|
66 |
invariantV :: "state set" |
|
5596 | 67 |
"invariantV == {s. (VV s = (#1 <= NN s & NN s <= #3)) & |
68 |
(NN s = #3 --> PP s)}" |
|
5232 | 69 |
|
70 |
(** The faulty invariant (for U alone) **) |
|
71 |
||
72 |
bad_invariantU :: "state set" |
|
5596 | 73 |
"bad_invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) & |
74 |
(#3 <= MM s & MM s <= #4 --> ~ PP s)}" |
|
4776 | 75 |
|
76 |
end |