CounterStart

TLC reached 3 states and 2 steps. The chart draws 4 states and 2 arrows. 1 state outside the constraints ends a rule's path, and the chart includes it. TLC checks the rules in a state outside the constraints, but it does not explore past it.

TypeOK breaksCopy Anchor Link

The shortest path has 0 steps: 0. 7

Rules that holdCopy Anchor Link

NoDeadlock