#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
PlaceKind
to express place of an invariant, together withReportPriority
that defines a relevance notion. -
Next the
NoKindInterface
is defined to form a common ground for theNoInvariant...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 theDisallowedSubset
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 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 firstinvariant
is the named object (generated by the framework), the secondinvariant
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.