State space visualization examples: Difference between revisions
| Line 2: | Line 2: | ||
== Alternating Bit Protocol == | == 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. | This is a visualisation of 3643 states and 11115 transitions of the MCAlternatingBit.tla model distributed with the [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html|TLC model checker], loaded with ProB. | ||
The goal predicate rBit=1 was used; those states satisfying this predicate are shown in orange. | The goal predicate rBit=1 was used; those states satisfying this predicate are shown in orange. | ||
Revision as of 17:51, 18 December 2015
Alternating Bit Protocol
This is a visualisation of 3643 states and 11115 transitions of the MCAlternatingBit.tla model distributed with the 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)
==============================================================