The transformation can be started in the following ways:

Besides the general application options, this application several other options.

The following options are part of the Synthesis category:

Internally during synthesis, predicates are represented using Binary Decision Diagrams (BDDs). There are various options that can influence the use of BDDs. The following options are part of the BDD sub-category of the Synthesis category:

The data-based supervisory controller synthesis tool supports a subset of CIF specifications. The following restrictions apply:

Only limited forms of predicates (for markers, invariants, initialization, guards, etc) are supported. The supported predicates are:

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:

Here are some examples of computations that can be statically evaluated:

Here are some examples of computations that can not be statically evaluated:

Only limited forms of assignments are supported. The supported assignments are:

For the following constraints:

Additionally, the tool warns about state/event exclusion invariants for events that are not in the alphabet of any automaton. Such invariants have no effect, as they try to (further) restrict events that are never enabled to begin with.

The following CIF to CIF transformations are applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be synthesized:

Additionally, the CIF specification is converted to an internal representation on which the synthesis is performed. This conversion also applies linearization (product variant) to the edges. Predicates are represented internally using Binary Decision Diagrams (BDDs).

Three types of requirements are supported: state invariants, state/event exclusion invariants, and requirement automata. For state invariants and state/event exclusion invariants, both named and nameless variants are supported.

State invariants are global conditions over the values of variables (and locations of automata) that must always hold. Such requirements are sometimes also called mutual state exclusions. Here are some examples:

State/event exclusion invariants or simply state/event exclusions are additional conditions under which transitions may take place for certain events. Here are some examples:

Requirement automata are simply automata marked as requirement. They usually introduce additional state by using multiple locations or a variable. The additional state is used to be able to express the requirement. One common example is a counter. For instance, consider the following requirement, which prevents more than three products being added to a buffer:

Another common example is a requirement that introduces ordering. For instance, consider the following requirement, which states that motor1 must always be turned on before motor2 is turned on, and they must always be turned off in the opposite order:

Besides the explicit requirements, synthesis also prevents runtime errors. This includes enforcing that integer variables stay within their range of allowed values. This is essentially an implicit requirement. For instance, for a CIF specification with a variable x of type int[0..5] and a variable y of type int[1..3], requirement invariant 0 <= x and x <= 5 and 1 <= y and y <= 3 is implicitly added and enforced by the synthesis algorithm. In the resulting controlled system, no runtime errors due to variables being assigned values outside their domain (integer value range) occur.

If the supervisor has to restrict so much of the behavior of the uncontrolled system that no initial state remains, the controlled system becomes empty. The synthesis algorithm then ends with an empty supervisor error, and no output CIF file is created.

If an initial state remains after synthesis, an output CIF file is created. The contents is the controlled system. The controlled system is obtained by taking the input specification, and modifying it. The requirement automata are changed to supervisor automata. Some or all of the requirement invariants may be removed, depending on the simplifications that are applied. The remaining requirement invariants are changed to supervisor invariants. An additional external supervisor automaton is added. Also, depending on the simplifications that are applied, the requirement automata may serve as monitors or observers for the external supervisor, or may actually impose the requirement restrictions. An external supervisor is a supervisor automaton that adds restrictions to the uncontrolled system (the plants), and potentially the requirement automata, depending on the simplifications that are applied. The supervisor uses the same events as the plants, and refers to plant and requirement locations and variables in its conditions.

By default, the resulting external supervisor automaton is put in the empty namespace, at the top level of the resulting specification. That is, the supervisor automaton is not put in any groups. See the Namespace section for more information.

By default, the added supervisor automaton is named sup. Using the Supervisor name option (see options section above), it is possible to specify a different name. Custom supervisor automaton names must be valid CIF identifiers, i.e. they may consist of letters, digits, and underscores (_), but may not start with a digit. If the resulting supervisor automaton has a name that conflicts with an existing declaration, it is automatically renamed to have a non-conflicting name. In such cases, a warning is printed to the console to inform the user.

The resulting supervisor has exactly one self loop edge for each of the controllable events in the alphabet of the controlled system (which is equal to the alphabet of the uncontrolled system). These self loops represent the possible conditions under which the supervisor allows the events to occur in the controlled system. The exact predicates may vary, depending on the simplifications that are applied.

