Skip to content

#457 Generalize invariants checking

Albert Hofkamp requested to merge 457-more-general-invariants-checker into develop

Adresses #457 (closed) #368 (closed) #424

I was wrong in thinking I didn't need the generalized invariant check in cif2plc, as we found out in !422 (merged) . Thus I moved implementing the check forward to allow finishing the cif2plc pre checker issue.

This patch is built bottom up.

  • It starts with adding a PlaceKind to express place of an invariant, together with ReportPriority that defines a relevance notion.

  • Next the NoKindInterface is defined to form a common ground for the NoInvariant...Kind enumerations that define what the user can specify for the check.

    If you read commits, I made the error here of adding a size(?) notion to the interface which doesn't work as it's not a member function.

    The interface is not strictly needed, but I think it's good to have it anyway as it reduces duplication of function docs, and forces consistency.

  • On top of the NoInvariant...Kind enumerations comes the DisallowedSubset class that stores a specified invariants subset that should be reported when found.

  • The main check class InvNoSpecificInvsCheck stores all the disallowed subsets for all combinations of SupKind, InvKind, and PlaceKind. It silently discards checks that are not relevant enough to get reported for each combination individually.

    Checking is then a simple "grab the disallowed subsets for the concrete invariant that we find, and report it if disallowed subsets are indeed found".

  • The check class is extended with the "ignore harmless invariants" extension (invariant true, needs true, disables false).

  • A tests to check the harmless extension works, and a test with 2 disallowed subsets.

Three further points:

  • I don't know how to fix the - Unsupported "named_invs.I2" (File "...": line 72, columns 15 .. 16): invariant is invariant. error. The message is stupid. The first invariant is the named object (generated by the framework), the second invariant is generated by my check.

  • There are other invariant checks and tests in the pre-checker framework, the simplest to do is perhaps remove those after merging this.

  • There is also a previous branch for this check that was deemed too complicated or wrong (branch 424-more-general-invariants-checker).

EDIT: Added the proper issue number in the title.

Edited by Albert Hofkamp

Merge request reports