Skip to content

#424 #736 Use precondition checker framework for the CIF controller properties checker

  • I took small steps per commit.
  • Changes:
    • Two precondition checkers of the CIF controller properties checker were migrated. They are executed one after another, with some preprocessing in between, and therefore can't be merged. This addresses #424 (closed).
    • Functional changes to the checks of the CIF controller properties checker:
      • Removed the 'no equations' check, as it is not needed. Algebraic variables have already been eliminated at that point. This elimination may lead to if expressions (which are allowed) and location references (which are also allowed). Equations for derivates are not something that needs to be checked either, since continuous variables are already disallowed.
      • The check is now a bit more strict on certain expressions on certain types, where previously only the types themselves were reported. This does not lead to less models being accepted.
      • Annotations are now ignored. This fixes #736 (closed) and addresses #593 (closed).
      • Stop non-determinism check for MDD-based checks earlier, if an event already is non-deterministic, as it doesn't need to be reported multiple times.
    • Small improvements/fixes for the controller properties checker 'Supported specifications' documentation:
      • = is supported on booleans as well (integers were listed twice).
      • Made it explicit that algebraic variables are supported as well (indicating only discrete and input variables may have given the impression that algebraic variables are not supported).
    • The checker framework is now has termination request awareness, and prints a message indicating the reported issues may be incomplete, if termination was requested. Currently only affects the CIF controller properties checker's non-determinism check.

Addresses #424 (closed) Addresses #593 (closed) Fixes #736 (closed)

Edited by Dennis Hendriks

Merge request reports