apalache
apalache copied to clipboard
Published
20 hours ago •
apalache-mc
apalache-mc
Unexpected equality test if [X -> Y] is used
Description
Comparison of two sets of functions, one of which is of form [X -> Y] leads to Unexpected equality test error
Input specification
---- MODULE Apalache_M0 ----
VARIABLE
\* @type: Bool;
x
\* @type: Set(Bool -> Bool);
u == {[q \in BOOLEAN |-> TRUE]}
\* @type: Set(Bool -> Bool);
v == [BOOLEAN -> BOOLEAN]
Init == x = TRUE
Next == x' = (v /= u)
====
The command line parameters used to run the tool
--out-dir=C:\work\TLA\tlc-qual\.tmp --run-dir=C:\work\TLA\tlc-qual\.tmp --length=5
Expected behavior
No error is expected
Log files
20:09:36.126 [main] INFO a.f.a.t.Tool\$ - # APALACHE version: 0.25.7 | build: 554bdb5
20:09:36.315 [main] INFO a.f.a.t.Tool\$ - Checker options: check --out-dir=C:\\work\\TLA\\tlc-qual\\.tmp --run-dir=C:\\work\\TLA\\tlc-qual\\.tmp --length=5 C:\\work\\TLA\\tlc-qual\\draft.sandbox\\Let\\FunSet\\dl\\ref\\Apalache_M0.tla
20:09:36.315 [main] INFO a.f.a.t.Tool\$ - Tuning:
20:09:36.331 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
20:09:36.549 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
20:09:36.549 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat
20:09:36.549 [main] INFO a.f.a.t.t.p.EtcTypeCheckerPassImpl - > Running Snowcat .::.
20:09:36.693 [main] INFO a.f.a.t.t.p.EtcTypeCheckerPassImpl - > Your types are purrfect!
20:09:36.693 [main] INFO a.f.a.t.t.p.EtcTypeCheckerPassImpl - > All expressions are typed
20:09:36.710 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [OK]
20:09:36.710 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass
20:09:36.710 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > TLC config file found in specification directory. To enable it, pass --config=C:\\work\\TLA\\tlc-qual\\draft.sandbox\\Let\\FunSet\\dl\\ref\\Apalache_M0.cfg.
20:09:36.710 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Command line option --init is not set. Using Init
20:09:36.710 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Command line option --next is not set. Using Next
20:09:36.710 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the initialization predicate to Init
20:09:36.710 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the transition predicate to Next
20:09:36.710 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass [OK]
20:09:36.710 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass
20:09:36.710 [main] INFO a.f.a.t.p.p.DesugarerPassImpl - > Desugaring...
20:09:36.710 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass [OK]
20:09:36.710 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass
20:09:36.726 [main] INFO a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next
20:09:36.750 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass [OK]
20:09:36.750 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #5: PrimingPass
20:09:36.750 [main] INFO a.f.a.t.a.p.PrimingPassImpl - > Introducing InitPrimed for Init'
20:09:36.750 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #5: PrimingPass [OK]
20:09:36.750 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #6: VCGen
20:09:36.750 [main] INFO a.f.a.t.b.p.VCGenPassImpl - > No invariant given. Only deadlocks will be checked
20:09:36.750 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #6: VCGen [OK]
20:09:36.750 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #7: PreprocessingPass
20:09:36.750 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Before preprocessing: unique renaming
20:09:36.761 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Applying standard transformations:
20:09:36.761 [main] INFO a.f.a.t.p.p.PreproPassImpl - > PrimePropagation
20:09:36.761 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Desugarer
20:09:36.761 [main] INFO a.f.a.t.p.p.PreproPassImpl - > UniqueRenamer
20:09:36.761 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Normalizer
20:09:36.761 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Keramelizer
20:09:36.761 [main] INFO a.f.a.t.p.p.PreproPassImpl - > After preprocessing: UniqueRenamer
20:09:36.777 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #7: PreprocessingPass [OK]
20:09:36.777 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #8: TransitionFinderPass
20:09:36.777 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > Found 1 initializing transitions
20:09:36.794 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > Found 1 transitions
20:09:36.795 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > No constant initializer
20:09:36.795 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > Applying unique renaming
20:09:36.797 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #8: TransitionFinderPass [OK]
20:09:36.797 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #9: OptimizationPass
20:09:36.797 [main] INFO a.f.a.t.p.p.OptPassImpl - > Applying optimizations:
20:09:36.797 [main] INFO a.f.a.t.p.p.OptPassImpl - > ConstSimplifier
20:09:36.797 [main] INFO a.f.a.t.p.p.OptPassImpl - > ExprOptimizer
20:09:36.797 [main] INFO a.f.a.t.p.p.OptPassImpl - > SetMembershipSimplifier
20:09:36.797 [main] INFO a.f.a.t.p.p.OptPassImpl - > ConstSimplifier
20:09:36.797 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #9: OptimizationPass [OK]
20:09:36.797 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #10: AnalysisPass
20:09:36.797 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Marking skolemizable existentials and sets to be expanded...
20:09:36.797 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Skolemization
20:09:36.813 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Expansion
20:09:36.824 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Remove unused let-in defs
20:09:36.824 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Running analyzers...
20:09:36.831 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Introduced expression grades
20:09:36.831 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #10: AnalysisPass [OK]
20:09:36.831 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #11: PostTypeCheckerSnowcat
20:09:36.831 [main] INFO a.f.a.t.b.p.PostTypeCheckerPassImpl - > Running Snowcat .::.
20:09:36.864 [main] INFO a.f.a.t.b.p.PostTypeCheckerPassImpl - > Your types are purrfect!
20:09:36.864 [main] INFO a.f.a.t.b.p.PostTypeCheckerPassImpl - > All expressions are typed
20:09:36.864 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #11: PostTypeCheckerSnowcat [OK]
20:09:36.864 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #12: BoundedChecker
20:09:37.423 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
20:09:37.423 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
20:09:37.445 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0. Is it enabled?
20:09:37.445 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0 is enabled
20:09:37.445 [main] INFO a.f.a.t.b.t.TransitionExecutorImpl - Step 0: picking a transition out of 1 transition(s)
20:09:37.453 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #0
20:09:37.453 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
20:09:37.473 [main] ERROR a.f.a.t.Tool\$ - <unknown>: checker error: Unexpected equality test over types FinFunSet[CellTFrom(Set(Bool)), CellTFrom(Set(Bool))] and CellTFrom(Set((Bool -> Bool)))
at.forsyte.apalache.tla.bmcmt.CheckerException: Unexpected equality test over types FinFunSet[CellTFrom(Set(Bool)), CellTFrom(Set(Bool))] and CellTFrom(Set((Bool -> Bool)))
at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:167)
at at.forsyte.apalache.tla.bmcmt.rules.EqRule.apply(EqRule.scala:55)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:345)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:378)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:412)
at at.forsyte.apalache.tla.bmcmt.rules.NegRule.apply(NegRule.scala:27)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:345)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:378)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:412)
at at.forsyte.apalache.tla.bmcmt.rules.AssignmentRule.apply(AssignmentRule.scala:37)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:345)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:378)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:412)
at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.prepareTransition(TransitionExecutorImpl.scala:106)
at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.prepareTransition(FilteredTransitionExecutor.scala:41)
at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.prepareTransition(ConstrainedTransitionExecutor.scala:97)
at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.\$anonfun\$prepareTransitionsAndCheckInvariants\$5(SeqModelChecker.scala:215)
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:209)
at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:127)
at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:67)
at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:128)
at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:86)
at at.forsyte.apalache.infra.passes.PassChainExecutor.exec\$1(PassChainExecutor.scala:23)
at at.forsyte.apalache.infra.passes.PassChainExecutor.\$anonfun\$run\$5(PassChainExecutor.scala:47)
at scala.util.Either.flatMap(Either.scala:352)
at at.forsyte.apalache.infra.passes.PassChainExecutor.\$anonfun\$run\$3(PassChainExecutor.scala:46)
at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:169)
at scala.collection.LinearSeqOps.foldLeft\$(LinearSeq.scala:165)
at scala.collection.immutable.List.foldLeft(List.scala:79)
at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:41)
at at.forsyte.apalache.tla.Tool\$.runAndExit(Tool.scala:193)
at at.forsyte.apalache.tla.Tool\$.runCheck(Tool.scala:282)
at at.forsyte.apalache.tla.Tool\$.\$anonfun\$run\$3(Tool.scala:136)
at at.forsyte.apalache.tla.Tool\$.\$anonfun\$run\$3\$adapted(Tool.scala:136)
at at.forsyte.apalache.tla.Tool\$.handleExceptions(Tool.scala:440)
at at.forsyte.apalache.tla.Tool\$.runForModule(Tool.scala:430)
at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:136)
at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:48)
at at.forsyte.apalache.tla.Tool.main(Tool.scala)
System information
- Apalache version:
0.25.7 build 554bdb5: - OS:
Windows 10: - JDK version:
18.0.1:
Thanks for the bug report, @craft095! To help us prioritize, could you let us know whether this bug is currently blocking your ability to use Apalache for checking your specs, or are you able to use a workarounds?
IIUC, the key problem here is just that we aren't normalizing the types before running our equality check. We are trying to compare values which of these two types:
FinFunSet[CellTFrom(Set(Bool)), CellTFrom(Set(Bool))]CellTFrom(Set((Bool -> Bool)))
which should be equivalent, afaict.
But we don't have a case for this combination in
https://github.com/informalsystems/apalache/blob/54c8972bbede4f0357de2f717ac54a6ba6b30ec7/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala#L136-L171
so we are falling back to the default error case.
Rather than add special cases to handle these permutations, I think we should ensure the types are normalized to a canonical form before we make these kinds of checks.
This is a missing feature. I would say that is blocked by #1452. Internally, FinFunSet corresponds to a function set that is defined via [ S -> T ]. If we want to compare it to an explicitly constructed set such as { x \in S: CHOOSE y \in T: TRUE }, we would have to expand the set [ S -> T ].
This issue goes to the box of https://github.com/informalsystems/apalache/milestone/56, which requires some systematic refactoring. We plan to do this in Q4.
I see, thank you. Could you help me with workaround? I managed to construct [D -> R] explicitly, but I cannot get types right to make Apalache happy:
---- MODULE Apalache_M0 ----
EXTENDS Naturals, FiniteSets
\* @type: (Set(a), Set(b)) => Set(a -> b);
FSets(D, R) ==
LET
\* @type: Int -> Set(a -> b);
F[n \in 0..Cardinality(D)] ==
IF n = 0
THEN {<<>>}
ELSE
LET
\* @type: Set(a -> b);
F0 == F[n - 1]
\* All functions in F0 have the same domain, choose any one
\* @type: a -> b;
f0 == CHOOSE f \in F0 : TRUE
\* @type: Set(a);
D_smaller == DOMAIN f0
\* @type: a;
d1 == CHOOSE d \in (D \ D_smaller) : TRUE
\* @type: Set(a);
D_bigger == D_smaller \union {d1}
IN
{
[d \in D_bigger |-> IF d \in DOMAIN f THEN f[d] ELSE r]
: f \in F0, r \in R
}
IN
F[Cardinality(D)]
ASSUME
\A d \in SUBSET (0..3) :
\A r \in SUBSET (4..5) :
[d -> r] = FSets(d, r)
====
Log:
# APALACHE version: 0.25.7 | build: 554bdb5 I@12:24:51.712
Checker options: check --out-dir=C:\work\TLA\tlc-qual\.tmp --run-dir=C:\work\TLA\tlc-qual\.tmp --length=5 C:\work\TLA\tlc-qual\draft.sandbox\Let\FunSet\dl\ref\Apalache_M0.tla I@12:24:51.887
Tuning: I@12:24:51.887
PASS #0: SanyParser I@12:24:51.887
Parsing file C:\work\TLA\tlc-qual\draft.sandbox\Let\FunSet\dl\ref\Apalache_M0.tla
Parsing file C:\Users\dkulagin\AppData\Local\Temp\Naturals.tla
Parsing file C:\Users\dkulagin\AppData\Local\Temp\FiniteSets.tla
Parsing file C:\Users\dkulagin\AppData\Local\Temp\__rewire_sequences_in_apalache.tla
Parsing file C:\Users\dkulagin\AppData\Local\Temp\__apalache_folds.tla
PASS #1: TypeCheckerSnowcat I@12:24:52.193
> Running Snowcat .::. I@12:24:52.193
[Apalache_M0.tla:20:34-20:42]: Annotation required. Found 4 matching operator signatures (((a40 -> a41)) => Set(a40)) or ((Seq(a42)) => Set(Int)) or (([]) => Set(Str)) or ((<| |>) => Set(Int)) for argument a102 E@12:24:52.415
[Apalache_M0.tla:20:21-20:42]: Error when computing the type of D_smaller E@12:24:52.426
> Snowcat asks you to fix the types. Meow. I@12:24:52.426
Checker has found an error I@12:24:52.426
It took me 0 days 0 hours 0 min 0 sec I@12:24:52.426
Total time: 0.712 sec I@12:24:52.426
EXITCODE: ERROR (120)
Hi @craft095!
I am trying to reproduce your example. There are several things:
- Multiline LET-IN definitions seem to swallow the type annotations. There is a simple workaround though: Just introduce series of LET-IN definitions, see #1961.
- For some reason, type annotations disappear under recursive functions and
IF-THEN-ELSE, see #1962. This is probably caused by some irregularity in the SANY parser. This needs some investigation.
So for (1), you have an easy workaround. For (2), I am not sure about what's happening. However, even if you fix it, we have dropped support for recursive operators and functions in favor of folds: https://apalache.informal.systems/docs/apalache/principles/recursive.html
@konnov , thank you for hint! I managed to do it with fold:
\* @type: (Set(a), Set(b)) => Set(a -> b);
FSets(D, R) ==
LET
\* Empty function
fe == [x \in D \ D |-> CHOOSE r \in R : TRUE]
\* @type: (Set(a -> b), a) => Set(a -> b);
F(F0, d1) ==
LET
\* All functions in F0 have the same domain, choose any one
\* @type: a -> b;
f0 == CHOOSE f \in F0 : TRUE
\* @type: Set(a);
D_smaller == DOMAIN f0
\* @type: Set(a);
D_bigger == D_smaller \union {d1}
IN
{
[d \in D_bigger |-> IF d /= d1 THEN f[d] ELSE r]
: f \in F0, r \in R
}
IN
ApaFoldSet(F, {fe}, D)