Why can the over-approximated set of legitimate states grow?

[grencez]

It happens when considering multiple systems. A candidate action of one system, but not another, can be added to both. I think this only allows the legitimate states to grow because of the extra step at the end of "shadow_ck()" that grows the over-approximation to include states that may not be part of the fixpoint.

My question is... should this growth happen? What use cases does it affect?

[grencez]

Issue #3 could benefit from this growth not happening, because it would then give a set of states that reliably shrinks.
We could also use the larger set that includes the growth, but it must consider candidate actions of all systems. In this case, the larger set would ideally be a step outside of "shadow_ck()".

[grencez]

The growth in "shadow_ck()" is not the only thing that allows the over-approximation to grow. Indeed, a new legitimate cycle can form due to an action that was not a candidate (but was a candidate of another system under consideration). This is exhibited by the examplesett/TokenRingFiveState.prot example. Certainly if you give the -optimize flag.

However, the invariant does not appear to shrink if "check_forward()" does not discard unnecessary candidate actions outright. We can still discard candidates that break self-disablement or create conflicts.