//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2021, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

:leveloffset: -2

[[tools-chapter-controller-checker]]
== Controller properties checker

indexterm:[controller properties checker]
indexterm:[tools,controller properties checker]
The controller properties checker can be used to determine whether a <<sbe-approaches-synthesis-based-supervisor-vs-controller,supervisor>> to be implemented as a <<sbe-approaches-synthesis-based-supervisor-vs-controller,controller>> satisfies certain desired properties.
These properties are not yet guaranteed through <<sbe-approaches-synthesis-synthesis,synthesis>>, and must therefore be checked on a synthesized supervisor, before <<sbe-in-practice-steps-implementation,code is generated>> from it.

The controller properties checker assumes a certain <<tools-controller-checker-execution-scheme,execution scheme>> for code generated from CIF specifications by code generators.
This scheme prescribes, among others, the use of iterations of the <<tools-controller-checker-execution-scheme-event-loops,event loops>> and the order in which <<lang-tut-basics-trans,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:

<<tools-controller-checker-bounded-response,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 <<lang-tut-time-livelock,livelock>> for uncontrollable events, nor for controllable events.
+
This check does not produce false negatives.
+
Read more about this check on the <<tools-controller-checker-bounded-response,bounded response check>> page.

<<tools-controller-checker-confluence,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 the controller can make any choice between controllable events without losing the <<sbe-approaches-synthesis-based-properties,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 <<tools-controller-checker-confluence,confluence check>> page.

<<tools-controller-checker-finite-response,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 <<lang-tut-time-livelock,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 <<tools-controller-checker-finite-response,finite response check>> page.

<<tools-controller-checker-non-blocking-under-control,Non-blocking under control>>::
The non-blocking under control property holds if a <<lang-tut-synthesis-marked,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 <<tools-controller-checker-non-blocking-under-control,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 <<lang-tut-annotations-controller,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.

indexterm:[controller properties checker,start]

=== Starting the checker

The checker can be started in the following ways:

* In Eclipse, right click a `.cif` or `.cifx` file in the _Project Explorer_ tab or _Package Explorer_ tab and choose menu:CIF simulation, validation and verification tools[Apply controller checks...].

* In Eclipse, right click an open text editor for a `.cif` or `.cifx` file and choose menu:CIF simulation, validation and verification tools[Apply controller checks...].

* Use the `cifcontrollercheck` tool in a ToolDef script.
See the <<tools-scripting-chapter-intro,scripting documentation>> and <<tools-scripting-chapter-tools,tools overview>> page for details.

* Use the `cifcontrollercheck` command line tool.

indexterm:[controller properties checker,options]

[[tools-controller-checker-options]]
=== 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,639.
By default, the limit is 10 printed cycle states.
For further details, see the <<tools-controller-checker-bounded-response,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.

indexterm:[controller properties checker,supported specifications]

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

* I/O declarations are ignored.
A warning is printed if a CIF/SVG input declaration is encountered.

* Annotations are ignored.

// *** BDD-based checks. ***
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 supported type:
** Boolean type.
** Ranged integer type (e.g. `int[0..5]`).
   Ranges that allow more than 2,147,483,647 (2^31 - 1) possible values are not supported.
** Enumeration type.
** Tuple type, with supported types for the tuple's fields.

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

* The following restrictions apply to user-defined functions:

** External user-defined functions are not supported.

** Internal user-defined functions with recursive calls are not supported.

** Internal user-defined functions with `while` statements are not supported.

** Internal user-defined functions with assignments that may result in runtime out-of-range errors are not supported.

** Internal user-defined functions may only be used in function calls.
   All other uses are not supported, including using them as data, such as storing them in variables, returning them from functions, and so on.

** Internal user-defined functions may only use supported data types (same as discrete and input variables) as their return and parameter types, and as the types of their local variables.

* 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, on two supported integer or enumeration expressions, or on two supported tuple expressions.

** The binary inequality comparison (`!=`) on two supported predicates, on two supported integer or enumeration expressions, or on two supported tuple 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.

** Function calls to internal user-defined functions with supported arguments that return a boolean value.

** Projections on tuples that result in a boolean value.

** Received values (`?`) with a boolean type.

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

