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:

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.

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

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

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

      • true and false (result is false)

      • c or false, for a constant c with value false (result is false)

      • 1 + 1 (result is 2)

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

      • v = true for v a discrete variable. The computation results in different values for different values of v.

      • v = e for v a discrete variable and e an enumeration literal/value. The computation results in different values for different values of v.

  • 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 confluence and finite response checks:

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

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