If there are controllable events that are never enabled in the controlled system, a warning is printed to the console. Enabling forward reachability ensures that warnings are also printed for events that are only enabled in the unreachable part of the statespace. Disabling forward reachability may lead to false negatives, i.e. such cases may not be reported.

The resulting supervisor may have an initialization predicate that restricts the states in which the system may be initialized (may start), on top of the initialization constraints already present in the uncontrolled system. For more information on this initialization predicate, see the section on initialization below.

The synthesis algorithm ensures that in the controlled system, the state requirement invariants hold in all reachable states. It also ensures that in the controlled system, for all transitions from reachable states, the events only occur if the requirement automata and state/event exclusion invariants allow them.

The synthesis algorithm does not restrict any uncontrollable events. Instead, such restrictions are propagated backwards to the source state of the edge with the uncontrollable event, and from there to the transitions that lead to the source state, etc. They are propagated backwards until an edge with a controllable event is encountered (for which the guard can be restricted) or the initial state is reached (and the initialization predicate can be restricted).

If a variable in the uncontrolled system has a single initial value, and the initialization predicate is restricted to not allow this initial value, initialization will be impossible, causing an empty supervisor error. For discrete variables with multiple potential initial values, the synthesis algorithm may restrict initialization to disallow certain initial values, while still leaving possibilities for initialization. For discrete variables declared to initially have an arbitrary initial value, as well as for input variables, the synthesis algorithm essentially determines under which conditions the system can be started, and still exhibits only safe, non-blocking behavior.

If the controlled system requires more strict initialization than the uncontrolled system, an additional initialization predicate is added to the resulting supervisor. The exact predicate may differ, depending on the simplifications that are applied.

Synthesis essentially works by calculations that involve predicates that partition the entire state space into states that satisfy a property or don’t satisfy a property. For instance, a marker predicate may indicate which states of the state space are marked. All other states are thus not marked.

Calculations during synthesis often involve reachability. For instance, from which states is it possible to reach a marker state? To compute the states that can reach a marker state, the marker predicate of the input specification is used. The marker predicate indicates the states that are themselves marked. Then, the states are calculated that can reach one of those marked states, via a single transition. They are put together, to form the states that are marked or can be marked after one transition. By taking another such step, we can add the states that can reach a marked state via two transitions. We then have all states that can reach a marked state via zero, one, or two transitions. We can repeat this until no new states are found, which is called reaching a fixed point.

This form of reachability is called backward reachability, as it starts with some target (e.g. marked states), and goes backwards to find all states from which the target can be reached. Backward reachability can lead to states that could never be reached from an initial state, even in the uncontrolled system. This leads to two separate issues.

The first issue is about unintuitive resulting supervisor guards. The resulting supervisor forbids certain transitions, by restricting controllable events. It among others forbids transitions that end up in states from which no marked state can be reached. However, if those forbidden states can never be reached from an initial state, there is no reason to restrict the controllable events in such cases. The guards of the resulting supervisor then appear to restrict the controllable events, while in fact the guard doesn’t impose a restriction for the controlled system. The supervisor simply doesn’t have the necessary information to know this.

The second issue is about performance. Expanding unreachable states during backward reachability takes time and costs memory, while it has no useful effect on the resulting controlled system.

The use of forward reachability can be a solution to both problems. Forward reachability starts with the initial states, and adds states reachable via one transitions, then via two transitions, then via three transitions, etc. This is repeated until all reachable states are found.

By combining both forward and backward reachability, the supervisor knows about states that exist in the uncontrolled system (due to forward reachability) and about states that it should forbid (due to backward reachability). This leads to the supervisor only restricting transitions that are strictly necessary. However, both when using forward reachability and when not using it, the synthesized supervisor is safe, non-blocking, and maximally permissive. It is only the guards that are more complex than they might need to be, if forward reachability is not used. More complex guards are often less readable, and potentially more expensive to implement in an actual controller.

By combining both forward and backward reachability, parts of the state space that are not relevant may not have to be expanded (as much), which may improve performance. However, computing the forward reachability may also take time and cost memory, thus reducing performance.

