Skip to content

#693 #695 CIF controller properties checker: re-implement confluence check using BDDs instead of MDDs

  • Easiest to understand by checking individual commits. Mostly reviewable per commit. Some things change again slightly in a later commit.
  • End-user visible changes:
    • Confluence check re-implemented using BDDs rather than MDDs. Should improve performance.
    • CIF controller properties checker now no longer supports non-determinism for controllable events, regardless of what checks are performed. Previously, only MDD-based checks had this precondition, but now all checks have it. This is consistent with data-based synthesis, and with what was already documented for the controller properties checker. This change is also because the confluence check doesn't support such non-determinism.
    • CIF controller properties checker has a slight improvement to its debug output.
  • Other changes:
    • Comment/JavaDoc fixes/improvements.
    • CIF to BDD no non-determinism for ctrl events.
    • Re-implement confluence check using BDDs.
      • I tried to keep the code similar to what was there before.
      • Some fields are removed, as they can be taken from the CIF/BDD spec.
      • I now refer to 'original' variables as 'zero' variables.
      • I added more JavaDocs about 'zero' variables and 'allStateCovered'.
      • I loop over event indices to prevent the 'skipInner' set/logic.
      • With BDDs, we need to do proper free-ing.
      • Some changes to empty lines and comments for consistency/clarity.
      • Improved debug output (disabled in code, not end-user visible).
    • Removed no longer used MDD code (dead code).

Addresses #695 (closed) Fixes #693 (closed)

Edited by Dennis Hendriks

Merge request reports