#1154 Always optimize created con/dis-junctions.
- End-user visible changes:
- The creation of conjunctions/disjunctions has been optimized in certain cases, to consider literal
true
andfalse
values, such that for instancetrue and X
becomesX
. - The CIF to CIF linearization product/merge transformations may get simpler linearized predicates for edge guards, urgency guards, and initialization/marker predicates from locations.
- The CIF to CIF eliminate monitors transformation may get simpler edge guards and send values.
- CIF to UPPAAL may use simpler edge guards in the conversion to UPPAAL.
- CIF to Supremica may use simpler edge guards and state invariant predicates in the conversion to Supremica.
- Data-based synthesis and the BDD-based checks of the CIF controller properties checker may get simpler predicates in the conversion of the specification to BDDs. This may lead to differences in conversion performance and debug output. For data-based synthesis, the benchmarks shown only minimal changes (< 0.1% change in memory/time). However, for the
wafer_scanner_n1
benchmark, synthesis requires about 12% less BDD operations.
- The creation of conjunctions/disjunctions has been optimized in certain cases, to consider literal
- Other changes:
- Delete the option to not optimize con/disjunction creation.
- Adapt test output.
Closes #1154 (closed)
Edited by Dennis Hendriks