It depends on the specification being synthesized whether enabling forward reachability increases or decreases performance. It also depends on the specification whether there is any benefit to using forward reachability for the guards of the supervisor. Forward reachability is disabled by default. It can be enabled using the Forward reachability option (see options section above).

Supervisor synthesis involves many reachability computations to determine which states can be reached from which other states (forward reachability), or which states can reach which other states (backward reachability). This involves repeatedly following edges to find those states, using a fixed point computation.

During reachability computations the edges are considered one by one to find more reachable states. Regardless of whether an edge leads to new states being found or not, the search always continues with the next edge. As long as new states are found, the edges will keep being applied one after the other. After the last edge has been considered, the first edge is considered again, then the second one, etc. Only once all edges have been applied and none of them lead to new states being found has a fixed point been reached and the computation stops.

The order in which the edges are considered for such computations has no effect on the final fixed point result. The order can however significantly influence the performance of supervisor synthesis. For instance, consider that there are dozens of edges and from the already discovered states there is only one edge that leads to more states being found. Then considering that one particular edge first will immediately lead to more states being found. Considering other edges first will lead to wasted computations, as they won’t find any new states.

Besides finding or not finding new states, which new states are found first and in what order may also influence performance. It may lead to smaller or larger intermediate BDD representations of predicates. See the section on the BDD variable order for more information.

Synthesis does not directly use the edges from the model. It applies linearization and then uses the edges from the linearized model. Edges are internally also added to support input variables during synthesis.

The order in which the edges are considered is determined by the Edge order option (see options section above). Several predefined orders exist, and it is also possible to define a custom order. By default, the model ordering is used. The following predefined orders exist:

Furthermore, a custom order can be defined. Custom orders consist of absolute names of events and input variables. That is, for an automaton a, with an event x, the absolute name of the event is a.x. In case edges are labeled with the same event, the edges are ordered based on the linearized model order. The * character can be used as wildcard in those names, and indicates zero or more characters. In case of multiple matches, the matches are sorted alphabetically in ascending order, based on their absolute names.

Multiple names can be separated with , characters. The edges and input variables matching the name pattern before the , are ordered before the edges and input variables matching the name pattern after the ,.

Each name pattern in the order must match at least one event or input variable. An event or input variable may not be included more than once in the order. Every event and input variable needs to be included in the order.

Determining the best edge order is difficult as it can be tricky to predict which edges will lead to finding new states and quickly reaching the fixed point result. When in doubt, use the default value of the option.

The synthesis algorithm computes various predicates, such as the conditions under which the controllable events may take place in the controlled system, and the initialization predicate of the controlled system. These predicates are included in the supervisor that results from synthesis.

However, if the controlled system imposes the exact same restrictions as the uncontrolled system, there is no need to list the full conditions in the supervisor, as the plants already define that behavior. The supervisor imposes no additional restrictions with respect to the plants, and it suffices to use true as condition for the supervisor to make that explicit.

There are several predicates in the synthesis result that can be simplified under the assumption of conditions that are already present in the input specification. In some cases this leads to smaller/simpler supervisor representations. In other cases it gives insight, indicating that the supervisor does not impose any additional restrictions. The following simplifications are available:

Which simplifications should be performed, can be specified using the BDD predicate simplify option (see options section above).

The table above lists in the first column, the option values to use for each of the simplifications, on the command line. The names given in the first column should be combined using commas, and used as option value. The simplifications that are specified using the option replace the default simplifications (see the second column of the table). However, it is also possible to specify additions and removals relative to the default simplifications, by prefixing simplifications (from the first column) with a + or - respectively. Replacements (no prefix) may not be combined with additions/removals (+ or - prefix). Specifying a simplification twice leads to a warning being printed to the console. Adding a simplification that is already present or removing a simplification that is not present, also leads to a warning being printed.

In the option dialog, each of the simplifications can be enabled or disabled using a checkbox.

The second column indicates for each simplification whether it is enabled by default. By default, all simplifications are enabled. The third column indicates the predicate in the synthesis result that can be simplified. The fourth column indicates under the assumption of which predicate the simplification is applied.

The simplification algorithm is not perfect, and may not simplify the predicates as much as could potentially be possible.

