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