State space visualization examples: Difference between revisions

Line 90: Line 90:
This is the visualisation of a simple threads model, of two threads with n=51 steps before a synchronisation occurs and threads start again. The state space contains 5410 nodes.
This is the visualisation of a simple threads model, of two threads with n=51 steps before a synchronisation occurs and threads start again. The state space contains 5410 nodes.


[[File:Threads51_sfdp.png|800px|center]]
[[File:Threads51_sfdp.png|600px|center]]


With partial order reduction, the state space is reduced to 208 states:
With partial order reduction, the state space is reduced to 208 states:
[[File:Threads51_POR_sfdp.png|800px|center]]
[[File:Threads51_POR_sfdp.png|600px|center]]

Revision as of 13:37, 21 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.

MCAlternatingBit sfdp.png

Below is a projection of this state space onto the expression (rBit,sBit), using the "Custom Transition Diagram" feature of ProB:

MCAlternatingBit projsrBit.png

More details about this statespace projection feature can be found in our ICFEM'15 article.

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 3866 states and 9661 transitions of a TLA+ model of a FIFO, as distributed with the TLA+ tools. This model (MCInnerFIFO) was loaded with ProB for TLA+ and the model checker run so that all states with queue size greater than qLen (3) were ignored, i.e., no successor states were computed (this can be set by defining SCOPE==card(q)<=qLen). The colour indicates the length of the queue variable q of the model (gray=0,blue=1,red=2, green=3, lightgray=4) .


MCInnerFIFO q3 sfdp.png


Below is a projection of this state space onto the expression card(q), using the "Custom Transition Diagram" feature of ProB:

MCInnerFIFO proj cardq.png

RushHour

This is a visualisation of the Rush_Hour_Puzzle Rush Hour puzzle B model, at the moment that ProB has found a solution. The solution node(s) are marked in orange.

RushHour sfdp.png

CAN Bus

This is a visualisation of the statespace of an Event-B model of a CAN Bus. The colours indicate the size of the BUSwrite variable (gray=0,blue=1,red=2, green=3, lightgray=4).

CANBus sfdp.png


Hanoi (6 Discs)

This is a visualisation of the statespace of a B model of the towers of Hanoi for 6 discs. The state space contains 731 nodes and 2186 nodes.

Hanoi6 sfdp.png

One can observe that this figure resembles a Sierpinski triangle. This is no coincidence, the state space of Hanoi is one.

Below is a projection of this state space onto the expression card(on(dest))), using the "Custom Transition Diagram" feature of ProB:

Hanoi6 proj cardondest.png


Threads - Partial Order Reduction

This is the visualisation of a simple threads model, of two threads with n=51 steps before a synchronisation occurs and threads start again. The state space contains 5410 nodes.

Threads51 sfdp.png

With partial order reduction, the state space is reduced to 208 states:

Threads51 POR sfdp.png