Controller property checker

> >

The controller property checker application can be used to determine whether a supervisor to be implemented as a controller satisfies the finite response and confluence properties. For both properties the assumption is that uncontrollable events are generated by the environment and the controller reacts to these by taking as many edges with controllable events as it can. It eventually runs out of edges with controllable events and waits again for receiving more uncontrollable events from the environment.

The finite response property assures that the controller does in fact always run out of edges with controllable events. That is, the system has no loops with only controllable events, there is no livelock for controllable events. The confluence property assures that all choices between edges with controllable events eventually always lead to the same state without enabled edges with a controllable event. It does not matter which edge with a controllable event you choose, you eventually always arrive at the same state.

Both algorithms are based on [Reijnen et al. (2019)].

Starting the checker

The checker can be started in the following ways:

In Eclipse, right click a .cif file in the Project Explorer tab or Package Explorer tab and choose CIF simulation, validation and verification tools Apply controller checks….
In Eclipse, right click an open text editor for a .cif file and choose CIF simulation, validation and verification tools Apply controller checks….
Use the cifcontrollercheck tool in a ToolDef script. See the scripting documentation and tools overview page for details.
Use the cifcontrollercheck command line tool.

Options

Besides the general application options, this application has the following options:

Input file path: The absolute or relative file system path to the input CIF specification.
Enable finite response checking: If set (the default), finite response is checked in the CIF specification. If unset, finite response checking is not performed.
Print control loops: If set (the default), during finite response checking the events that may still occur in a controllable-event loop are printed to the console.
Enable confluence checking: If set (the default), confluence is checked in the CIF specification. If unset, confluence checking is not performed.

At least one of the checks must be enabled.

Supported specifications

The CIF controller property checker supports a subset of CIF specifications. The following restrictions apply:

Channels (events with data types) are not supported.
Continuous variables are not supported.
State invariants are not supported, unless they are trivially true.
Functions are not supported.
Events not declared as controllable or uncontrollable are not supported. This includes the tau event, both explicitly used on edges, as well as implicitly for edges without explicitly mentioned events.
Multi-assignments on edges (such as do (x, y) := (1, 2)) are not supported. However, it is allowed to use multiple assignments on an edge (such as do x := 1, y := 2).
Only discrete/input variables with a boolean, ranged integer (e.g. int[0..5]), or enumeration type are supported.
Only the following expressions are supported: boolean literal values (true and false), integer literal values, enumeration literal values, binary expressions (partially, see below), unary expressions (partially, see below), casts that don’t change the type, if expressions, switch expressions, and references to constants, discrete variables, input variables, algebraic variables, and locations.
Only the following binary operators are supported: logical equivalence (<=>), logical implication (=>), logical conjunction (and on boolean operands), logical disjunction (or on boolean operands), addition (+) on integer operands, subtraction (-) on integer operands, multiplication (*) on integer operands, integer division (div), integer modulus (mod), equality (=) on integer, integer or enumeration operands, inequality (!=) on boolean, integer or enumeration operands, less than (<) on integer operands, less than or equal to (<=) on integer operands, greater than (>) on integer operands, and greater than or equal to (>=) on integer operands.
Only the following unary operators are supported: logical inverse (not), negation (-) on an integer operand, and plus (+) on an integer operand.
Automata with non-determinism for controllable events are not supported. That is, automata that have locations with multiple outgoing edges for the same controllable event, with overlapping guards (e.g. x > 1 and x < 4), are not supported. Note that this check may lead to false positives, as checks are an over-approximation and guard overlap may be detected for unreachable states.
I/O declarations are ignored. A warning is printed if a CIF/SVG input declaration is encountered.
Annotations are ignored.

Preprocessing

The following CIF to CIF transformations are applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be checked:

Finite response

The finite response property of a model ensures that the controller will always perform a finite number of steps to reach a decision. A controller with finite response cannot loop around and perform edges forever, it always blocks after some maximum number of steps and sends new control commands to the system it controls.

The algorithm implementing the check verifies lack of event loops that consist of only controllable events. For example, the automaton in the example below has finite-response, because between event c_on and c_off, the location of Sensor has to change via an uncontrollable event.

automaton 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

automaton 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 does not have finite response. Whenever StartButton and StopButton are both equal to true, the motor keeps starting and stopping.

input bool StartButton, StopButton;

automaton 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

Finite response for a model is determined as follows.

Find controllable-event loops in automata. For this, guards and updates are omitted, also see false negatives.
Find variables that are never updated by controllable events. This includes by definition all input variables.
For all events in a controllable-event loop, determine whether the guards are mutually exclusive. For this, only the variables found in step 2 are considered. For the guards, all other edge guards and state/event exclusion conditions are included.
If there are events in the alphabet of an automaton, but not in any of its controllable-event loops, this event is removed from the set of controllable events.
If the set of controllable events changed, repeat the process.
If the set of controllable events is empty, the model has finite response. Otherwise, it can not be concluded there is finite response. Note that the check is an over-approximation, and there may be false negatives.

False negatives

The finite response check is an over-approximation of the existence of controllable event-loops. As a result, the check might indicate that the specification may not have finite response, while in reality it has finite response. When the check indicates that there is finite response, this is always correct.

