Skip to content

#971 CIF controller properties checker: bounded response check uses execution order

  • Best to review per commit.
  • End-user visible changes:
    • The semantics of the uncontrollable/controllable events bounds of the controller properties annotation have changed. Rather than representing the maximum length of the sequences of events, they now represent the number of iterations of the event loops, assuming the execution scheme.
    • The CIF controller properties checker's bounded response check now computes the different bounds, assuming the execution scheme.
    • The CIF controller properties checker now converts the input CIF specification to an internal representation for each check, rather than at the start. This may reduce the required memory if multiple internal representations are required.
    • The CIF controller properties checker documentation has some small improvements.
  • Other changes:
    • ControllerCheckerCheck is now an interface.
    • Different checks may convert to BDD/MDD differently now.
    • CIF to BDD now has an extra option to 'adhere to the execution scheme'.
    • The controller properties checks perform less redundant tests now. Check for a specific check are only done for that check, not also for all checks. Prevents too large maintenance burden when changing one test. Prevents doing too expensive tests for other checks.
    • Added CifExecSchemeUtils class. Used it instead of sorting, where relevant.

Closes #971 (closed)

Edited by Dennis Hendriks

Merge request reports