I think some background for the other developers might be good. Section 4.3.2 of my PhD thesis covers this algorithm.
Idea
This checkers tries to find out whether a specification has "finite response". Finite response assures that always only a finite number of controllable events can be executed, then a state must be reached where only uncontrollable (or none) events are enabled. This property is useful when we want to generate PLC code, as it protects from infinite "event loops". The idea of the PLC code is that the environment generates some uncontrollable event and the supervisory controller reacts by executing some of its controllable events. Then it waits for the plant to generate a new uncontrollable event. When an infite number of controllable events can be executed, the supervisory controller will never stop its response (we protect from this is the generated PLC code by killing the loop, but most often the loop continues in the next PLC cycle).
This example does have finite response, as we can always generate at most one controllable event.
How does the checker work?
We find strongly connected locations (via controllable events) in automata, using Tarjan's strongly connected components algorithm (Class EventLoopSearch). From the strongly connected components, we derive the (local) controllable event loops.
Then we try to "prove" that these local controllable event loops cannot be event loops in the specification (global). We do this based on the linearized guard.
In the example, we can see that Motor.c_on needs Button.Pushed and Motor.c_off needs Button.Released. We can derive that the value of Button can only be changed by transitions with uncontrollable events (We call these Σc-independent variables). Thus, (Motor.c_on, Motor.c_off) cannot be a controllable event loop. These checks we do with multi-valued decision diagrams (MDDs).
I think that what we do is:
Find the local controllable loops.
Compute linearized guard per event (per loop).
Convert linearized guard to MDD per event.
Abstract from non-Σc-independent variables, per MDD.
Compute the "and" of all abstracted MDD's per loop.
If the result is "false", then the local controllable loop is not a global loop.
There are some additional properties that say that if a controllable event is in the alphabet of an automaton, but not in any of the local controllable loops of that automaton, that event cannot be in any global controllable loop. Once we conclude that, we can handle that event as if it were uncontrollable.
How good is the checker?
If the checkers says we have finite response that is always true. If the checker says we do not have finite response, then it might be wrong. E.g., the controllable event loop can be unreachable. If we can compute the state-space as a single automaton, the checker is always 100% correct.
For models that follow a sensor/actuator structure with many state/event condition requirements, this checker works particularly well.
This morning I opened the branch again, and apparently I forgot to fix the finite response checker.
(I added that first, found it needs the multi-value things, so added that as well, but didn't go back to the checker to fix paths etc.)
If someone wants to fix that, it's fine. Otherwise I will do that after adding the confluence check.
EDIT: On second look, it looks so broken that it's not much use to try fixing code I think, lots of missing parts.
I had a quick look, it shows a lot of errors but almost all of these are easy to fix. Shouldn't be that much work. I can do that, but I don't know when I have time for it.
Don't forget the command line scripts. And the CIF tool documentation for the new tool.
I'll let you two work on this merge request first. I'll review it once you two think it is ready. We can do that as part of %v0.3, so there is no hurry.
I removed [WIP] from the issue title. That is for merge requests that are not yet finished. For issues that are not closed but have an assignee, the status is implicitly in progress.