apalache Temporal translation broken with nested temporal subformulas and quantifiers

Translation of temporal properties is broken, if the property contains nested temporal subformulas and quantifiers.

Take the temporal property of the MWE below;

TemporalProp == [](\A i \in DOMAIN x: <>(i \in DOMAIN x))

In the temporal encoding, the binding under \A is lost in Next by introducing literals for the temporal subformulas. In particular, after TemporalPass, the encoding is:

Init == ...
    /\ __temporal_t_2 = (\A i$2 \in DOMAIN x: __temporal_t_3)

...

Step == ...
    /\ (__temporal_t_3 <=> i$2 \in DOMAIN x \/ __temporal_t_3')
    /\ (__temporal_t_3_unroll
      <=> __temporal_t_3_unroll_prev \/ (__InLoop' /\ i$2 \in DOMAIN x))
    /\ __temporal_t_2' = (\A i$2 \in DOMAIN x: __temporal_t_3)

Obviously, in Step, i$2 is not bound.

Impact

I believe this is nonblocking, but it affects @josef-widder's Quint spec for Polygon.

Input specification

-------------------------- MODULE test --------------------------

EXTENDS Integers

VARIABLE
    \* @type: Int -> Int;
    x

Init == x = [i \in Nat |-> 42]
Next == x' = x

TemporalProp == [](\A i \in DOMAIN x: <>(i \in DOMAIN x))

===============

The command line parameters used to run the tool

--temporal=TemporalProp --write-intermediate

Expected behavior

Log files

2023-09-25T12:14:28,760 [main] INFO  a.f.a.t.Tool\$ - # APALACHE version: v0.43.0-12-g7303626a2 | build: v0.43.0-12-g7303626a2
2023-09-25T12:14:28,771 [main] INFO  a.f.a.t.t.o.CheckCmd - Tuning: search.outputTraces=false
2023-09-25T12:14:28,891 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser
2023-09-25T12:14:29,045 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser [OK]
2023-09-25T12:14:29,046 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat
2023-09-25T12:14:29,046 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
2023-09-25T12:14:29,113 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Your types are purrfect!
2023-09-25T12:14:29,113 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > All expressions are typed
2023-09-25T12:14:29,123 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat [OK]
2023-09-25T12:14:29,123 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass
2023-09-25T12:14:29,125 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to Init
2023-09-25T12:14:29,125 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
2023-09-25T12:14:29,125 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set a temporal property to TemporalProp
2023-09-25T12:14:29,132 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass [OK]
2023-09-25T12:14:29,132 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass
2023-09-25T12:14:29,132 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
2023-09-25T12:14:29,141 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass [OK]
2023-09-25T12:14:29,141 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass
2023-09-25T12:14:29,142 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next, TemporalProp
2023-09-25T12:14:29,152 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass [OK]
2023-09-25T12:14:29,152 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass
2023-09-25T12:14:29,152 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > Rewriting temporal operators...
2023-09-25T12:14:29,154 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > Found 1 temporal properties
2023-09-25T12:14:29,154 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > Adding logic for loop finding
2023-09-25T12:14:29,288 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass [OK]
2023-09-25T12:14:29,288 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass
2023-09-25T12:14:29,288 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next, TemporalProp
2023-09-25T12:14:29,303 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass [OK]
2023-09-25T12:14:29,303 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass
2023-09-25T12:14:29,304 [main] INFO  a.f.a.t.p.a.PrimingPassImpl -   > Introducing InitPrimed for Init'
2023-09-25T12:14:29,320 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass [OK]
2023-09-25T12:14:29,320 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen
2023-09-25T12:14:29,320 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > Producing verification conditions from the invariant TemporalProp
2023-09-25T12:14:29,321 [main] INFO  a.f.a.t.b.VCGenerator -   > VCGen produced 1 verification condition(s)
2023-09-25T12:14:29,332 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen [OK]
2023-09-25T12:14:29,332 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass
2023-09-25T12:14:29,333 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
2023-09-25T12:14:29,336 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
2023-09-25T12:14:29,336 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
2023-09-25T12:14:29,346 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
2023-09-25T12:14:29,356 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
2023-09-25T12:14:29,367 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
2023-09-25T12:14:29,377 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
2023-09-25T12:14:29,392 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
2023-09-25T12:14:29,404 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass [OK]
2023-09-25T12:14:29,404 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass
2023-09-25T12:14:29,411 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found 1 initializing transitions
2023-09-25T12:14:29,414 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found 2 transitions
2023-09-25T12:14:29,415 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > No constant initializer
2023-09-25T12:14:29,415 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Applying unique renaming
2023-09-25T12:14:29,428 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass [OK]
2023-09-25T12:14:29,428 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass
2023-09-25T12:14:29,431 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
2023-09-25T12:14:29,432 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2023-09-25T12:14:29,435 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
2023-09-25T12:14:29,436 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > SetMembershipSimplifier
2023-09-25T12:14:29,437 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2023-09-25T12:14:29,449 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass [OK]
2023-09-25T12:14:29,449 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass
2023-09-25T12:14:29,451 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
2023-09-25T12:14:29,451 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Skolemization
2023-09-25T12:14:29,451 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Expansion
2023-09-25T12:14:29,453 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Remove unused let-in defs
2023-09-25T12:14:29,454 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
2023-09-25T12:14:29,467 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
2023-09-25T12:14:29,467 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass [OK]
2023-09-25T12:14:29,467 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #13: BoundedChecker
2023-09-25T12:14:29,475 [main] DEBUG a.f.a.t.b.s.Z3SolverContext - Creating Z3 solver context 0
2023-09-25T12:14:29,873 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
2023-09-25T12:14:29,874 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT
2023-09-25T12:14:29,913 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0. Is it enabled?
2023-09-25T12:14:29,915 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0 is enabled
2023-09-25T12:14:29,916 [main] INFO  a.f.a.t.b.SeqModelChecker - State 0: Checking 1 state invariants
2023-09-25T12:14:29,916 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking state invariant 0
2023-09-25T12:14:29,920 [main] INFO  a.f.a.t.b.SeqModelChecker - State 0: state invariant 0 holds.
2023-09-25T12:14:29,923 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 0: picking a transition out of 1 transition(s)
2023-09-25T12:14:29,924 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #0
2023-09-25T12:14:29,924 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT
2023-09-25T12:14:29,937 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - Adapted exception intercepted: 
at.forsyte.apalache.tla.bmcmt.RewriterException: No rewriting rule applies to expression: i\$1 ∈ DOMAIN x
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:403)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422)
	at at.forsyte.apalache.tla.bmcmt.rules.OrRule.mapArg\$1(OrRule.scala:58)
	at at.forsyte.apalache.tla.bmcmt.rules.OrRule.\$anonfun\$apply\$2(OrRule.scala:62)
	at scala.collection.immutable.List.map(List.scala:246)
	at scala.collection.immutable.List.map(List.scala:79)
	at at.forsyte.apalache.tla.bmcmt.rules.OrRule.apply(OrRule.scala:62)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:355)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:388)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422)
	at at.forsyte.apalache.tla.bmcmt.rules.EqRule.apply(EqRule.scala:49)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:355)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:388)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.mapArg\$1(AndRule.scala:62)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.\$anonfun\$apply\$2(AndRule.scala:66)
	at scala.collection.immutable.List.map(List.scala:250)
	at scala.collection.immutable.List.map(List.scala:79)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.apply(AndRule.scala:66)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:355)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:388)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422)
	at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.prepareTransition(TransitionExecutorImpl.scala:107)
	at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.prepareTransition(FilteredTransitionExecutor.scala:48)
	at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.prepareTransition(ConstrainedTransitionExecutor.scala:98)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.\$anonfun\$prepareTransitionsAndCheckInvariants\$5(SeqModelChecker.scala:213)
	at scala.runtime.java8.JFunction1\$mcVI\$sp.apply(JFunction1\$mcVI\$sp.scala:18)
	at scala.collection.immutable.Range.foreach(Range.scala:190)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.prepareTransitionsAndCheckInvariants(SeqModelChecker.scala:207)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:123)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:66)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:135)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:88)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.exec(PassChainExecutor.scala:64)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$3(PassChainExecutor.scala:53)
	at scala.util.Either.flatMap(Either.scala:352)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$1(PassChainExecutor.scala:51)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
	at scala.collection.LinearSeqOps.foldLeft\$(LinearSeq.scala:179)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.runOnPasses(PassChainExecutor.scala:44)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:34)
	at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:132)
	at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:138)
	at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:118)
	at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)
