Skip to content

#410 CIF controller properties checker: add non-blocking under control check

  • Changes:
    • Preparations:
      • CifBddReachability: decide whether to use uncontrollable and input-variable edges separately.
      • Controller checker: code improvement on conclusion API.
        • CheckConclusion: Renamed printDetails to printResult as it prints the result, including the details of the result.
        • CheckConclusion: Added printsResults to query whether details are printed or not.
        • ControllerCheckerApp: More regular code to decide empty line between conclusions printing of different checks. Some existing checks conditionally print details, other always. And the new check (at least in this first version) never prints details.
    • Actual change:
      • Extended controller:properties annotation with nonBlockingUnderControl argument.
      • Added non-blocking under control check to controller properties checker.
    • Unrelated change:
      • PLCgen docs: added that computing a state space can also verify that a specification has no runtime errors, similar to what the CIF controller properties checker already indicates.
  • I've set this to only address #410, not close it, as we're still discussing some points there.
  • For the most part, it is best to review per commit. But, the tests are changed via many commits, in an attempt to keep intermediate diffs understandable. That tests part is best to understand per commit, but hold reviews until the end until you've seen all these commits.

Addresses #410

Merge request reports