Skip to content

Mec in Interval Iteration

Using the following command.

check erlang.jani -E K=5000,R=100,TIME_BOUND=50 --alg IntervalIteration --props TminReach

The statespace of interval iterations contains a mec. State with index 8 goes to state with index 11. The state with index 11 goes to state with index 8. All with one branch and probability one.

I noticed that avoid was null.