Data-based synthesis options

> > > >

Besides the general application options, the data-based synthesis tool has several other options.

The following options are part of the Synthesis category:

Input file path: The absolute or relative local file system path to the input CIF specification.
Output file path: The absolute or relative local file system path to the output CIF file. If not specified, defaults to the input file path, where the .cif file extension is removed (if present), and a .ctrlsys.cif file extension is added.
Supervisor name: The name of the resulting supervisor automaton. If not specified, it defaults to sup. For more information, see the section about the resulting supervisor.
Supervisor namespace: The namespace of the resulting supervisor. If not specified, it defaults to the empty namespace. For more information, see the section about namespaces.
Forward reachability: Whether to perform forward reachability during synthesis, or omit it. Is disabled by default. For more information, see the section about forward reachability.
Fixed-point computations order: The order in which the fixed-point computations are to be performed during synthesis. This may impact the performance of synthesis. For more information, see the section about fixed-point computations order.
Exploration strategy: The exploration strategy to use for symbolic reachability computations. This strategy determines in which order the edges are to be considered. This may impact the performance of synthesis. For more information, see the section about edge order.
Edge granularity: Specify the granularity of edges to use during synthesis. For more information, see the section about edge granularity.
Edge order: This option is no longer supported. Use the Edge order for backward reachability and Edge order for forward reachability options instead.
Edge order for backward reachability: Synthesis involves many reachability computations. Some of them involve following edges backward to find reachable states. The order in which the edges are considered for such backward reachability computations is determined by this option. For more information, see the section about edge order.
Edge order for forward reachability: Synthesis involves many reachability computations. Some of them involve following edges forward to find reachable states. The order in which the edges are considered for such forward reachability computations is determined by this option. For more information, see the section about edge order.
Edge order duplicate events: Specify whether duplicate events are allowed for custom edge orders specified using the Edge order for backward reachability and Edge order for forward reachability options. By default, duplicate events are disallowed. For more information, see the section about edge order.
Edge workset algorithm: This option is no longer supported. Use the Exploration strategy option instead.
State requirement invariant enforcement: Specify how state requirement invariants are enforced during synthesis. By default, they are all enforced via the controlled behavior. But, this can also be decided per edge, enforcing them via edge guards for edges with controllable events, and enforcing them via the controlled behavior for edges with uncontrollable events. For more information, see the section on state requirement invariants.
Statistics: The kinds of statistics to print. By default, no statistics are printed. For more information, see the section about statistics.
Continuous performance statistics file: The absolute or relative local file system path to the continuous performance statistics output file. If not specified, defaults to the input file path, where the .cif file extension is removed (if present), and a .stats.txt file extension is added. For more information, see the section about statistics.
Event warning: Whether to warn for events that are never enabled in the input specification or never enabled in the controlled system. Is enabled by default. Disabling this warning may increase the performance of synthesis.
Plants referencing requirements warnings: Whether to warn for plants that reference requirement state. Is enabled by default. Disabling this warning may increase the performance of synthesis.

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:

BDD output mode: This option can be used to control how the BDDs are converted to CIF for the output of synthesis. For more information, see the section about BDD representations of the resulting supervisor.
BDD output name prefix: The prefix to use for BDD related names in the output. Only has an effect if the BDD output mode option is set to represent the internal BDD nodes directly in CIF. The default prefix is bdd. For more information, see the section about BDD representations of the resulting supervisor.
BDD initial variable ordering: CIF variables and automata are represented using one or more boolean variables. The initial order of the boolean variables is determined by this option. For more information, see the section about BDD variable orders and in particular the section about initial variable ordering.
BDD hyper-edge creation algorithm: CIF variables and automata are represented using one or more boolean variables. The initial order can be improved and optimized by various variable ordering algorithms. This option controls how hyper-edges are created, which are used by the variable ordering algorithms. For more information, see the section about BDD variable orders and in particular the section about automatic variable ordering.
BDD DCSH variable ordering algorithm: CIF variables and automata are represented using one or more boolean variables. The initial order of the boolean variables can be improved by enabling this option. For more information, see the section about BDD variable orders and in particular the section about automatic variable ordering.
BDD FORCE variable ordering algorithm: CIF variables and automata are represented using one or more boolean variables. The initial order of the boolean variables can be improved by enabling this option. For more information, see the section about BDD variable orders and in particular the section about automatic variable ordering.
BDD sliding window variable ordering algorithm: CIF variables and automata are represented using one or more boolean variables. The initial order of the boolean variables can be improved by enabling this option. For more information, see the section about BDD variable orders and in particular the section about automatic variable ordering.
BDD sliding window size: The maximum length of the window to use for the BDD sliding window variable ordering algorithm. This option only has effect if the BDD sliding window variable ordering algorithm option is enabled. The size must be an integer number in the range [1 .. 12]. The default size is 4. For more information, see the section about BDD variable orders and in particular the section about automatic variable ordering.
BDD advanced variable ordering: CIF variables and automata are represented using one or more boolean variables. The variable ordering can be configured most flexibly using this option. For more information, see the section about BDD variable orders and in particular the section about advanced variable ordering configuration.
BDD predicate simplify: Several BDD predicates may be simplified under the assumption of other predicates, resulting in smaller/simpler output. This may decrease the size of the resulting controller, and may give more insight. For more information, see the section about predicate simplification.
BDD library initial node table size: The BDD library that is used maintains an internal node table. This option can be used to set the initial size of that node table. The size will automatically be increased during synthesis, if necessary. Increasing the initial size can increase performance for large systems, as it will not be necessary to repeatedly increase the size of the node table. However, a larger node table requires more memory, and can lead to the node table no longer fitting within CPU caches, degrading performance. The default is 100000 nodes. The initial node table size must be in the range [1 .. 2³¹ - 1]. For more information, see the section about statistics.

BDD library operation cache size: The BDD library that is used maintains several internal operation caches. This option can be used to set the fixed size of these caches. The operation cache size must be in the range [2 .. 2³¹ - 1]. By default, this option is disabled (value off on the command line), and the BDD library operation cache ratio option is used instead. For more information, see the section about BDD operation caches.

BDD library operation cache ratio: The BDD library that is used maintains several internal operation caches. This option can be used to set the ratio of the size of the operation caches of the BDD library to the size of the node table of the BDD library. For instance, a ratio of 0.1 means that the sizes of the operation caches are 10% of the size of the node table. The operation cache ratio must be in the range [0.01 .. 1000]. The default ratio is 1.0. This option has no effect if the BDD library operation cache size option is enabled. For more information, see the section about BDD operation caches.
BDD debug max nodes: Internally, predicates are represented using Binary Decision Diagrams (BDDs). This option control 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. For more information, see the section about debug output.
BDD debug max paths: Internally, predicates are represented using Binary Decision Diagrams (BDDs). This option control 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 non-negative. The option can be set to have an infinite maximum (no maximum), using option value inf. For more information, see the section about debug output.