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 execution scheme for code generated from CIF specifications by code generators. This scheme prescribes, among others, the use of iterations of the event loops and the order in which transitions are executed. All code generators must adhere to this scheme, for the results of the controller properties checker to carry over to implemented controllers.

The following properties can be checked:

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.

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.
Non-blocking under control: The non-blocking 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 non-blocking, 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 non-blocking under control check page.

After performing the checks, the controller properties 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 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 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 non-blocking under control checking: If set (the default), non-blocking under control is checked in the CIF specification. If unset, non-blocking under control checking is not performed.
Maximum number of printed cycle states: The maximum number of printed cycle states to print to the console, in case bounded response doesn’t hold due to cycles. The integer number must be non-negative and at most 2,147,483,637. By default, the limit is 10 printed cycle states. For further details, see the bounded response check documentation.
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.
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 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, the check is an over-approximation 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.
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).
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, confluence and non-blocking 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, for x a discrete or input variable with a boolean type).
- Algebraic boolean variables with supported predicates as their values (x, for x an algebraic variable with a boolean type).
- Boolean constants (x, for x a constant with a boolean type).
- Locations (aut.loc, for aut and automaton and loc 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 bi-conditional (<=>) 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.
- Any other valid CIF predicate (computation) that results in a boolean 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:
  {1} in {1, 2} (result is true)
  
  [false, true][0] (result is false)
  
  c - 1, for a constant c with value 4 (result is 3)
  Here are some examples of computations that can not be statically evaluated:
  v = true for v a discrete variable. The computation results in different values for different values of v.
  
  {v} in {1, 2} for v a discrete variable. The computation results in different values for different values of v.
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 non-negative integer literal/value.
- An enumeration literal/value.
- Discrete and input integer/enumeration variables (x, for x a discrete or input variable with an integer or enumeration type).
- Algebraic integer/enumeration variables with supported expressions as their values (x, for x an algebraic variable with an integer or enumeration type).
- Integer/enumeration constants (x, for x a constant with an integer or enumeration type).
- +i for i a supported integer expression.
- i + j for i and j supported integer expressions.
- i div j and i mod j for i a supported integer expressions, and j 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 non-negative 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:
  2 * 5 (result is 10)
  
  floor(3.14) (result is 3)
  
  c + 1, for a constant c with value 2 (result is 3)
  Here are some examples of computations that can not be statically evaluated:
  v - 1, for v a discrete variable. The computation results in different values for different values of v.
  
  ceil(sqrt(-1.0)), since sqrt of a negative number results in a runtime error upon evaluation.
Only limited forms of assignments are supported.
- The supported forms are:
  xb := p (with xb a boolean variable, and p 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 top-level 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, while x := x + (-2) is not. Assignment x := x - 2 matches xi := ie - ie, with the first ie matching x and the second ie matching 2, both of which are supported integer expressions. Assignment x := x + (-2) matches xi := ie, with the ie matching i + j, and the j then matching -2, which is not a supported integer expression.
  - x := x + 1 - 1 is supported, while x := x - 1 + 1 is not. Assignment x := x + 1 - 1 is parsed as x := (x + 1) - 1, which matches xi := ie - ie. The first ie matches x + 1, which matches i + j, with i matching x and j matching 1, both of which are supported integer expressions. The second ie matches 1, which is also a supported integer expression. Assignment x := x - 1 + 1 is parsed as x := (x - 1) + 1, which matches xi := ie, with ie matching (x - 1) + 1, which matches i + j, with i matching x - 1, which is not a supported integer expression, as the - operator is not at the top level.
  - x := x - (3 - 1) is supported, while x := x - 1 - 1 is not. Assignment x := x - (3 - 1) matches xi := ie - ie, with the first ie matching x, a supported integer expression, and the second ie matching 3 - 1, which can be statically evaluated to 2, and is therefore supported. Assignment x := x - 1 - 1 is parsed as x := (x - 1) - 1, which matches xi := ie - ie, with the first ie matching x - 1, which is not a supported integer expression, as the - operator is not at the top level.
  - x := x + 1 - y and x := x + y - 1 are supported, while x := x - (y - 1) and x := x - (1 - y) are not. The former two assignments are parsed as x := (x + 1) - y and x := (x + y) - 1. They both match xi := 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 finite response check:

Channels (events with data types) are not supported.
Functions (both standard library functions and user-defined 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 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 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:

Eliminate component definition/instantiation

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:

Remove I/O declarations

Any changes they cause are not included in the output model.

The following transformations are applied, in case bounded response or non-blocking under control is checked:

Relabel supervisors as plants

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.

Execution scheme

The controller properties checker assumes a certain execution scheme for code generated from CIF specifications by code generators. This scheme prescribes, among others, the order in which transitions are executed. All code generators must adhere to this scheme, for the results of the controller properties checker to carry over to implemented controllers.

Assumptions

The scheme assumes that the CIF specification has only controllable and uncontrollable events. It thus assumes that the specification has no kindless event. This includes the absence of any tau events, either explicitly on edges or implicitly by the absence of event on edges.

Furthermore, the description of the scheme below assumes that the specification has no component definitions/instantiations. If the specification has them, they must be eliminated using the Eliminate component definition/instantiation CIF to CIF transformation. By always using this transformation, we ensure that all tools eliminate them in the same way.

Code parts

From a CIF specification, code can be generated using code generators. It is assumed that the code is regularly executed, for instance at a fixed or variable time interval. The code execution must be completed before the same code is executed again. For instance, if PLC code is generated, the main program would be executed once per PLC cycle.

The code has three parts, that are executed in order:

The values of the input variables are read from the environment.
Execute transitions:
1. Execute transitions for uncontrollable events in an event loop, to update the state based on the inputs.
2. Execute transitions for controllable events in an event loop, to compute the control response, and update the state to reflect it.
The output variables are written to the environment.

Event loops

To ensure a consistent transition execution order, each event loop is executed in a specific manner:

The events are ordered in some way (see event order below).
For each event, in order, at most one transition is executed per iteration of the loop.
If the event is enabled, one transition is executed for it. If the event is disabled, it is skipped.
After each event, regardless of whether it was enabled and a transition was executed for it, the next event is considered, and so on for all the events of the particular loop.
Once all events have been considered once, if for any of the events a transition was executed, then another iteration of the loop is performed.
The loop is executed as many times as necessary, until no event is enabled anymore. However, a limit may be set and then the loop is executed as most as many times as the limit indicates. For instance, the limit may be derived from the result of the bounded response check.

To ensure consistent execution of transitions for events, the edges that participate must be chosen in a specific manner:

If the event is a channel, the first enabled sender automaton for that channel participates in the transition (see automaton order below).
If the event is a channel, the first enabled receiver automaton for that channel participates in the transition (see automaton order below).
For each participating automaton for the event (sender, receiver, monitor or non-monitor synchronizing automaton), the first enabled edge participates in the transition (see location and edge orders below).
For a monitor automaton for the event, if there is no enabled edge in the current location of the automaton, the automaton is ignored for that transition.

To ensure a consistent transition execution order, various elements of CIF specifications must be considered one-by-one in a specific order:

The events of the specification are sorted (see sorting details below).
The automata of the specification are sorted (see sorting details below).
The location of an automaton must be considered in model order, the order in which they are defined in the automaton.
The edges of a location must be considered in the model order, the order in which they are defined in the location.

Note that the order of the events on an edge, in case an edge has multiple events, does not affect the transition execution order.

For objects of CIF specification that are sorted, the sorting must be done in a specific manner:

The absolute non-escaped names of the objects must be sorted.
Sorting must be based on the ASCII characters of the names.
The names must primarily be sorted case-insensitively, but in case they are the same, they must secondarily be sorted case-sensitively.
The names must be sorted in ascending order, such that for instance button is placed before motor, and thus button is considered before motor.
A prefix must be placed before any longer names of which it is a prefix, such that button is placed before button2.

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 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