//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 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
//////////////////////////////////////////////////////////////////////////////

indexterm:[data-based supervisory controller synthesis,options]

:leveloffset: -2

[[tools-datasynth-options]]
== 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 <<tools-datasynth-supervisor,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 <<tools-datasynth-supervisor-namespace,section about namespaces>>.

* _Forward reachability_: Whether to perform forward reachability during synthesis, or omit it.
Is disabled by default.
For more information, see the <<tools-datasynth-forward-reach,section about forward reachability>>.

* _Fixed-point computations order_: The order in which the different forward/backward reachability fixed-point computations are to be performed during synthesis.
This may impact the performance of synthesis.
For more information, see the <<tools-datasynth-fixed-point-order,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 <<tools-datasynth-edge-order,section about edge order>>.

* _Edge granularity_: Specify the granularity of edges to use during synthesis.
For more information, see the <<tools-datasynth-edge-granularity,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 <<tools-datasynth-edge-order,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 <<tools-datasynth-edge-order,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 <<tools-datasynth-edge-order,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 <<tools-datasynth-state-req-invs,section on state requirement invariants>>.

* _Statistics_: The kinds of statistics to print.
By default, no statistics are printed.
For more information, see the <<tools-datasynth-stats,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 <<tools-datasynth-stats,section about statistics>>.

[[tools-datasynth-options-event-warn]]
* _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.
For more information, see the <<tools-datasynth-early-prob-detect,section about early problem detection>>.

[[tools-datasynth-options-plants-ref-reqs-warn]]
* _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.
For more information, see the <<tools-datasynth-early-prob-detect,section about early problem detection>>.

Internally during synthesis, predicates are represented using link:https://en.wikipedia.org/wiki/Binary_decision_diagram[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 <<tools-datasynth-supervisor-bdd,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 <<tools-datasynth-supervisor-bdd,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 <<tools-datasynth-var-order,section about BDD variable orders>> and in particular the <<tools-datasynth-var-order-initial-ordering,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 <<tools-datasynth-var-order,section about BDD variable orders>> and in particular the <<tools-datasynth-var-order-auto-var-ordering,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 <<tools-datasynth-var-order,section about BDD variable orders>> and in particular the <<tools-datasynth-var-order-auto-var-ordering,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 <<tools-datasynth-var-order,section about BDD variable orders>> and in particular the <<tools-datasynth-var-order-auto-var-ordering,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 <<tools-datasynth-var-order,section about BDD variable orders>> and in particular the <<tools-datasynth-var-order-auto-var-ordering,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 <<tools-datasynth-var-order,section about BDD variable orders>> and in particular the <<tools-datasynth-var-order-auto-var-ordering,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 <<tools-datasynth-var-order,section about BDD variable orders>> and in particular the <<tools-datasynth-var-order-adv-config,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 <<tools-datasynth-simplification,section about predicate simplification>>.

[[tools-datasynth-options-initial-node-table-size]]
* _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 [2 .. 2^31^ - 1].
For more information, see the <<tools-datasynth-stats,section about statistics>>.

[[tools-datasynth-options-cache-size]]
* _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^31^ - 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 <<tools-datasynth-op-cache,section about BDD operation caches>>.

[[tools-datasynth-options-cache-ratio]]
* _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 <<tools-datasynth-op-cache,section about BDD operation caches>>.

* _BDD debug max nodes_: Internally, predicates are represented using link:https://en.wikipedia.org/wiki/Binary_decision_diagram[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^31^ - 1].
The option can be set to have an infinite maximum (no maximum), using option value `inf`.
For more information, see the <<tools-datasynth-dbg-output,section about debug output>>.

* _BDD debug max paths_: Internally, predicates are represented using link:https://en.wikipedia.org/wiki/Binary_decision_diagram[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 <<tools-datasynth-dbg-output,section about debug output>>.