When simplifying with respect to state requirement invariants, the supervisor no longer enforces those requirements, as they are assumed to already hold. As such, the simplification prevents such invariants from being removed from the resulting CIF specification. This applies to some of the other simplifications as well. For instance, the simplification over state/event exclusion requirement invariants leads to them being part of the output as well. This may affect whether other tools can handle the resulting supervisor model as input, depending on what kind of features they support. In particular, for code generation, simplification of the guards with respect to the state requirement invariants may need to be disabled.

By default, the synthesis algorithm shows no progress information, and does not explain how the resulting supervisor is obtained. By enabling debug output, detailed information is printed to the console. Debug output can be enabled by setting the Output mode option (General category) to Debug.

The debug output also contains information about the number of states in the resulting controlled system (the uncontrolled system restricted by the synthesized supervisor). If the resulting supervisor (and thus the controlled system) is empty, or if forward reachability is enabled, the number of states that is printed is an exact number (e.g. exactly 0 states, exactly 1 state, exactly 1,234 states). In other situations, the controlled behavior predicate that is used to determine the number potentially gives an over-approximation, and an upper bound on the number of states is printed (e.g. at most 1,234 states).

Enabling debug output may significantly slow down the synthesis algorithm, especially for larger models. The performance degradation stems mostly from the printing of predicates. Predicates are internally represented using Binary Decision Diagrams (BDDs). To print them, they are converted to CNF or DNF predicates, similar to one of the approaches to convert BDDs to CIF predicates for synthesis output.

To limit the performance degradation, options are available to limit the conversion of BDDs to CNF/DNF predicates. The BDD debug max nodes controls the maximum number of BDD nodes for which to convert a BDD to a readable CNF/DNF representation for the debug output. The default is 10 nodes. The maximum must be in the range [1 .. 2³¹ - 1]. The option can be set to have an infinite maximum (no maximum), using option value inf. The BDD debug max paths option controls the maximum number of BDD true paths for which to convert a BDD to a readable CNF/DNF representation for the debug output. The default is 10 paths. The maximum must be in the range [1 .. 1.7e308]. The option can be set to have an infinite maximum (no maximum), using option value inf. If a BDD has more than the specified maximum number of nodes, or more than the specified number of true paths, it is not converted to a CNF/DNF predicate. Instead, it is converted to a textual representation that indicates the number of nodes and true paths, e.g. <bdd 1,234n 5,678p> for a BDD with 1,234 nodes and 5,678 true paths.

By limiting the conversion of BDDs to CNF/DNF predicates, debug output can still be used for large models to see progress information, while not degrading the performance too much.

The data-based synthesis tool supports printing various kinds of statistics. By default, no statistics are printed. Statistics can be enabled using the Statistics option (see options section above). The following statistics are available:

In the option dialog, each of the different kinds of statistics can be enabled and disabled individually, using a checkbox.

From the command line, using the --stats option, the names of the different kinds of statistics, as indicated above between square brackets, should be used, separated by commas. For instance, use --stats=bdd-gc-collect,bdd-gc-resize to enable both BDD garbage collection statistics and BDD node table resize statistics, but keep all other statistics disabled.

Specifying a statistics kind twice leads to a warning being printed to the console.

The synthesis algorithm checks the specification for common issues, for early detection of problems that will lead to an empty supervisor. If such a problem is detected, a warning is printed to the console. Among others, checks are included for no initial states/variables, no marked states, and no states due to the state requirement invariants.

The synthesis algorithm also checks whether there are events that are never enabled in the input specification. If such a problem is detected, a warning is printed to the console. Among others, checks are included for events that are forbidden by automaton guards, event/state exclusion plant and requirement invariants, and state plant invariants.

The synthesis algorithm also checks for plant invariants or plant automata that reference requirement state. If such a problem is detected, a warning is printed to the console. Among others, references in guards, updates, invariant predicates, initialization predicates, marker predicates and initial values for discrete variables are detected.

Internally, predicates are represented using Binary Decision Diagrams (BDDs). CIF variables and automata are represented using one or more boolean variables (also called BDD variables or bits). For instance, a boolean CIF variable is represented using a single boolean/BDD variable, and a CIF variable of type int[0..8] is represented using four boolean/BDD variables (9 possible values, log₂(9) ≈ 3.17). For each automaton with two or more locations, a location pointer variable is created, that represents the current or active location of that automaton. For instance, an automaton with three locations is represented using two boolean/BDD variables. Two boolean/BDD variables can represent 2² = 4 values, so one value is not used.

