State space visualization examples: Difference between revisions
| 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|1000px|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.
