Controller property checker

> >

The controller property checker application can be used to determine if a supervisor to be implemented as a controller satisfies finite response. Finite response assures that there are no loops consisting of controllable events, i.e., there is no livelock for controllable events. The assumption is that uncontrollable events are generated by the environment and the controller reacts to these with controllable events. If the controller has finite response, the controller will only generate a finite number of controllable events, before it waits for new (uncontrollable) events from the environment.

The algorithm for finite response is 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.
Print control loops: If set, the events that may still occur in a controllable-event loop are printed to the console.

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 the check is 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.

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

A model has finite response if there do not exist 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

This 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

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 finite response check silently discards any such behavior.

When PLC code is generated for models with runtime errors, finite response 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