Skip to content

#621 Prepare controller properties checker tool for BDD-based bounded response check

  • Best to review per commit. I took very small steps, to make it clear what happens step-by-step, and keep the diffs per commit small. Best to keep any comments for the end though, as some things are changed in multiple commits, or are later changed again.
  • End-user visible changes:
    • Proper/consistent naming of the tool itself (in: JavaDocs, comments, class names, documentation, app name, app description, error messages, etc).
    • If no checks enabled, don't load the specification, do any preparations, etc.
    • Improved check for no (un)controllable events. Check also for uncontrollable events. Check based on alphabet of the specification, not event declarations.
    • Changed debug output for starting to prepare, to now indicate it prepares for MDD-based checks.
    • New precondition: only plant/supervisor automata/invariants, no kindless/requirement.
    • Check for no state invariants, only events with controllability, no tau (implicit and explicit) with new precondition checker framework.
    • Require at least one automaton as precondition. Was a warning before.
    • Small documentation improvements.
  • Other changes:
    • Consistently refer to MDDs, not multi-valued. MDD was already used in various places, but not consistently. Improves BDD vs MDD consistency. (in: JavaDocs, comment, class names, package names, etc).
    • Prepare for later having both BDD-based and MDD-based checks (comment changes, moved some MDD-related classes to new mdd package, don't refer to 'both checks', quantify that it some things are only for MDDs, do certain preparations only for MDD-based checks, etc).
    • Print debug output when starting preparations for MDDs, not during it.
    • Moved some MDD-specific tests to a sub-folder.
    • Renamed some tests.
    • Fixed indentation in a test model.
    • Some other changes in the ControllerCheckerApp to make it easier to later add BDD-related checks, and more checks in general (keep some things more local).
    • Some other small comment etc changes.

Addresses #621

Merge request reports