Skip to content

#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 and false values, such that for instance true and X becomes X.
    • 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.
  • Other changes:
    • Delete the option to not optimize con/disjunction creation.
    • Adapt test output.

Closes #1154 (closed)

Edited by Dennis Hendriks

Merge request reports

Loading