Add support for actions under temporal operators #1879
Conversation
Codecov Report
@@ Coverage Diff @@
## unstable #1879 +/- ##
============================================
+ Coverage 76.83% 76.85% +0.02%
============================================
Files 400 400
Lines 12271 12279 +8
Branches 577 584 +7
============================================
+ Hits 9428 9437 +9
+ Misses 2843 2842 -1
Continue to review full report at Codecov.
|
| @@ -33,6 +34,21 @@ class TableauEncoder( | |||
|
|
|||
| private def inBoolSet(element: TBuilderInstruction): TBuilderInstruction = builder.in(element, builder.booleanSet()) | |||
|
|
|||
| /* replaces all occurences of foo := bar with foo = bar */ | |||
There was a problem hiding this comment.
could you add a comment on why it is sound?
There was a problem hiding this comment.
You mean, why this is okay to do?
This is inside a temporal property, not in an actual action. Leaving these as assignments leads the transition finder to see an assignment on the right-hand side of another assignment.
E.g. consider this
CoolAction == x := 2
TemporalProperty == <>[CoolAction]_x
Due to the details of the encoding, a variable will be produced that gets assigned like this:
_temporal__CoolAction := (x := 2)
Then the assignment (x := 2) should be written as an equality, and that's what this function does.
I added the explanation to where the function is invoked, let me know what you think.
There was a problem hiding this comment.
I mean, usually you would have x' := 2, that is x with a prime. Would you keep the prime?
There was a problem hiding this comment.
Clarified this a bit more. (TLDR: everything is kept the same, except := is replaced by =)
Co-authored-by: Igor Konnov <igor@informal.systems>
tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/temporal/TableauEncoder.scala
Outdated
Show resolved
Hide resolved
Fixes buggy behaviour when actions are inside temporal operators by subtly changing the encoding.
It necessitates a change from the way the encoding is specified in the paper, which is necessary due to the technicalities of TLA+.
Essentially, double-priming is not allowed, while in LTL stacking next operators is no issue, so the subtle changes account for this.