-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathABSpec.tla
67 lines (55 loc) · 3.35 KB
/
ABSpec.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
------------------------------ MODULE ABSpec --------------------------------
EXTENDS Integers
CONSTANT Data \* The set of all possible data values.
VARIABLES AVar, \* The last <<value, bit>> pair A decided to send.
BVar \* The last <<value, bit>> pair B received.
(***************************************************************************)
(* Type correctness means that AVar and BVar are tuples <<d, i>> where *)
(* d \in Data and i \in {0, 1}. *)
(***************************************************************************)
TypeOK == /\ AVar \in Data \X {0,1}
/\ BVar \in Data \X {0,1}
(***************************************************************************)
(* It's useful to define vars to be the tuple of all variables, for *)
(* example so we can write [Next]_vars instead of [Next]_<< ... >> *)
(***************************************************************************)
vars == << AVar, BVar >>
(***************************************************************************)
(* Initially AVar can equal <<d, 1>> for any Data value d, and BVar equals *)
(* AVar. *)
(***************************************************************************)
Init == /\ AVar \in Data \X {1}
/\ BVar = AVar
(***************************************************************************)
(* When AVar = BVar, the sender can "send" an arbitrary data d item by *)
(* setting AVar[1] to d and complementing AVar[2]. It then waits until *)
(* the receiver "receives" the message by setting BVar to AVar before it *)
(* can send its next message. Sending is described by action A and *)
(* receiving by action B. *)
(***************************************************************************)
A == /\ AVar = BVar
/\ \E d \in Data: AVar' = <<d, 1 - AVar[2]>>
/\ BVar' = BVar
B == /\ AVar # BVar
/\ BVar' = AVar
/\ AVar' = AVar
Next == A \/ B
Spec == Init /\ [][Next]_vars
(***************************************************************************)
(* For understanding the spec, it's useful to define formulas that should *)
(* be invariants and check that they are invariant. The following *)
(* invariant Inv asserts that, if AVar and BVar have equal second *)
(* components, then they are equal (which by the invariance of TypeOK *)
(* implies that they have equal first components). *)
(***************************************************************************)
Inv == (AVar[2] = BVar[2]) => (AVar = BVar)
-----------------------------------------------------------------------------
(***************************************************************************)
(* FairSpec is Spec with the addition requirement that it keeps taking *)
(* steps. *)
(***************************************************************************)
FairSpec == Spec /\ WF_vars(Next)
=============================================================================
\* Modification History
\* Last modified Wed Oct 18 04:07:37 PDT 2017 by lamport
\* Created Fri Sep 04 07:08:22 PDT 2015 by lamport