Bounded response check

The controller properties checker can check a supervisor for having bounded response.

The bounded response property holds if for each execution of the code, the number of iterations of the event loops to execute for uncontrollable and controllable events are both bounded. This property ensures that the code that executes the uncontrollable events, as well as the code that executes the controllable events, always terminate. That is, the system has no loops with only uncontrollable events, or with only controllable events. In other words, there is no livelock for uncontrollable events, nor for controllable events.

If bounded response doesn’t hold, additional information is printed to the console:

Examples

The check verifies lack of transition loops that consist of only uncontrollable or only controllable events. For example, the Actuator automaton in the example below has bounded response, because between transitions for events c_on and c_off, the location of Sensor has to change via an uncontrollable event. The Sensor automaton does not have bounded response, as the sensor can keep go on and off forever, without restrictions.

plant Actuator:
  controllable c_on, c_off;

  location Off:
    initial;
    edge c_on when Sensor.On goto On;
  location On:
    edge c_off when Sensor.Off goto Off;
end

plant Sensor:
  uncontrollable u_on, u_off;

  location Off:
    initial;
    edge u_on goto On;
  location On:
    edge u_off goto Off;
end

The model below also does not have bounded response. Whenever StartButton and StopButton are both equal to true, the motor keeps starting and stopping.

input bool StartButton, StopButton;

plant Motor:
  controllable c_on, c_off;

  location Off:
    initial;
    edge c_on when StartButton goto On;
  location On:
    edge c_off when StopButton goto Off;
end

Implementation details

The computation of bounded response takes into account the execution scheme. Bounded response for a model is computed as follows:

  1. If there are no initial states, the bounds are both trivially zero.

  2. Otherwise, we compute the possible start states for the uncontrollable and controllable event loops.

  3. Then we compute for each event loop its bound, using its possible start states as input.

The possible start states that we can be in before the uncontrollable and controllable event loops are computed as follows:

  1. We have three event loops, one for the input variable events (which can change before the 'program code' is executed), the uncontrollable events, and the controllable events. We initialize the states we can be in at the start of the input variables events loop to the initial states of the system. We initialize the states we can be in at the start of the uncontrollable and controllable event loops to false.

  2. We execute as many rounds as needed to reach a fixed point for the three types of start states, by in each round executing the 'program code' once:

    1. In a round, we first do an event loop for the input variable events, starting from the currently known possible start states for that loop. This allows input variables to change value. The result of executing that loop are the new possible states that the uncontrollable events loop can start in.

    2. We then similarly perform an event loop for the uncontrollable events, from its known possible start states. We then update the start states of the controllable events loop based on the states we can be in at the end of the uncontrollable events loop.

    3. We then similarly perform an event loop for the controllable events, from its known possible start states. We then update the start states of the input variable events loop based on the states we can be in at the end of the controllable events loop.

The end states we can be in after executing a single full event loop from given start states, are computed as follows:

  • The algorithm is similar to that of computing the bound (see below), but with a small difference. Besides tracking which states we can currently be in, at each point of the execution, we also track the states we can be in at the ends of different iterations. This is required due the possibility of having cycles in the event sequences of the specification.

    If for example in one iteration a variable x is inverted from true to false, and in the next iteration it is inverted again from false to true, then each iteration ends in different states than the previous one. We thus can’t determine a fixed point that way.

    This is not a problem when computing the bound, as then we know that every state in the cycle is present, and thus they all go to the next state in the cycle, and we still get a fixed point. But here, we are computing the loop start states, so we don’t have them yet, and we thus can’t rely on them yet.

    Here, we therefore compute all possible end states of all iterations of the loop, and detect a fixed point for that. This fixed point will be reached, since we can’t forever reach new end states for next iterations.

    Note that we use the 'all iterations end states' to detect the fixed point, but still we return only the end states we reached after the last iteration as the result of this computation.

The end states we can be in after after executing a single iteration of an event loop from given start states, are computed as follows:

  • To match the execution scheme, we try each event in the prescribed order, and execute at most one transition for it per iteration.

  • The states in which an event can start, are:

    • For the first event: the given start states.

    • For all other events: the states in which the previous event could end.

  • To take an edge for an event, we consider the states we can be in before taking the edge. We compute the states in which we can end up by taking the edge. We also consider the states we can remain in, if the guard of the edge is not enabled. We combine them, to get the states after possibly taking a transition for the edge. We then continue with the next edge for the same event, but only from the states in which the previous edges for that same event were not enabled. The result of possibly applying at most one transition for the event is the combination of all the possible target states in which we can end up by applying the different edges (for different source states), and the states in which we may remain because none of the guards of the edges for the event is enabled.

The bound for an event loop, given the possible start states for that event loop, is computed as follows:

  • We start with all states we can be in before the event loop, to account for execution starting in any of those states.

  • If there are no events, the bounds are trivially zero. Otherwise, the current states are those states where we can be after applying zero transitions from the start of the execution (bound zero).

  • We find the bound by in each iteration taking at most one transition for the relevant events. In each iteration, we thus try to take a transition per event, and we end up with the states we can be in after that iteration.

  • If the specification has bounded response, all sequences are of finite length, and at some point they end. That is, after enough iterations, given the length of the sequence and the transition execution order, no more transitions can be executed for the events. If in iteration n no more transitions can be executed, then the possible states we can be in before and after that iteration are the same, and we have reached a fixed point. Since no transitions were executed in iteration n, n - 1 iterations is then enough, and the bound is thus n - 1.

  • If the specification does not have bounded response (assuming the execution scheme), then there is at least one cycle of states. The states within a cycle will with one transition go to the next state in their cycle. Cycles are thus preserved with each iteration. If all bounded sequences at some point end, then only the cycles (there could be more of them) remain. Then a fixed point is reached, but since transitions can still be executed, there is no bounded response.