#457 Generalize invariants checking
Adresses #457 (closed) #368 (closed) #424 (closed)
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
PlaceKindto express place of an invariant, together withReportPrioritythat defines a relevance notion. -
Next the
NoKindInterfaceis defined to form a common ground for theNoInvariant...Kindenumerations 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...Kindenumerations comes theDisallowedSubsetclass that stores a specified invariants subset that should be reported when found. -
The main check class
InvNoSpecificInvsCheckstores all the disallowed subsets for all combinations ofSupKind,InvKind, andPlaceKind. 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 firstinvariantis the named object (generated by the framework), the secondinvariantis 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.