State space visualization examples: Difference between revisions

(Created page with " == 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...")
 
Line 6: Line 6:
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.


[[File:MCAlternatingBit_sfdp.png]]
[[File:MCAlternatingBit_sfdp.png|800px|center]]

Revision as of 17:46, 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.

MCAlternatingBit sfdp.png