Add bounded response check to CIF controller checker

Problem

The code generators use a while-loop to check for events to execute. To ensure that for instance the PLC is fast enough and that the loop will terminate, it would be nice to know how often this loop is executed. The CIF controller checker can check for finite response, but if there is finite response it does not yet compute the actual bounds for the uncontrollable and controllable events.

Original proposed solution

Conceptually, you search the state space for sequences of controllable events. By keeping track of the ends of these sequences, you can keep appending controllable events until the set of states is invariant. When this happens, the longest sequence is found if the set of states is empty, or finite response is disproved if the set is non-empty. Below, a snippet of Java-code is given, based on the synthesis algorithm, which does this.

Code

    private static void checkControllableSequence(SynthesisAutomaton aut, boolean dbgEnabled) {
        // Build a list of edges for controllable events.
        List<SynthesisEdge> controllableEdges = list();
        for (Entry<Event, List<SynthesisEdge>> entry : aut.eventEdges.entrySet()) {
            if (entry.getKey().getControllable()) {
                controllableEdges.addAll(entry.getValue());
            }
        }

        // Find all reachable states.
        CifDataSynthesisReachability reachability = new CifDataSynthesisReachability(aut, 0, //
                "forward controlled-behavior", "initialization", "controlled-behavior", //
                aut.ctrlBeh, // no restriction
                false, // not bad states = good states
                true, // forward reachability
                true, true, // include all edges
                dbgEnabled);
        BDD sequenceStates = reachability.performReachability(aut.initialCtrl.id());

        // Iterate over the sequence.
        for (int maxSequence = 0;; maxSequence++) {
            dbg("Iteration " + maxSequence);

            // Build the set of states after n + 1 sequential controllable transitions.
            BDD newStates = aut.factory.zero();
            for (SynthesisEdge edge : controllableEdges) {
                // Take a controllable transition to a (new) state.
                edge.preApply(true, null);
                BDD edgeStates = edge.apply(sequenceStates.id(), false, true, null, false);
                edge.postApply(true);
                newStates.orWith(edgeStates);
            }

            // If there are no states remaining, we have found the longest sequence.
            if (newStates.isZero()) {
                dbg("Controlled system has at most %d consecutive controllable events.", maxSequence);
                return;
            }

            // If there is no change, we have found one or more cycles.
            if (newStates.equalsBDD(sequenceStates)) {
                dbg("Controlled system does not have finite response.");
                return;
            }

            // Update end states of the sequence.
            sequenceStates = newStates;

            // Stop if requested.
            if (aut.env.isTerminationRequested()) {
                return;
            }
        }
    }

Original notes/future improvements

Some initial tests show that this computation is feasible, taking up to a few minutes for a random lock model. My tests were done by replacing the main data-based synthesis method (synthesizeFixedPoints) with the method above. This brings with it a lot of irrelevant code, so it might be faster if this is properly implemented.

I tried to get some useful output when the system does not have finite response, to give the designer some input on which events might cause this. However, this method does not find minimal cycles, so it is hard to separate the problematic events from other enabled events.

If used in combination with sequencing, the performance can probably be improved. Because you only care about controllable events within an event loop in the generated code.

Current idea

@jverbakel wrote this PDF, which explains the algorithm in more detail. It is also discussed in the comments of this issue in more detail.

The idea is to add a new 'bounded response' check to the CIF controller checker. If bounded response is present, it will add an annotation with the bounds for the uncontrollable and controllable events to the input model, and write out the modified input model as output. The PLC code generator can then read that annotation and take those parameter values as the bounds of the while loops. Modifying the PLC code generator is done in #816 (closed).

I propose that the annotation be attached to the specification as a whole, and be named controller:properties. It allows us to potentially also add other properties as parameters of this annotation, in case the CIF controller checker gets more of them in the future. The parameters would be uncontrollablesBound and controllablesBound, both of type integer, with only non-negative integer values allowed. So, for instance: @@controller:properties(uncontrollablesBound: 3, controllablesBound: 7).

Steps for first version

Move more parts out of the data-based synthesis tool, for reuse in other plugins such as the controller checker (free BDDs, apply plant invariants). (#269)
Add CIF to CIF transformation to relabel supervisors as plants. (#834 (closed))
Add CifEventUtils.getAlphabet(Specification) method. (#835 (closed))
Some first changes to the controller checker to make room for adding BDD-based checks. (!898 (merged))
Add 'bounded response check' to controller checker. Only checks for bounded response, and computes the bounds. No annotations yet. (!903 (merged))
Add the controller:properties annotation, and add it to the model as output of the CIF controller checker if the specification has bounded response. (!907 (merged))

Potential follow-ups

Finished / no issue yet:

Document that users should not modify the model after applying the controller check, or at least be very careful in doing so, if it is needed to for instance add timers before code generation. (!911 (merged))
Could improve debug output of various checks (use indentation for debug output of each check, consistency in empty lines, consistency in indentation within checks, prevent trailing whitespace by #406 (closed), etc). (#937 (closed))
Could attempt not to relabel supervisors to plants, as now the debug output indicates 'Plant' instead of 'Supervisor' for instance for automata generated for state/event exclusion invariants. Note that we do document that we apply this transformation, but still users could be confused if they read the debug output.
Could consider printing the events of the cycle in the debug output, in case there is no bounded response. Finite response does this as well. While finite response has explicit cycles, so we can indicate how many there are, and which events for the cycle. For bounded response we only know which events exist in any cycle (there could be more cycles, events could occur more times in the same cycle, etc). We can find these events by considering which events could be applied in the last round, when cycles were detected. (!1142 (merged))
Could indicate a state that is part of a cycle. There could be more than one. We can just get the satisfying assignments (or just one) of the fixed-point predicate. We can convert the predicate to a CIF text, and print that, to help users analyze the problem. (!1144 (merged))
Could maybe compute a path to the state with a cycle, using backwards reachability. That way, we could help users to analyze the problem. A problem to be solved is that a reachability computation doesn't give a path, so a new algorithm would be needed.
Could drop the non-determinism constraint for CIF to BDD conversion, since we don't need it for the bounded response check.

Other issues:

Could we maybe check the models for modifications by users, after the controller checks? (#895)
Could we check for runtime errors, rather than giving a wrong result? (#894)
Could allow end users to configure more BDD-related settings for the CIF to BDD conversion, BDD reachability computation, etc. (#1050)

Addresses #892

Edited Nov 19, 2024 by Dennis Hendriks