The CIF variables and location pointer variables for the automata (together called synthesis variables) can be ordered. This ordering can significantly influence the performance of synthesis. Synthesis variables that have a higher influence on the result of predicates (simply put, occur more frequently in predicates) should generally be put earlier in the ordering. Furthermore, in general, strongly related synthesis variables (e.g. by comparison, integer computation, or assignment) should be kept closely together in the order. For two synthesis variables x and y, examples of predicates that introduce relations are x = y (by comparison) and 5 < x + y (by integer computation), and examples of assignments that introduce relations are x := y and x := y + 1 (both by assignment).

For the initial variable ordering, it is possible to order the BDD variables per synthesis variable, or to interleave the BDD/boolean variables of some synthesis variables. This can significantly influences the performance of synthesis. Generally, strongly related synthesis variables should be interleaved.

For more information on ordering and its influence on performance, see Chapter 3 of [Minato (1996)].

For each CIF variable and location pointer, two synthesis variables are created, one storing the old/current value (before a transition), and one storing the new value (after a transition). For a single CIF variable or location pointer, the old and new synthesis variables are always kept together, and interleaved. The old synthesis variable is also always before the new synthesis variable.

The initial order of the boolean/BDD variables is determined by the BDD variable order option (see options section above). Several predefined orders exist, and it is also possible to define a custom order. By default, the sorted order is used. The following predefined orders exist:

Furthermore, a custom initial order can be defined. Custom orders consist of absolute names of variables and automata. That is, for an automaton a, with a discrete variable x, the absolute name of the variable is a.x. The * character can be used as wildcard in those names, and indicates zero or more characters. In case of multiple matches, the matches are sorted increasingly on their absolute names, and interleaved.

Multiple names can be separated with ; characters. The synthesis variables matching the name pattern before the ; are ordered before the synthesis variables matching the name pattern after the ;. The ; separator does not introduce interleaving. The , separator can be used instead of the ; separator to introduce order but also introduce interleaving.

Each name pattern in the order must match at least one variable or automaton. A variable or automaton may not be included more than once in the order. Every variable and automaton (with two or more locations) needs to be included in the order. It is not possible to specify new variables, as they are always directly after their corresponding old variables, and they are always interleaved.

For instance, consider two automata: a and b, each with three variables of type int[0..3]: x1, x2, and x3. The automata have three locations each, so location pointers are created for them. We thus have six discrete variables: a.x1, a.x2, a.x3, b.x1, b.x2, and b.x3, and two location pointer variables: a and b. Consider the following custom order: b*;a.x3,a.x1;a.x2,a. Pattern b* matches location pointer variable b as well as the three discrete variables of automaton b (b.x1, b.x2, and b.x3). They are ordered in increasing alphabetic order, and are interleaved. Variables a.x3 and a.x1 are also interleaved, with a.x3 before a.x1. Finally, variable a.x2 is ordered before the location pointer for automaton a, and they are interleaved as well. This results in the following initial boolean/BDD variable ordering, with bits whose name ends with + representing bits of new variables rather than current/old variables, and x#0 representing bit zero of variable x:

b#0
b+#0
b.x1#0
b.x1+#0
b.x2#0
b.x2+#0
b.x3#0
b.x3+#0
b#1
b+#1
b.x1#1
b.x1+#1
b.x2#1
b.x2+#1
b.x3#1
b.x3+#1

a.x3#0
a.x3+#0
a.x1#0
a.x1+#0
a.x3#1
a.x3+#1
a.x1#1
a.x1+#1

a.x2#0
a.x2+#0
a#0
a+#0
a.x2#1
a.x2+#1
a#1
a+#1

The default orders are often not optimal performance-wise. Manually specifying a custom order often requires specialist knowledge and can take quite some time. Luckily, there are algorithms that can automatically compute a decent variable order.

