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.
