State space visualization examples

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.