No edit summary |
|||
Line 10: | Line 10: | ||
[[File:MCAlternatingBit_sfdp.png|1000px|center]] | [[File:MCAlternatingBit_sfdp.png|1000px|center]] | ||
Below is a projection of this state space onto the expression <tt>(rBit,sBit)</tt>: | |||
[[File:MCAlternatingBit_projsrBit.png|400px|center]] | |||
The main file of the model is: | The main file of the model is: |
(This page is under construction)
This is a visualisation of 3643 states and 11115 transitions of a TLA+ model of the alternating bit protocol, as distributed with the TLA+ tools. This model (MCAlternatingBit.tla) was loaded with ProB for TLA+, the model checker run for a few seconds and then the command "State Space Fast Rendering" with options (scale,fast) was used.
The goal predicate rBit=1 was used; those states satisfying this predicate are shown in orange.
Below is a projection of this state space onto the expression (rBit,sBit):
The main file of the model is:
--------------------------- MODULE MCAlternatingBit ------------------------- EXTENDS AlternatingBit, TLC INSTANCE ABCorrectness CONSTANTS msgQLen, ackQLen SeqConstraint == /\ Len(msgQ) \leq msgQLen /\ Len(ackQ) \leq ackQLen SentLeadsToRcvd == \A d \in Data : (sent = d) /\ (sBit # sAck) ~> (rcvd = d) ============================================================================= ImpliedAction == [ABCNext]_cvars TNext == WF_msgQ(~ABTypeInv') TProp == \A d \in Data : (sent = d) => [](sent = d) CSpec == ABSpec /\ TNext DataPerm == Permutations(Data) ==============================================================