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 .In Eclipse, right click an open text editor for a
.cif
file and choose .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 controllableevent 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.Multiassignments on edges (such as
do (x, y) := (1, 2)
) are not supported. However, it is allowed to use multiple assignments on an edge (such asdo 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
andfalse
), 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 nondeterminism 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
andx < 4
), are not supported. Note that this check may lead to false positives, as checks are an overapproximation 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
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 finiteresponse, 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 controllableevent 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 controllableevent 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 controllableevent 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 overapproximation, and there may be false negatives.
False negatives
The finite response check is an overapproximation of the existence of controllable eventloops. 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 nonreachable 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 theb
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 changesx
and jumps to a different location, but there an edge with thea
event can be taken and it overwrites all changes made by theb
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
andb
matters, since taking the edge with eventa
disables eventb
. However, if the edge with eventb
is taken first, then after eventa
, a third eventc
reverts the change made by the edge with eventb
. Therefore it does not matter whether eventsb
andc
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 overapproximation, 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 overapproximation 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 nonreachable 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 databased and eventbased 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 MortelFronczak, Michel A. Reniers and Jacobus E. Rooda, "Finite Response and Confluence of Statebased Supervisory Controllers", In: Proceedings of the 15th International Conference on Automation Science and Engineering, pages 509516, 2019, doi:10.1109/COASE.2019.8843335