Controller properties checker
The controller properties checker can be used to determine whether a supervisor to be implemented as a controller satisfies certain desired properties. These properties are not yet guaranteed through synthesis, and must therefore be checked on a synthesized supervisor, before code is generated from it.
The controller properties checker assumes a certain structure of code generated by code generators:
Some code for the model is executed, and after a fixed or variable time, the code is executed again, and so on.
Every time the code is executed:
First the external inputs are read.
Then transitions for uncontrollable events are executed to update the state based on the inputs.
Then transitions for controllable events are executed to compute the control response, and update the state to reflect it.
And finally, the external outputs are written.
The controller checker can check the following properties:
 Bounded response

The bounded response property holds if for each execution of the code, the number of transitions 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.
This check does not produce false negatives.
Read more about this check on the bounded response check page.
 Confluence

The confluence property holds if for each execution of the controllable events, it does not matter in which order the controllable events are executed, as the same state is reached regardless. This property ensures that that the controller can make any choice between controllable events without losing the guarantees of synthesis. By extension, this means that code generators may generate code for the controller that executes the controllable events in any order.
This check does not check for confluence of the uncontrollable events. Furthermore, the check may produce false negatives.
Read more about this check on the confluence check page.
 Finite response

The finite response property holds if for each execution of the code, the number of transitions to execute for controllable events is finite. This property ensures that the code that executes the controllable events always terminates. That is, the system has no loops with only controllable events. In other words, there is no livelock for controllable events.
This check does not check for finite response of the uncontrollable events. Furthermore, the check may produce false negatives. Hence, it is recommended to use the bounded response check instead.
Read more about this check on the finite response check page.
 Nonblocking under control

