|
5252
|
1 |
(* Title: HOL/UNITY/Handshake.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1998 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Handshake Protocol
|
|
|
7 |
|
|
|
8 |
From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
|
|
|
9 |
*)
|
|
|
10 |
|
|
|
11 |
Handshake = Union +
|
|
|
12 |
|
|
|
13 |
record state =
|
|
|
14 |
BB :: bool
|
|
|
15 |
NF :: nat
|
|
|
16 |
NG :: nat
|
|
|
17 |
|
|
|
18 |
constdefs
|
|
|
19 |
(*F's program*)
|
|
|
20 |
cmdF :: "(state*state) set"
|
|
|
21 |
"cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
|
|
|
22 |
|
|
|
23 |
prgF :: "state program"
|
|
|
24 |
"prgF == (|Init = {s. NF s = 0 & BB s},
|
|
|
25 |
Acts = {id, cmdF}|)"
|
|
|
26 |
|
|
|
27 |
(*G's program*)
|
|
|
28 |
cmdG :: "(state*state) set"
|
|
|
29 |
"cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
|
|
|
30 |
|
|
|
31 |
prgG :: "state program"
|
|
|
32 |
"prgG == (|Init = {s. NG s = 0 & BB s},
|
|
|
33 |
Acts = {id, cmdG}|)"
|
|
|
34 |
|
|
|
35 |
(*the joint invariant*)
|
|
|
36 |
invFG :: "state set"
|
|
|
37 |
"invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
|
|
|
38 |
|
|
|
39 |
end
|