2023-09-25T12:14:29,938 [main] ERROR a.f.a.t.Tool\$ - <unknown>: rewriter error: No rewriting rule applies to expression: i\$1 ∈ DOMAIN x
at.forsyte.apalache.infra.AdaptedException: <unknown>: rewriter error: No rewriting rule applies to expression: i\$1 ∈ DOMAIN x
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:39)
	at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:132)
	at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:138)
	at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:118)
	at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)

System information

Apalache version: v0.43.0-12-g7303626a2 build v0.43.0-12-g7303626a2
OS: Mac OS X
JDK version: 17.0.2

Triage checklist (for maintainers)

[ ] Reproduce the bug on the main development branch.
[ ] Add the issue to the apalache GitHub project.
[ ] If the bug is high impact, ensure someone available is assigned to fix it.

Sep 25 '23 10:09 thpani

@p-offtermatt Do you remember if you considered this during your internship? That is, is this kind of property not supported at all?

Sep 25 '23 10:09 thpani

Are we talking about main or the temporal branch?

Sep 25 '23 10:09 Kukovec

Are we talking about main or the temporal branch?

main.

This is non-blocking, I just created the issue to have it on file.

Sep 25 '23 10:09 thpani

iirc this is not supported at all - I remember stumbling over this and I think the decision was to focus on the non-quantifier case, and the quantified temporal-formula case was never finished

Sep 25 '23 11:09 p-offtermatt

I think for many specs we can work around that. Even in the draft spec that I have written, I first had written temporal formulas where indices don't range over temporal operators (because that is what I am used to in the parameterized case).

But then I realized that to others (e.g., clients), the formula that creates the troubles might be more readable.

From a user perspective, the error message was a bit frightening, though. Would it be hard to identify whether the temporal formula is outside of the fragment Apalache supports, and in this case return a better error message?

Sep 25 '23 15:09 josef-widder

From a user perspective, the error message was a bit frightening, though. Would it be hard to identify whether the temporal formula is outside of the fragment Apalache supports, and in this case return a better error message?

Yes, we should issue a proper error message if the property is outside the supported language fragment.

Sep 27 '23 13:09 thpani

apalache apalache copied to clipboard

Temporal translation broken with nested temporal subformulas and quantifiers

Impact

Input specification

The command line parameters used to run the tool

Expected behavior

Log files

System information

Triage checklist (for maintainers)

apalache
apalache copied to clipboard