Extend the invariant filter to specify particular invariants #2034
Conversation
From words `$stepNo` to words
`${stepNo}->${invariantKind}${invariantNo}`.
Codecov Report
@@ Coverage Diff @@
## main #2034 +/- ##
=======================================
Coverage 77.74% 77.74%
=======================================
Files 419 420 +1
Lines 12844 12846 +2
Branches 590 588 -2
=======================================
+ Hits 9985 9987 +2
Misses 2859 2859
📣 Codecov can now indicate which changes are the most critical in Pull Requests. Learn more |
| * all invariants only *after* exactly 10 steps have been made, | ||
| * the *first* state invariant only after exactly 15 steps, and | ||
| * the *second* action invariant after exactly 20 steps. |
There was a problem hiding this comment.
I'm a bit confused by this example: the first case seems to entail all variants are already checked from step 10 on, so I don't understand how the other two steps can be relevant. Is it possible this configures the checks to run only on the 10th step? Or are the second and third conditions here redundant? Or perhaps I'm misunderstanding the functionality?
There was a problem hiding this comment.
Ah, I can see how this could be confusing!
The first clause does not apply from step 10 onwards, but only at step 10 (hence, "exactly 10 steps").
Do you think it would help to reword this? Or maybe it's enough to change the emphasis from "after" to "exactly"?
There was a problem hiding this comment.
Yes, that does clear things up for me! I would suggestion perhaps something like:
| * all invariants only *after* exactly 10 steps have been made, | |
| * the *first* state invariant only after exactly 15 steps, and | |
| * the *second* action invariant after exactly 20 steps. | |
| * *all* invariants (because of the wildcard match) at the 10th step, | |
| * the *first* state invariant (`state0`) at the 15th step, and | |
| * the *second* action invariant (`action1`) at the 20th step. |
There was a problem hiding this comment.
I think we're getting close :)
Still one issue though: saying "at the Xth step" here is inaccurate, as it might refer to both the states before and after taking the step. Technically, we're checking invariants at all (step+1)th (symbolic) states. How about this?
| * all invariants only *after* exactly 10 steps have been made, | |
| * the *first* state invariant only after exactly 15 steps, and | |
| * the *second* action invariant after exactly 20 steps. | |
| * *all* invariants (because of the wildcard match) at states reached after the 10th step, | |
| * the *first* state invariant (`state0`) at states reached after the 15th step, and | |
| * the *second* action invariant (`action1`) at states reached after the 20th step. |
There was a problem hiding this comment.
My issue here is that in this context I take "after" to mean "anytime from this point forward". I guess its because while you mean the plural "states" to range breadth wise over the immediate successor steps, I think the natural reading is to read it as both breadth- and depth-wise, ranging over all states that could follow.
Maybe using a phrase like "immediate successor states" would help?
There was a problem hiding this comment.
I guess that's why Igor's original wording was "after exactly 10 steps", which to me communicates that it refers only to 10, not 9 or 11.
But I think you resolve the order of "after" and "exactly" differently than I do?
There was a problem hiding this comment.
True “after exactly 5 minutes” means to me “any time > t+5m”. Could be i am unusually fixated on an indeterminate range for “after” :)
I don’t want to get you hung up here, especially not if it’s consistent with the other docs. Maybe just merge it as is and we can revisit if other users have trouble?
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala
Show resolved
Hide resolved
Co-authored-by: Shon Feder <shon@informal.systems>
| * all invariants only *after* exactly 10 steps have been made, | ||
| * the *first* state invariant only after exactly 15 steps, and | ||
| * the *second* action invariant after exactly 20 steps. |
There was a problem hiding this comment.
Yes, that does clear things up for me! I would suggestion perhaps something like:
| * all invariants only *after* exactly 10 steps have been made, | |
| * the *first* state invariant only after exactly 15 steps, and | |
| * the *second* action invariant after exactly 20 steps. | |
| * *all* invariants (because of the wildcard match) at the 10th step, | |
| * the *first* state invariant (`state0`) at the 15th step, and | |
| * the *second* action invariant (`action1`) at the 20th step. |
Closes #2031. Towards https://github.com/informalsystems/apalache-cloud/issues/106.
We currently expose an invariant filter via tuning flags. It accepts a regular expression recognizing words over step numbers. Apalache then only checks state and action invariants in the step numbers accepted by the filter.
We extend the invariant filter syntax to also specify which invariants to check in a step.
We achieve this by extending the regular expression to accepting words (really, triples) of the shape
${stepNo}->${invariantKind}${invariantNo}. This is similar to the existing transition filter syntax that accepts words${stepNo}->${transitionNo}.make fmt-fix(or had formatting run automatically on all files edited)