CounterInitPast

TLC reached 0 states and 0 steps. The chart draws 1 states and 0 arrows. Every initial state is outside the constraints, so TLC explores none of them. 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.

NotNine breaksCopy Anchor Link

The shortest path has 0 steps: 0. 9

Rules that holdCopy Anchor Link

NoDeadlock