CounterTie

TLC reached 5 states and 4 steps. The chart draws 6 states and 6 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. 1 step that the constraints exclude ends a rule's path, and the chart includes it. TLC checks the rules after such a step, but it does not take the step.