Skip to content

#1087 Add 'Eliminate state invariants' CIF to CIF transformations

  • This turned out to be much more subtle than I realized upfront, so it also took a bit more time to get it right.
  • Best to review per commit, but read the commit messages as some changes are spread out over multiple commits.
  • End-user visible changes:
    • A new 'Eliminate state invariants' CIF to CIF transformation has been added. It comes in three variants: one that eliminates all state invariants, one that only eliminates plant state invariants, and one that only eliminates supervisor state invariants.
  • Other changes:
    • Added CifCollectUtils.collectInvariants.
    • Improved SimplifyValues:
      • Made 'dummyInv' field final.
      • JavaDoc improvements for transform(Expression).
      • transform(Expression) is now easier to use; no more null result. It handles completely replaced expressions in the transform method now, rather than callers having to handle it. Updated CIF to mCRL2 transformation for this change.
      • Check preconditions.
    • Improved CifAddressableUtils:
      • Improved/extended JavaDocs/comments.
      • Improved code, using more modern Java concepts.
      • getRefExprs and collectProjs now check for no wrapping expressions.
      • Added new hasProjs method.
    • Added new CifUpdateUtils class.
      • It comes with hasProjectedAddressable and hasTupleAddressable methods.
      • Some methods from ElimIfUpdates have been moved to CifUpdateUtils, to allow reusing them, and also come with these changes:
        • Updated/improved JavaDocs/comments.
        • Comments re-wrapped to 120 characters line length.
        • Added new exception, as can't use one from CIF to CIF transformer.
        • Make sure enough deepcloning is used.
        • Don't support wrapping expressions in addressables.
      • Added new updatesToNewValueExprPerVar method.
    • Added CifValueUtils.hasSubExprSatisfyingPred method.

Closes #1087 (closed)

Merge request reports

Loading