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.