diff --git a/AB.tla b/AB.tla new file mode 100644 index 0000000..d8948f4 --- /dev/null +++ b/AB.tla @@ -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 <> + +(***************************************************************************) +(* 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' = <> + ELSE AVar' = AVar + /\ BtoA' = Tail(BtoA) + /\ UNCHANGED <> + +(***************************************************************************) +(* The action of the receiver sending an acknowledgment message for the *) +(* last data item it received. *) +(***************************************************************************) +BSnd == /\ BtoA' = Append(BtoA, BVar[2]) + /\ UNCHANGED <> + +(***************************************************************************) +(* 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 <> + +(***************************************************************************) +(* 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 diff --git a/ABSpec.tla b/ABSpec.tla new file mode 100644 index 0000000..8a9432c --- /dev/null +++ b/ABSpec.tla @@ -0,0 +1,66 @@ +------------------------------ MODULE ABSpec -------------------------------- +EXTENDS Integers + +CONSTANT Data \* The set of all possible data values. + +VARIABLES AVar, \* The last <> pair A decided to send. + BVar \* The last <> pair B received. + +(***************************************************************************) +(* Type correctness means that AVar and BVar are tuples <> 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 <> 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' = <> + /\ 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