** An 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` and `-i` for `i` a supported integer expression.

** `i + j`, `i - j`, and `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.

** `abs(i)` and `sign(i)` for `i` a supported integer expression.

** `max(i, j)` and `min(i, j)` for `i` and `j` supported integer expressions.

** Conditional expressions (`if` expressions) with supported guard predicates and supported resulting values.

** `Switch` expressions with supported control values and supported resulting values.

** Function calls to internal user-defined functions with supported arguments that return an integer or enumeration value.

** Projections on tuples that result in an integer or enumeration value.

** Received values (`?`) with an integer or enumeration type.

** Any other valid CIF expression (computation) that results in an 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 tuple expressions (for binary comparisons, initial values of variables, right hand sides of assignments, etc) are supported.
  The supported expressions are:

** A tuple literal/value.

** Discrete and input tuple-typed variables (`x`, for `x` a discrete or input variable with a tuple type).

** Algebraic tuple-typed variables with supported expressions as their values (`x`, for `x` an algebraic variable with a tuple type).

** Tuple-typed constants (`x`, for `x` a constant with a tuple type).

** Conditional expressions (`if` expressions) with supported guard predicates and supported resulting tuple-typed values.

** `Switch` expressions with supported control values and supported resulting tuple-typed values.

** Function calls to internal user-defined functions with supported arguments that return a tuple value.

** Projections on tuples that result in a tuple value.

** A received value (`?`) with a tuple type.

** Any other valid CIF expression (computation) that results in a tuple 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.

// *** MDD-based checks. ***
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 (`pass:[+]`) 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.

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

indexterm:[controller properties checker,preprocessing]

=== Preprocessing

To increase the subset of CIF specifications that can be checked, various <<tools-cif2cif-chapter-index,CIF to CIF transformations>> are applied as preprocessing.

The following transformations are applied for the tool in general, regardless of which checks are performed:

* <<tools-cif2cif-chapter-elim-comp-def-inst>>

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:

* <<tools-cif2cif-chapter-remove-io-decls>>

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

// *** BDD-based checks. ***
The following transformations are applied, in case bounded response or non-blocking under control is checked:

* <<tools-cif2cif-chapter-relabel-supervisors-as-plants>>

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

// *** MDD-based checks. ***
The following transformations are applied (in the given order), in case confluence or finite response is checked:

* <<tools-cif2cif-chapter-elim-state-event-excl-invs>>

* <<tools-cif2cif-chapter-elim-monitors>>

* <<tools-cif2cif-chapter-elim-self>>

* <<tools-cif2cif-chapter-elim-type-decls>>

* <<tools-cif2cif-chapter-elim-locs-in-exprs>>

* <<tools-cif2cif-chapter-enums-to-ints>>

* <<tools-cif2cif-chapter-elim-alg-vars>>

* <<tools-cif2cif-chapter-elim-consts>>

* <<tools-cif2cif-chapter-simplify-values>>

* <<tools-cif2cif-chapter-elim-if-updates>>

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

indexterm:[controller properties checker,execution scheme]

[[tools-controller-checker-execution-scheme]]
=== 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 <<tools-cif2cif-chapter-elim-comp-def-inst>> 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 <<lang-tut-basics-trans,transitions>>:
.. Execute transitions for <<sbe-approaches-synthesis-based-events,uncontrollable events>> in an event loop, to update the state based on the inputs.
.. Execute transitions for <<sbe-approaches-synthesis-based-events,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.

[[tools-controller-checker-execution-scheme-event-loops]]
**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 <<tools-controller-checker-bounded-response,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`.

indexterm:[controller properties checker,runtime errors]

[[tools-controller-checker-runtime-errors]]
=== 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 also the <<tools-plcgen-supported-specifications,section about supported specifications>> of the PLC code generator.

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 <<tools-chapter-datasynth,data-based>> and <<tools-eventbased-chapter-supervisorsynthesis,event-based>> supervisor synthesis tools.
Alternatively, the <<tools-chapter-cif-explorer,CIF explorer>> may be used to verify that the specification does not contain runtime errors.

[bibliography]
[[tools-controller-checker-references]]
=== References

* [[[reijnen19,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:link:https://doi.org/10.1109/COASE.2019.8843335[10.1109/COASE.2019.8843335]
