## Non-blocking under control check

The controller properties checker can check a supervisor for being non-blocking under control.

The non-blocking under control property holds if a marked state can be reached, with the transitions for uncontrollable events and controllable events executed separately in code generated from the supervisor. This property ensures that the code is still non-blocking, and that the non-blockingness guarantee of synthesis is thus preserved in generated code.

Concretely, the check verifies that for every reachable state, there exists a controllable-complete path. That is, for every reachable state, there exists a path to a marked state, with no controllable events enabled in the last/marked state of the path, and all transitions on the path are either for controllable events, or for uncontrollable ones from states where no controllable events are enabled.

### Examples

Consider the following example model, with a `Supervisor1a` automaton. The non-blocking under control property holds for this model.

All locations are reachable. From locations `Start`, `Done1` and `Done2`, controllable event sequences are possible to marked location `BothDone`, where no controllable event is possible. There is thus a marked location at the end of the controllable-event paths consisting of `c_act1` and `c_act2` events. In location `BothDone`, `u_button_pushed` is enabled and no controllable events can be taken. From that location, `u_button_pushed` can thus be taken, followed by the controllable events.

Note that event `u_button_pushed` is monitored, which means the event is also possible in the other locations. That is ok, since a controllable-complete path must exist, and does for every reachable state. That other uncontrollable events are enabled in locations where controllable events are taken on the controllable-event path, does not invalidate the property. The property only puts requirements on uncontrollable events that are taken as part of a controllable-complete path, as they may only occur from states where no controllable events are enabled.

    supervisor Supervisor1a:
      controllable c_act1, c_act2;
      uncontrollable u_button_pushed;
      monitor u_button_pushed;

      location Start:
        initial;
        edge c_act1 goto Done1;
        edge c_act2 goto Done2;

      location Done1:
        edge c_act2 goto BothDone;

      location Done2:
        edge c_act1 goto BothDone;

      location BothDone:
        marked;
        edge u_button_pushed goto Start;
    end

Now consider a slightly different version of this model, as shown below. Automaton `Supervisor1b` is similar to `Supervisor1a`, but has a different marked location. For `Supervisor1b`, the non-blocking under control property does not hold.

All locations are still reachable. And if `c_act1` is done first, before `c_act2`, the automaton goes through marked location `Done1`. But, if instead `c_act2` is done first, before `c_act1`, the automaton does not go through a marked location. And if every time the choice is made to first do `c_act2` before `c_act1`, then the automaton never goes through a marked location. The automaton is can thus exhibit blocking behavior, depending on the order in which the events are executed in generated code.

The non-blocking under control property does not hold here, since in the only marked location there is a controllable event enabled. The marked location should be at the end of the controllable-events path, not within it.

    supervisor Supervisor1b:
      controllable c_act1, c_act2;
      uncontrollable u_button_pushed;
      monitor u_button_pushed;

      location Start:
        initial;
        edge c_act1 goto Done1;
        edge c_act2 goto Done2;

      location Done1:
        marked;
        edge c_act2 goto BothDone;

      location Done2:
        edge c_act1 goto BothDone;

      location BothDone:
        edge u_button_pushed goto Start;
    end

As another example, consider the `Supervisor2a` automaton below. This model is a simplified version of `Supervisor1a`, where `c_act1` is always done first, before `c_act2`. For this model, the non-blocking under control property also holds.

It still has the marked location at the end of the controllable-event path. Also, the uncontrollable event `u_button_pushed` is still possible from that marked location, where no controllable event is enabled.

    supervisor Supervisor2a:
      controllable c_act1, c_act2;
      uncontrollable u_button_pushed;
      monitor u_button_pushed;

      location Start:
        initial;
        edge c_act1 goto Done1;

      location Done1:
        edge c_act2 goto BothDone;

      location BothDone:
        marked;
        edge u_button_pushed goto Start;
    end

Now consider a slightly different version of this model, as shown below. Compared to `Supervisor2a`, automaton `Supervisor2b` has the additional option to do `u_button_pushed` between `c_act1` and `c_act2`. And only by this additional edge, can it reach a marked location. For `Supervisor2b`, the non-blocking under control property does not hold.

Still, all locations are reachable. But, if first `c_act1` is done, then `c_act2`, and finally `u_button_pusehd`, then it cycles without going through a marked location. A marked location can of course be reached, by doing `u_button_pushed` in location `Done1`. But, in the generated code first all transitions for uncontrollable events are executed, and then the transitions for controllable events. In `Start`, no uncontrollable event is possible. And after doing `c_act1` the code will keep doing transitions for controllable events, opting for `c_act2` rather than `u_button_pushed`. Hence, a marked state can never be reached in the generated code. A marked state can only be reached by doing the uncontrollable event in between controllable events, which is excluded by the execution model of the generated code.

A controllable-complete path may only include an uncontrollable event if from its source state no controllable events are enabled. Uncontrollable event `u_button_pushed` may thus not be included from location `Done1`, as there `c_act2` is enabled. The controllable-complete path can thus never reach the marked location. The non-blocking under control property therefore doesn’t hold in this model.

    supervisor Supervisor2b:
      controllable c_act1, c_act2;
      uncontrollable u_button_pushed;
      monitor u_button_pushed;

      location Start:
        initial;
        edge c_act1 goto Done1;

      location Done1:
        edge c_act2 goto BothDone;
        edge u_button_pushed goto Halt;

      location BothDone:
        edge u_button_pushed goto Start;

      location Halt:
        marked;
    end

### Implementation details

Non-blocking under control for a model is determined as follows:

- Compute predicate gc that indicates in which states a controllable event is enabled in the system. This is computed by taking the disjunction of the guards of the edges labeled with controllable events.

- Compute predicate not gc that indicates in which states no controllable events are enabled in the system. This is computed by taking the inverse of gc.

- Compute the ccp states, the states on controllable-complete paths. This is computed by performing a backwards reachability computation from marked and not gc states. During this reachability computation, for each edge labeled with an uncontrollable event, including edges for allowing input variables to change value, guard and not gc is used instead of its original guard.

- Compute the bad states, the not-ccp states and states that can reach such states. This is computed by performing a backwards reachability computation from not ccp states. Unlike in the previous step, the original guards are used for all edges during this reachability computation.

- The model is non-blocking under control if the initial states are not bad. That is, the model is non-blocking under control check if (initial and bad) = false holds.

This algorithm is based on [Reijnen et al. (2019)].