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
PlaceKindto express place of an invariant, together with
ReportPrioritythat defines a relevance notion.
NoKindInterfaceis defined to form a common ground for the
NoInvariant...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 the
DisallowedSubsetclass that stores a specified invariants subset that should be reported when found.
The main check class
InvNoSpecificInvsCheckstores all the disallowed subsets for all combinations of
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 (
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
invariantis the named object (generated by the framework), the second
invariantis 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
EDIT: Added the proper issue number in the title.