Predicate simplification
The data-based 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:
| Option value | Default | Predicate | May be simplified assuming |
|---|---|---|---|
|
|
yes |
Supervisor guards of controllable events |
Plant guards, for the matching events |
|
|
yes |
Supervisor guards of controllable events |
State/event exclusion requirement invariants derived from the requirement automata, for the matching events |
|
|
yes |
Supervisor guards of controllable events |
State/event exclusion plant invariants from the input specification, for the matching events |
|
|
yes |
Supervisor guards of controllable events |
State/event exclusion requirement invariants from the input specification, for the matching events |
|
|
yes |
Supervisor guards of controllable events |
State plant invariants from the input specification |
|
|
yes |
Supervisor guards of controllable events |
State requirement invariants from the input specification (includes the range requirement invariants added by the synthesis algorithm) |
|
|
yes |
Supervisor guards of controllable events |
Controlled behavior as computed by synthesis |
|
|
yes |
Initialization predicate of the controlled system |
Initialization predicate of the uncontrolled system |
|
|
yes |
Initialization predicate of the controlled system |
State plant invariants from the input specification |
Which simplifications should be performed, can be specified using the BDD predicate simplify option (see the options section).
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.