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)].