Replace assignments in invariants #1664
Conversation
Codecov Report
@@ Coverage Diff @@
## unstable #1664 +/- ##
============================================
+ Coverage 74.96% 74.99% +0.02%
============================================
Files 358 356 -2
Lines 11612 11597 -15
Branches 541 552 +11
============================================
- Hits 8705 8697 -8
+ Misses 2907 2900 -7
Continue to review full report at Codecov.
|
| case ex @ NameEx(name) if vars.contains(name) => | ||
| // add prime to a variable from vars | ||
| OperEx(TlaActionOper.prime, ex)(ex.typeTag) | ||
|
|
||
| case OperEx(TlaActionOper.prime, primedOnce @ OperEx(TlaActionOper.prime, _)) => | ||
| // in case the variable was already primed, remove the second prime | ||
| primedOnce |
There was a problem hiding this comment.
Rather than defining de-priming of doubly primed expressions, which relies on the implementation detail that ReplaceFixed implements post-transform too
https://github.com/informalsystems/apalache/blob/919e65948904156615a05980d98b335fd5a8fc2a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/ReplaceFixed.scala#L96-L99
I'd prefer defining this in a way that never attempts to add unnecessary primes in the first place:
| case ex @ NameEx(name) if vars.contains(name) => | |
| // add prime to a variable from vars | |
| OperEx(TlaActionOper.prime, ex)(ex.typeTag) | |
| case OperEx(TlaActionOper.prime, primedOnce @ OperEx(TlaActionOper.prime, _)) => | |
| // in case the variable was already primed, remove the second prime | |
| primedOnce | |
| case ex@OperEx(TlaActionOper.prime, _) => | |
| // in case the expression was already primed, ignore | |
| ex | |
| case ex @ NameEx(name) if vars.contains(name) => | |
| // add prime to a variable from vars | |
| OperEx(TlaActionOper.prime, ex)(ex.typeTag) |
There was a problem hiding this comment.
Are you sure that this code would not introduce two primes, i.e., by going to 113-115 first and then to 109-111 one level up in the recursion?
There was a problem hiding this comment.
When it goes one level up it will already be primed, so 109 will skip.
x -(113)-> x' -(109)-> x'
x' -(109)-> x' -(109)-> x'
There was a problem hiding this comment.
Ah, that makes sense.
There was a problem hiding this comment.
Heh, does not seem to work: https://github.com/informalsystems/apalache/runs/6174445003?check_suite_focus=true
There was a problem hiding this comment.
I looked into it, seems like your implementation of withFun doesn't allow short-circuiting.
Unlike a dedicated transformation, like Prime, it must always first look into the generic OperEx case
https://github.com/informalsystems/apalache/blob/919e65948904156615a05980d98b335fd5a8fc2a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/ReplaceFixed.scala#L96-L99
This is potentially problematic in practice; a lot of transformations rely on the fact that certain synactic forms halt exploration, because transforming may ruin subexpressions, but these generic PartialFunction traversals do not, they always full explore the expression tree.
There was a problem hiding this comment.
True. Prime had a very special behavior. We can think of generalizing ReplaceFixed even further.
There was a problem hiding this comment.
It's not just Prime, a typical tx has cases like
case InterestingCase => interestingCaseTx
case OperEx(args) => mapOverArgs
case LetIn => mapOverDecls
case default => defaultTxwhere interestingCaseTx would typically not recurse any more. I think this can be fixed by changing
ex match {
case LetInEx(body, defs @ _*) =>
// Transform bodies of all op.defs
val newDefs = defs.map(tracker.trackOperDecl { d => d.copy(body = self(d.body)) })
val newBody = self(body)
val retEx = if (defs == newDefs && body == newBody) ex else LetInEx(newBody, newDefs: _*)(ex.typeTag)
tr(retEx)
case OperEx(op, args @ _*) =>
val newArgs = args.map(self)
val retEx = if (args == newArgs) ex else OperEx(op, newArgs: _*)(ex.typeTag)
tr(retEx)
case _ => tr(ex)in withFun to
ex match {
case special if partialFun.isDefinedAt(special) =>
partialFun(special)
case LetInEx(body, defs @ _*) =>
// Transform bodies of all op.defs
val newDefs = defs.map(tracker.trackOperDecl { d => d.copy(body = self(d.body)) })
val newBody = self(body)
val retEx = if (defs == newDefs && body == newBody) ex else LetInEx(newBody, newDefs: _*)(ex.typeTag)
retEx
case OperEx(op, args @ _*) =>
val newArgs = args.map(self)
val retEx = if (args == newArgs) ex else OperEx(op, newArgs: _*)(ex.typeTag)
retEx
case _ => exThere was a problem hiding this comment.
It got automerged. Shall we open another PR for your suggestions?
…ns/package.scala Co-authored-by: Kukovec <jure.kukovec@gmail.com>
Closes #1663. As discussed in #1663, the model checker fails when an invariant contains assignments, e.g.,
UNCHANGED x. The bugfix is very simple: All assignmentsx' := eare replaced back tox' = ein the invariant candidates.Instead of implementing a yet another class similar to
PrimeandDeprime, I have refactoredReplaceFixedto accept a partial function, which produces a replacement, if the function is defined on its argument. To disambiguate three versions ofapply, I have renamed them towhenEqualsTo,whenMatches, andwithFun. This refactoring touched a lot of files, but the changes are syntactic.make fmt-fix(or had formatting run automatically on all files edited)