The nonblocking under control property holds if a marked state can be reached, even though the transitions for uncontrollable events and controllable events are executed in a specific way in generated code. This property ensures that the code is still nonblocking, and this guarantee of synthesis is thus preserved in generated code.
This check does not produce false negatives.
Read more about this check on the nonblocking under control check page.
After performing the checks, the controller checker adapts the input model, to encode the results of the checks that were performed in the controller properties annotation of the model. It then writes the modified model to a file. If only some of the checks are performed, the earlier results of checks that are skipped are preserved. This allows the checks to be performed one by one.
After checking whether the properties hold on a model, that model should not be adapted anymore, as this may invalidate the results of the checks. If changes must be made, such as adding timers before generating code, then such changes should be made with great care, as not to invalidate the results of the checks.
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 bounded response checking: If set (the default), bounded response is checked in the CIF specification. If unset, bounded response checking is not performed.
Enable confluence checking: If set (the default), confluence is checked in the CIF specification. If unset, confluence checking is not performed.
Enable finite response checking: If set (the default), finite response is checked in the CIF specification. If unset, finite response checking is not performed.
Enable nonblocking under control checking: If set (the default), nonblocking under control is checked in the CIF specification. If unset, nonblocking under control 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.
Output file: The absolute or relative file system path to the output CIF specification. If not specified, defaults to the input file path, where the
.cif
file extension is removed (if present), and a.checked.cif
file extension is added.
At least one of the checks must be enabled.
Supported specifications
The CIF controller properties checker supports a subset of CIF specifications. The following restrictions apply for the tool in general, regardless of which checks are performed:
Specifications without automata are not supported.
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, the check is an overapproximation and guard overlap may be detected for unreachable states.Only plant and supervisor automata are supported. Kindless and requirement automata are not supported.
Only plant and supervisor invariants are supported. Kindless and requirement invariants are not supported.
State invariants are not supported, unless they are trivially
true
.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.Continuous variables are not supported.
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
).Partial variable assignments on edges (such as
do x[0] := 5
) are not supported.I/O declarations are ignored. A warning is printed if a CIF/SVG input declaration is encountered.
Annotations are ignored.
The following restrictions apply only to the bounded response and nonblocking under control checks:
Discrete and input variables are supported, but only if they have a boolean type, ranged integer type (e.g.
int[0..5]
), or enumeration type. For integer types, ranges that include negative integer values are not supported.Discrete variables must have supported initial values. If explicit initial values are given, they must be supported predicates (for boolean variables) or supported expressions as described below (for all other variables).
Constants, algebraic variables and algebraic parameters of components are supported as long as their values are supported in the context where they are used (as described below).
Conditional updates (
if
updates) are not supported.Only limited forms of predicates (for markers, invariants, initialization, guards, initial values of boolean variables, right hand sides of assignments, etc) are supported. The supported predicates are:
Boolean literals (
true
,false
).Discrete and input boolean variables (
x
, forx
a discrete or input variable with a boolean type).Algebraic boolean variables with supported predicates as their values (
x
, forx
an algebraic variable with a boolean type).Boolean constants (
x
, forx
a constant with a boolean type).Locations (
aut.loc
, foraut
and automaton andloc
a location of that automaton).The unary inverse operator (
not
) on a supported predicate.The binary logical conjunction (
and
) on two supported predicates.The binary logical disjunction (
or
) on two supported predicates.The binary logical implication (
=>
) on two supported predicates.The binary logical biconditional (
<=>
) on two supported predicates.The binary equality comparison (
=
) on two supported predicates, or on two supported integer or enumeration expressions.The binary inequality comparison (
!=
) on two supported predicates, or on two supported integer or enumeration expressions.The binary less than comparison (
<
) on two supported integer expressions.The binary less than or equal comparison (
<=
) on two supported integer expressions.The binary greater than comparison (
>
) on two supported integer expressions.The binary greater than or equal comparison (
>=
) on two supported integer expressions.Conditional expressions (
if
expressions) with supported guard and resulting value predicates.Switch
expressions with supported control value and resulting value predicates.
Only limited forms of integer and enumeration expressions (for binary comparisons, initial values of variables, right hand sides of assignments, etc) are supported. The supported expressions are:
A nonnegative integer literal/value.
An enumeration literal/value.
Discrete and input integer/enumeration variables (
x
, forx
a discrete or input variable with an integer or enumeration type).Algebraic integer/enumeration variables with supported expressions as their values (
x
, forx
an algebraic variable with an integer or enumeration type).Integer/enumeration constants (
x
, forx
a constant with an integer or enumeration type).+i
fori
a supported integer expression.i + j
fori
andj
supported integer expressions.i div j
andi mod j
fori
a supported integer expressions, andj
a positive integer value, or a computation that results in a positive integer value, as long as the computation is not too complex to be performed statically. That is,j
must essentially be constant.Conditional expressions (
if
expressions) with supported guard predicates and supported resulting values.Switch
expressions with supported control values and supported resulting values.Any other valid CIF expression (computation) that results in a nonnegative integer value or an enumeration value, as long as the computation is not too complex to be performed statically. That is, the computation must essentially represent a fixed/constant value.
Here are some examples of computations that can be statically evaluated:
true and false
(result isfalse
)c or false
, for a constantc
with valuefalse
(result isfalse
)1 + 1
(result is2
)2 * 5
(result is10
)floor(3.14)
(result is3
)c + 1
, for a constantc
with value2
(result is3
)
Here are some examples of computations that can not be statically evaluated:
v + 1
, forv
a discrete variable. The computation results in different values for different values ofv
.v = true
forv
a discrete variable. The computation results in different values for different values ofv
.v = e
forv
a discrete variable ande
an enumeration literal/value. The computation results in different values for different values ofv
.
Only limited forms of assignments are supported.
The supported forms are:
xb := p
(withxb
a boolean variable, andp
a supported predicate)xi := ie
xi := ie  ie
xe := ee
For the following constraints:
xb
is a boolean variable.xi
is a supported integer variable, as described above.xe
is an enumeration variable.p
is a supported predicate, as described above.ie
is a supported integer expression, as described above.ee
is a supported enumeration expression, as described above.
What exactly is supported for assignments, expressions and predicates can be subtle:
For instance, subtraction is only supported as the toplevel operator at the right hand side of an assignment, and not anywhere else in expressions.
To see whether an assignment is supported, first match it against the supported forms listed above. Then, for each of the parts of the assignment that are matched against the placeholder variables, check the listed constraints. If a placeholder matches an expression or predicate, recursively check whether the expression or predicate is supported, by matching it against its supported forms, etc.
Slightly rewriting an unsupported form may make it supported. If an assignment, expression or predicate is not supported, changes such as adding parenthesis or swapping the order of operator arguments, could make it supported.
Here as some examples, where variable
x
is a supported discrete variable:x := x  2
is supported, whilex := x + (2)
is not. Assignmentx := x  2
matchesxi := ie  ie
, with the firstie
matchingx
and the secondie
matching2
, both of which are supported integer expressions. Assignmentx := x + (2)
matchesxi := ie
, with theie
matchingi + j
, and thej
then matching2
, which is not a supported integer expression.x := x + 1  1
is supported, whilex := x  1 + 1
is not. Assignmentx := x + 1  1
is parsed asx := (x + 1)  1
, which matchesxi := ie  ie
. The firstie
matchesx + 1
, which matchesi + j
, withi
matchingx
andj
matching1
, both of which are supported integer expressions. The secondie
matches1
, which is also a supported integer expression. Assignmentx := x  1 + 1
is parsed asx := (x  1) + 1
, which matchesxi := ie
, withie
matching(x  1) + 1
, which matchesi + j
, withi
matchingx  1
, which is not a supported integer expression, as the
operator is not at the top level.x := x  (3  1)
is supported, whilex := x  1  1
is not. Assignmentx := x  (3  1)
matchesxi := ie  ie
, with the firstie
matchingx
, a supported integer expression, and the secondie
matching3  1
, which can be statically evaluated to2
, and is therefore supported. Assignmentx := x  1  1
is parsed asx := (x  1)  1
, which matchesxi := ie  ie
, with the firstie
matchingx  1
, which is not a supported integer expression, as the
operator is not at the top level.x := x + 1  y
andx := x + y  1
are supported, whilex := x  (y  1)
andx := x  (1  y)
are not. The former two assignments are parsed asx := (x + 1)  y
andx := (x + y)  1
. They both matchxi := ie  ie
, with the
operator at the top level. The latter two assignments are not supported, as the
operators in(y  1
) and(1  y)
are in those cases not at the top level.
The following restrictions apply only to the confluence and finite response checks:
Channels (events with data types) are not supported.
Functions (both standard library functions and userdefined ones) are not supported.
Only discrete, input and algebraic 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 boolean, 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.
Preprocessing
To increase the subset of CIF specifications that can be checked, various CIF to CIF transformations are applied as preprocessing.
The following transformations are applied for the tool in general, regardless of which checks are performed:
Any changes they cause are included in the output model as well.
The following transformations are applied for the tool in general, regardless of which checks are performed:
Any changes they cause are not included in the output model.
The following transformations are applied, in case bounded response or nonblocking under control is checked:
Any changes they cause are not included in the output model.
The following transformations are applied (in the given order), in case confluence or finite response is checked:
Any changes they cause are not included in the output model.
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. Since the checker silently discards any such behavior, the outcome of the various checks may be incorrect if the model exhibits behavior leading to runtime errors.
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