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 a TLA+ model of the alternating bit protocol, as distributed with the [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html|TLC model checker].
This is a visualisation of 3643 states and 11115 transitions of a TLA+ model of the alternating bit protocol, as distributed with the [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html| TLC model checker].
This model (MCAlternatingBit.tla) was loaded with ProB, 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 ProB, the model checker run for a few seconds and then the command "State Space Fast Rendering" with options (scale,fast) was used.



Revision as of 17:54, 18 December 2015

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 TLC model checker. This model (MCAlternatingBit.tla) was loaded with ProB, 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.

MCAlternatingBit sfdp.png


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)
==============================================================