State space visualization examples: Difference between revisions
| Line 7: | Line 7: | ||
[[File:MCAlternatingBit_sfdp.png|1000px|center]] | [[File:MCAlternatingBit_sfdp.png|1000px|center]] | ||
The main file of the model is: | |||
<PRE> | |||
--------------------------- 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) | |||
============================================================== | |||
</PRE> | |||
Revision as of 17:48, 18 December 2015
Alternating Bit Protocol
This is a visualisation of 3643 states and 11115 transitions of the MCAlternatingBit.tla model distributed with the TLC model checker, loaded with ProB.
The goal predicate rBit=1 was used; those states satisfying this predicate are shown in orange.
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)
==============================================================