Debug output

By default, the data-based 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.

Bounded reachability requirements

For bounded reachability requirements, debug output also reports the configured bound, the minimum-bound status and the reason that the bounded computation stopped. These messages describe an individual backward reachability computation within the overall synthesis computation. Synthesis can repeat this computation as other requirements and computations restrict the controlled behavior, so intermediate results may differ from those for the final supervisor.

For a requirement with from, the cover states are the source states to which the requirement currently applies, taking the current controlled behavior and any avoid or stay restriction into account. Cover states are covered when the computation has found a path to the goal from every such source state. Different source states may use different paths, possibly to different goal states, and their shortest permitted paths may have different lengths. If there are applicable source states and all are covered, the minimum bound is the largest of these shortest-path lengths: it is the smallest bound sufficient for every applicable source state.

For example, a bounded reachability requirement with from: source may have bound: 10, while one source state needs only one transition to reach the goal and another needs three. If all other applicable source states can also reach the goal within three transitions, debug output contains:

... [bounded result, bound: 10, minimum bound: 3, cover states covered].

Coverage can also hold at depth zero, either because all applicable source states already satisfy the goal or because there are no applicable source states. Thus, coverage alone does not show that source states remain reachable from an initial state.

If a fixed point is reached first, the reported minimum bound instead indicates the depth beyond which no additional states are found. For example:

... [bounded result, bound: 10, minimum bound: 2, fixed point].

This means that allowing more than two transitions would not add any states to this reachability result. It does not imply that all applicable source states can reach the goal: some may be unable to do so under the current restrictions, regardless of the bound. Without from, there are no cover states to check, and a minimum bound is reported only if a fixed point is reached.

If the configured bound is exhausted before either condition is reached, debug output instead contains, for example:

... [bounded result, bound: 10, minimum bound: not determined, bound reached].

For a requirement with from, this means that not all source states to which the requirement currently applies could reach the goal within the configured bound.

Performance implications

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 .. 231 - 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 non-negative. 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.