To avoid false negatives, use the CIF explorer to compute the untimed statespace.

False negatives may be reported in the following situations:

Loops exist in the non-reachable part of the statespace.
Edges contain guards or updates.

While determining loops in the automata, only explicit loops are considered. That is, the algorithm omits guards and updates of the variables. For that reason, in the example below, c_on and c_off are two independent loops (instead of c_on, c_off if the guards and update were included). To reduce the number of false negatives, it is advised to use locations instead of variables whenever possible or eliminate the variables using the CIF explorer before performing the check.

automaton Actuator:
  controllable c_on, c_off;
  disc bool on = false;
  location:
    initial;
    edge c_on  when not on do on := true;
    edge c_off when     on do on := false;
end

Confluence

The confluence property of a model says that a computed decision is always the same, no matter how you computed it. While computing a response, a model may have several different edges enabled at the same time. A controller then has a choice which edge to perform first. With the confluence property, the controller may make any choice between edges that it desires, but the reached decision is always the same.

The check verifies that for every state in the model with several edges enabled at the same time, any taken edge will lead to the same decision.

The Actuator automaton below has two different edges with controllable events from the same location, but only one of them can be enabled at the same time since the Sensor automaton cannot be in two locations at the same time. As a result, the automaton does not need to choose between edges and the model is confluent.

automaton Actuator:
  controllable events c_a, c_b;
  disc bool on = false;

  location A:
    initial;
    edge c_a when Sensor.On do on := true;
    edge c_b when Sensor.Off do on := false;
end

automaton Sensor:
  uncontrollable u_on, u_off;

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

Note that the confluence property can only hold for models with finite response. The controller must first always reach a decision before you can consider uniqueness of it.

Implementation details

Confluence is determined by checking that for all edge pairs with different controllable events, one of the following cases holds:

Mutual exclusiveness

If the edge with the first event is never enabled at the same time as the edge with the second event, this case applies. Only one of the edges can be taken at any time, there is never a choice between the edges.

edge a when x = 10 goto ...;

edge b when x = 12 goto ...;

The guard holds for at most one of the edges, it is impossible to pick a 'wrong' edge. This case also applies if the edges start from different locations in the same automaton.

Update equivalence

The edge with the first event is enabled at the same time as the edge with the second event, but they both change the system state in the same way.

edge a do x := 5 goto P;

edge b do x := 5 goto P;

As either event has the same effect, which edge is taken does not matter.

Independence

The edge with the first event leads to a state with an edge with the second event and vice versa. Both sequences make the same changes.

  edge a do x := 5 goto P;

  edge b do y := 7 goto Q;

location P:
  edge b do y := 7 goto R;
location Q:
  edge a do x := 5 goto R;

While first taking the a edge leads to a different state than first taking the b edge, they converge again after the next edge.

Skippable

The edge with the second event may be taken, but its change is overridden.

  edge a do x := 6 goto Q;

  edge b do x := 1 goto P;

location P:
  edge a do x := 6 goto Q;

The edge with event b temporarily changes x and jumps to a different location, but there an edge with the a event can be taken and it overwrites all changes made by the b edge.

Reversible

A pair of unrelated events may or may not occur.

location P:
  edge a goto Q;

automaton Z:
  location A:
    edge b when P goto B;
  location B:
    edge c when Q goto A;

Here the choice between events a and b matters, since taking the edge with event a disables event b. However, if the edge with event b is taken first, then after event a, a third event c reverts the change made by the edge with event b. Therefore it does not matter whether events b and c are taken, since they cancel each other out.

If a match can be found for all pairs, the checker concludes that the confluence property holds. Otherwise, it says that a proof of the confluence property could not be found. As the check is an over-approximation, there may be false negatives (the property holds but that could not be proven due to limitations in the checks).

False negatives

The confluence check is an over-approximation of edges for controllable event pairs. As a result, the check might indicate that the specification may not be confluent, while in reality it is confluent. When the check indicates that there is confluence, this is always correct.

False negatives may be reported in the following situations:

Checked edge pairs may be in the non-reachable part of the state space.
The system continues to behave in the same way after diverging.
Not all edges of an event pair match with the same case.
Guard conditions or assigned values have no effect if you take the reachable state space into account.

By using the CIF explorer before performing the check some of the above causes are eliminated.

Runtime errors

The model is assumed not to contain runtime errors, such as division by zero, modulus of zero, or assigning out of bounds values. The checker silently discards any such behavior.

When PLC code is generated for models with runtime errors, the properties cannot be guaranteed as the resulting code may not behave as the CIF specification (see generated code).

One way to get a model without runtime errors is to use supervisor synthesis, since that removes such behavior from its input. For more information, see the data-based and event-based supervisor synthesis tools. Alternatively, the CIF explorer may be used to verify that the specification does not contain runtime errors.

References

[Reijnen et al. (2019)] Ferdie F.H. Reijnen, Albert T. Hofkamp, Joanna M. van de Mortel-Fronczak, Michel A. Reniers and Jacobus E. Rooda, "Finite Response and Confluence of State-based Supervisory Controllers", In: Proceedings of the 15th International Conference on Automation Science and Engineering, pages 509-516, 2019, doi:10.1109/COASE.2019.8843335