Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Temporal translation broken with nested temporal subformulas and quantifiers #2746

Open
3 tasks
thpani opened this issue Sep 25, 2023 · 6 comments
Open
3 tasks
Labels

Comments

@thpani
Copy link
Collaborator

thpani commented Sep 25, 2023

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.
@thpani thpani added the bug label Sep 25, 2023
@thpani
Copy link
Collaborator Author

thpani commented Sep 25, 2023

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

@Kukovec
Copy link
Collaborator

Kukovec commented Sep 25, 2023

Are we talking about main or the temporal branch?

@thpani
Copy link
Collaborator Author

thpani commented Sep 25, 2023

Are we talking about main or the temporal branch?

main.

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

@p-offtermatt
Copy link
Collaborator

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

@josef-widder
Copy link
Contributor

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?

@thpani
Copy link
Collaborator Author

thpani commented Sep 27, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

4 participants