The algorithms all take an initial variable ordering, and try to improve it using a fast heuristic. Some algorithms search for a local optimum. A better initial variable ordering may then result in a better final variable ordering (a better local optimum), and may also speed up the automatic variable ordering algorithm itself (reaching an optimum faster). Other algorithms search for a global optimum. However, the algorithms are all based on heuristics. The guarantees that they provide differ, but none of them guarantees that synthesis will actually be quicker. In practice however, they typically do improve synthesis performance, especially for larger and more complex models.

For the initial variable ordering, the CIF variables and location pointers may be arbitrarily interleaved. If an automatic variable ordering algorithm changes the initial order, no synthesis variables are interleaved, except for each old variable with its corresponding new variable.

The automatic variable ordering algorithms are not applied if the CIF model has less than two synthesis variables, as with zero variables there is nothing to order, and with one variable there is only one possible order. They are also not applied if the model has no guards, updates, or other predicates from which to derive relations between the variables. Without such relations, the algorithms lack the required input to search for improved variable orders.

The variable relations serve as input for the algorithms. Different algorithms may use different representations of the variable relations, such as hyper-edges or graph edges. Further information about these representations may be obtained by enabling debug output.

The following variable ordering algorithms are available:

If enabled, the algorithms are applied in the order they are listed above.

One of the main properties of BDDs is that they employ full sharing. That is, if a part of a binary tree needs to be represented more than once, it is stored only once, and reused. This leads to BDDs being represented using directed acyclic graphs, rather than binary trees.

The BDD library uses an operation cache to speed up synthesis. Whenever a certain operation is performed on one or more nodes of a BDD graph, the result is cached. If that same operation is performed again on the same nodes, the cached result is reused, if available. This way, repeated calculations can be prevented for shared sub-graphs.

The operation cache is essential for the performance of the synthesis algorithm. With an infinite cache, the operations are generally linear in the number of nodes used to represent the BDDs on which they are applied. Without caching, the computation time grows exponentially.

Obviously, in practice we can’t have an infinite cache, as a computer only has a finite amount of memory available. We thus need to work with a finite cache. Whenever a new cached operation result doesn’t fit in the cache, an older result is overwritten, and will need to be recomputed if it is needed again.

Increasing the cache size can significantly increase performance for large systems, as a cache that is too small is ineffective, and results in many operations needing to be repeated, that could have otherwise been obtained from the cache. However, a larger than needed cache may also significantly decrease performance, as a cache that is too large may no longer fit within CPU caches, leading to more expensive accesses to the main memory.

The operation cache size can be configured in two ways: as a fixed size that remains the same during the entire synthesis, or a variable cache size that grows in size as the node table grows in size. See the options section above for details.

The following options have an effect on the performance of data-based synthesis:

The first column categorizes the different options a bit, for different kind of options. The second column lists the different options. The third column indicates in which section on this page of the documentation you can find more information about that option. The fourth column indicates the effect of the option. The fifth column indicates what to choose for the option, for best performance, although a trade-off may be involved.

Obviously, the actual model that is used has a large impact as well. More variables often leads to longer synthesis times. However, the predicates that are used may also significantly impact performance.

Try to use state/event exclusion requirement invariants instead of requirement automata with a single location and self loops. Also, try to avoid an event-based modeling style, and use a data-based modeling style instead, if possible.

Data-based synthesis supports input variables. The model itself doesn’t specify which value an input variable has at any given moment. Input variables can thus have any value (as long as it fits within the data type of the variable), and the value can change at any time. Input variables are ideal to model sensors.

To support this for data-based synthesis, the input variable is treated as a discrete variable with an arbitrary initial value. To allow the input variable to arbitrarily change, an uncontrollable event is added (with the same absolute name as the input variable). Also, a single edge is added for that event. The edge is always enabled (guard true, since the input variable can always change value), and the update indicates that it can get any value that it doesn’t currently have (x+ != x for x an input variable, with x the value of the variable before the update, and x+ the value of the variable after the update). Obviously, the value of the input variable is kept within the range of values that is allowed by its data type.

Using synthesis with requirements that restrict the allowed values of an input variable will result in an empty supervisor, as a supervisor can’t prevent the environment from changing the value of the input variable (it would have to restrict the uncontrollable event that is internally added to model value changes of the input variable). A supervisor can however impose additional restrictions on the initial value of an input variable. The supervisor can then only guarantee safe, non-blocking behavior if the system is initialized in accordance with the additional initialization restrictions.