hellerve/tla-notes
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

ab: add initial specs

Browse Source
This commit is contained in:
Veit Heller
2019-01-14 18:43:28 +01:00
parent 31fbbc4d95
commit ea55b8b33a
2 changed files with 166 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

100
AB.tla Normal file
View File

@@ -0,0 +1,100 @@
--------------------------------- MODULE AB ---------------------------------
EXTENDS Integers, Sequences
CONSTANT Data
(***************************************************************************)
(* We first define Remove(i, seq) to be the sequence obtained by removing *)
(* element number i from sequence seq. *)
(***************************************************************************)
Remove(i, seq) ==
[j \in 1..(Len(seq)-1) |-> IF j < i THEN seq[j]
ELSE seq[j+1]]
VARIABLES AVar, BVar, \* The same as in module ABSpec
AtoB, \* The sequence of data messages in transit from sender to receiver.
BtoA \* The sequence of ack messages in transit from receiver to sender.
\* Messages are sent by appending them to the end of the sequence.
\* and received by removing them from the head of the sequence.
vars == << AVar, BVar, AtoB, BtoA >>
TypeOK == /\ AVar \in Data \X {0,1}
/\ BVar \in Data \X {0,1}
/\ AtoB \in Seq(Data \X {0,1})
/\ BtoA \in Seq({0,1})
Init == /\ AVar \in Data \X {1}
/\ BVar = AVar
/\ AtoB = << >>
/\ BtoA = << >>
(***************************************************************************)
(* The action of the sender sending a data message by appending AVar to *)
(* the end of the message queue AtoB. It will keep sending the same *)
(* message until it receives an acknowledgment for it from the receiver. *)
(***************************************************************************)
ASnd == /\ AtoB' = Append(AtoB, AVar)
/\ UNCHANGED <<AVar, BtoA, BVar>>
(***************************************************************************)
(* The action of the sender receiving an ack message. If that ack is for *)
(* the value it is sending, then it chooses another message to send and *)
(* sets AVar to that message. If the ack is for the previous value it *)
(* sent, it ignores the message. In either case, it removes the message *)
(* from BtoA. *)
(***************************************************************************)
ARcv == /\ BtoA # << >>
/\ IF Head(BtoA) = AVar[2]
THEN \E d \in Data : AVar' = <<d, 1 - AVar[2]>>
ELSE AVar' = AVar
/\ BtoA' = Tail(BtoA)
/\ UNCHANGED <<AtoB, BVar>>
(***************************************************************************)
(* The action of the receiver sending an acknowledgment message for the *)
(* last data item it received. *)
(***************************************************************************)
BSnd == /\ BtoA' = Append(BtoA, BVar[2])
/\ UNCHANGED <<AVar, BVar, AtoB>>
(***************************************************************************)
(* The action of the receiver receiving a data message. It sets BVar to *)
(* that message if it's not for the data item it has already received. *)
(***************************************************************************)
BRcv == /\ AtoB # << >>
/\ IF Head(AtoB)[2] # BVar[2]
THEN BVar' = Head(AtoB)
ELSE BVar' = BVar
/\ AtoB' = Tail(AtoB)
/\ UNCHANGED <<AVar, BtoA>>
(***************************************************************************)
(* LoseMsg is the action that removes an arbitrary message from queue AtoB *)
(* or BtoA. *)
(***************************************************************************)
LoseMsg == /\ \/ /\ \E i \in 1..Len(AtoB):
AtoB' = Remove(i, AtoB)
/\ BtoA' = BtoA
\/ /\ \E i \in 1..Len(BtoA):
BtoA' = Remove(i, BtoA)
/\ AtoB' = AtoB
/\ UNCHANGED << AVar, BVar >>
Next == ASnd \/ ARcv \/ BSnd \/ BRcv \/ LoseMsg
Spec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
ABS == INSTANCE ABSpec
THEOREM Spec => ABS!Spec
-----------------------------------------------------------------------------
(***************************************************************************)
(* FairSpec is Spec with fairness conditions added. *)
(***************************************************************************)
FairSpec == Spec /\ SF_vars(ARcv) /\ SF_vars(BRcv) /\
WF_vars(ASnd) /\ WF_vars(BSnd)
=============================================================================
\* Modification History
\* Last modified Mon Jan 14 18:42:09 CET 2019 by veitheller
\* Created Wed Mar 25 11:53:40 PDT 2015 by lamport

66
ABSpec.tla Normal file
View File

@@ -0,0 +1,66 @@
------------------------------ 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 Mon Jan 14 17:53:44 CET 2019 by veitheller
\* Created Fri Sep 04 07:08:22 PDT 2015 by lamport