Assignment cover analysis #261
Conversation
There was a problem hiding this comment.
I like the idea a lot. However, it would be really cool to lift this analysis to the operator level. I imagine a command similar to the typecheck command that analyses operator definitions one-by-one, in order to compute to which variables each operator is potentially assigning. You could merge this info in Next to figure out, whether the assignments are complete. It would be quite useful for the user to see the variables that are assigned in each operator.
| @@ -81,6 +81,10 @@ class CheckerExceptionAdapter @Inject()(sourceStore: SourceStore, | |||
| case err: MalformedTlaError => | |||
| val msg = "%s: unexpected TLA+ expression: %s".format(findLoc(err.causeExpr), err.getMessage) | |||
| FailureMessage(msg) | |||
|
|
|||
| case err: CoverData.CoverException => | |||
| val msg = "Incomplete assignment cover: \n%s\n".format(err.getMessage) | |||
There was a problem hiding this comment.
Can we write a more comprehensible error message and point to the manual?
There was a problem hiding this comment.
Any suggestions as to what such a message would look like? (other than the points-to-manual part)
There was a problem hiding this comment.
For instance: "Unable to find assignments for all state variables"
|
|
||
| val nextName = options.getOrElse("checker", "next", "Next") | ||
| val nextBody = findBodyOf(nextName, inModule.declarations: _*) | ||
| // We only check for manual assignments in Next |
There was a problem hiding this comment.
Why only in Next? Once this feature is out, the users will use them in Init as well.
There was a problem hiding this comment.
Technically, Init never has assignments (no primes)
There was a problem hiding this comment.
We produce InitPrimed in one of the first passes
There was a problem hiding this comment.
Exactly, therefore it has no manual assignments to check for
There was a problem hiding this comment.
Why cannot we write x := foo in Init?
There was a problem hiding this comment.
That's still not an assignment, x' := foo is (in InitPrime). The real question is, do you want a manual assignment (e.g. of x) in InitPrime to force you to manually assign all instances of x in Next? I think not.
There was a problem hiding this comment.
I think, yes. Once we tell the users that they can manually annotate the spec with assignments, it would be hard to explain them why they cannot manually annotate Init.
There was a problem hiding this comment.
I'll add the check if you want, just keep in mind that if anyone ever manually assigns to a variable in Init they will have to manually assign all assignments to that same variable in Next.
|
What I have in mind, the analyses that impose constraints on the input language (e.g., assignments, type annotations) should be triggered as early as possible, without doing too much preprocessing. Not only it will give the user better feedback, but also this analysis can be used independently of our model checker. |
Well, that is what the analysis does. It outputs what each operator covers in |
|
From reading the code, I had the impression that it assumes all operator bodies being inlined. Is not it the case? |
|
It was designed to be done just before the assignment phase so it does assume only nullary operators, but it runs the check over every operator body (now presumed inlined). The part where it checks |
|
Our preprocessing phase does a lot of stuff. How hard is it to write this new analysis without assuming any preprocessing? I don't see where the need for nullary operators is coming from. |
Not that hard. To do this kind of analysis, the nullary operator assumption isn't strictly necessary, but since I originally wrote the cover check to happen around the assignment phase it was a convenient simplifying assumption. |
|
I think we should do it in two phases: merge this PR (provided that we resolve the discussion about |
|
Alright, I'll just update the error message and IntPrime code pass before that. |
No description provided.