The dnj branching bisimulation algorithm triggers an assertion with the --tau option about mcrl2 HOT 4 CLOSED

The assertion did not take into account a situation if the last label has zero transitions. I have reformulated the assertion to include that case (not yet checked in, still testing).
Is there a way to create labels with zero transitions in other places than the last label, so that one might test that as well?

from mcrl2.

I think it’s solved, I am not sure whether I can close the issue or I should let one of you run additional tests before closing.

from mcrl2.

I have re-enabled the test that was used to find this case as it seem to work now. I am not sure why reading an .aut file results in an LTS where one label has zero transitions, but I guess in general this would only be created in code.

from mcrl2.

Regarding the question of David, I believe that by using the --tau option, you can hide multiple action labels at once. These labels will not occur anymore in the transition system, and one of them will not be positioned as the last label. It is also possible that both labels are not the last label.

from mcrl2.