State space visualization examples: Difference between revisions
No edit summary |
|||
| Line 45: | Line 45: | ||
This model (MCAlternatingBit.tla) was loaded with [[TLA|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. | This model (MCAlternatingBit.tla) was loaded with [[TLA|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 colour indicates the length of the queue variable q of the model (gray=0,blue=1,red=2, green=3) . | |||
[[File:MCInnerFIFO_sfdp.png|1000px|center]] | [[File:MCInnerFIFO_sfdp.png|1000px|center]] | ||
Revision as of 09:17, 20 December 2015
(This page is under construction)
Alternating Bit Protocol
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)
==============================================================
MCInnerFIFO
This is a visualisation of 5081 states and 7569 transitions of a TLA+ model of a FIFO, 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 colour indicates the length of the queue variable q of the model (gray=0,blue=1,red=2, green=3) .
