Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
lemmy opened this issue · 0 comments
lemmy commented
https://apalache-mc.org/docs/adr/006rfc-unit-testing.html?highlight=gen(#51-using-apalache-generators advises to conjoin TypeOK to the predicate involving the Gen operator.
---- MODULE Foobar ----
EXTENDS Apalache, Integers
VARIABLE
\* @type: { p : Set({ q : Set(Int) }) };
v
TypeOK ==
v \in [ p: SUBSET [ q: SUBSET Int ] ] \* Infinite sets such as Int trigger the error.
Init ==
/\ v = [ p |-> {[ q |-> { 1 } ]} ]
/\ TypeOK \* Conjoining TypeOK triggers the error.
GenInit ==
/\ v = Gen(1)
/\ TypeOK \* Conjoining TypeOK triggers the error.
Next ==
UNCHANGED v
====Init
-> % ~/apalache/apalache-0.45.3/bin/apalache-mc check --init=Init --next=Next Foobar.tla
17:37:44.762 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- Loading configuration
17:37:44.787 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- > TLC config file found in specification directory. To enable it, pass --config=Foobar.cfg.
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.
Output directory: /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/Foobar.tla/2024-08-27T17-37-44_41841269002290680
# APALACHE version: 0.45.3 | build: 0b3ae56 I@17:37:44.978
Tuning: search.outputTraces=false I@17:37:45.006
PASS #0: SanyParser I@17:37:45.146
Parsing file /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/Foobar.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Apalache.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Integers.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Naturals.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__rewire_sequences_in_apalache.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__apalache_folds.tla
PASS #1: TypeCheckerSnowcat I@17:37:45.331
> Running Snowcat .::. I@17:37:45.331
> Your types are purrfect! I@17:37:45.501
> All expressions are typed I@17:37:45.501
PASS #2: ConfigurationPass I@17:37:45.501
> Set the initialization predicate to Init I@17:37:45.503
> Set the transition predicate to Next I@17:37:45.503
PASS #3: DesugarerPass I@17:37:45.505
> Desugaring... I@17:37:45.505
PASS #4: InlinePass I@17:37:45.516
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next I@17:37:45.516
PASS #5: TemporalPass I@17:37:45.530
> Rewriting temporal operators... I@17:37:45.530
> No temporal property specified, nothing to encode I@17:37:45.530
PASS #6: InlinePass I@17:37:45.530
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next I@17:37:45.530
PASS #7: PrimingPass I@17:37:45.531
> Introducing InitPrimed for Init' I@17:37:45.532
PASS #8: VCGen I@17:37:45.672
> No invariant given. Only deadlocks will be checked I@17:37:45.672
PASS #9: PreprocessingPass I@17:37:45.672
> Before preprocessing: unique renaming I@17:37:45.672
> Applying standard transformations: I@17:37:45.677
> PrimePropagation I@17:37:45.677
> Desugarer I@17:37:45.678
> UniqueRenamer I@17:37:45.678
> Normalizer I@17:37:45.679
> Keramelizer I@17:37:45.680
> After preprocessing: UniqueRenamer I@17:37:45.683
PASS #10: TransitionFinderPass I@17:37:45.686
> Found 1 initializing transitions I@17:37:45.695
> Found 1 transitions I@17:37:45.695
> No constant initializer I@17:37:45.695
> Applying unique renaming I@17:37:45.696
PASS #11: OptimizationPass I@17:37:45.697
> Applying optimizations: I@17:37:45.701
> ConstSimplifier I@17:37:45.702
> ExprOptimizer I@17:37:45.702
> SetMembershipSimplifier I@17:37:45.704
> ConstSimplifier I@17:37:45.704
PASS #12: AnalysisPass I@17:37:45.705
> Marking skolemizable existentials and sets to be expanded... I@17:37:45.706
> Skolemization I@17:37:45.707
> Expansion I@17:37:45.707
> Remove unused let-in defs I@17:37:45.707
> Running analyzers... I@17:37:45.709
> Introduced expression grades I@17:37:45.710
PASS #13: BoundedChecker I@17:37:45.710
<unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)] E@17:37:46.491
at.forsyte.apalache.infra.AdaptedException: <unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:39)
at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:135)
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)
Please report an issue at [https://github.com/informalsystems/apalache/issues]: at.forsyte.apalache.infra.AdaptedException: <unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
A bug report template has been generated at [/Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/Foobar.tla/2024-08-27T17-37-44_41841269002290680/BugReport.md].
If you choose to use it, please complete the template with a description of the expected behavior and impact.
It took me 0 days 0 hours 0 min 1 sec I@17:37:46.496
Total time: 1.504 sec I@17:37:46.496
EXITCODE: ERROR (255)GenInit
-> % ~/apalache/apalache-0.45.3/bin/apalache-mc check --init=GenInit --next=Next Foobar.tla
17:38:42.548 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- Loading configuration
17:38:42.573 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- > TLC config file found in specification directory. To enable it, pass --config=Foobar.cfg.
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.
Output directory: /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/Foobar.tla/2024-08-27T17-38-42_12136351957546524448
# APALACHE version: 0.45.3 | build: 0b3ae56 I@17:38:42.761
Tuning: search.outputTraces=false I@17:38:42.781
PASS #0: SanyParser I@17:38:42.913
Parsing file /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/Foobar.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Apalache.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Integers.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Naturals.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__rewire_sequences_in_apalache.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__apalache_folds.tla
PASS #1: TypeCheckerSnowcat I@17:38:43.099
> Running Snowcat .::. I@17:38:43.099
> Your types are purrfect! I@17:38:43.260
> All expressions are typed I@17:38:43.260
PASS #2: ConfigurationPass I@17:38:43.261
> Set the initialization predicate to GenInit I@17:38:43.262
> Set the transition predicate to Next I@17:38:43.263
PASS #3: DesugarerPass I@17:38:43.265
> Desugaring... I@17:38:43.265
PASS #4: InlinePass I@17:38:43.273
Leaving only relevant operators: CInitPrimed, GenInit, GenInitPrimed, Next I@17:38:43.273
PASS #5: TemporalPass I@17:38:43.289
> Rewriting temporal operators... I@17:38:43.290
> No temporal property specified, nothing to encode I@17:38:43.290
PASS #6: InlinePass I@17:38:43.290
Leaving only relevant operators: CInitPrimed, GenInit, GenInitPrimed, Next I@17:38:43.290
PASS #7: PrimingPass I@17:38:43.291
> Introducing GenInitPrimed for GenInit' I@17:38:43.292
PASS #8: VCGen I@17:38:43.434
> No invariant given. Only deadlocks will be checked I@17:38:43.434
PASS #9: PreprocessingPass I@17:38:43.434
> Before preprocessing: unique renaming I@17:38:43.434
> Applying standard transformations: I@17:38:43.438
> PrimePropagation I@17:38:43.439
> Desugarer I@17:38:43.439
> UniqueRenamer I@17:38:43.439
> Normalizer I@17:38:43.440
> Keramelizer I@17:38:43.441
> After preprocessing: UniqueRenamer I@17:38:43.443
PASS #10: TransitionFinderPass I@17:38:43.446
> Found 1 initializing transitions I@17:38:43.454
> Found 1 transitions I@17:38:43.454
> No constant initializer I@17:38:43.455
> Applying unique renaming I@17:38:43.455
PASS #11: OptimizationPass I@17:38:43.456
> Applying optimizations: I@17:38:43.461
> ConstSimplifier I@17:38:43.461
> ExprOptimizer I@17:38:43.462
> SetMembershipSimplifier I@17:38:43.463
> ConstSimplifier I@17:38:43.464
PASS #12: AnalysisPass I@17:38:43.464
> Marking skolemizable existentials and sets to be expanded... I@17:38:43.466
> Skolemization I@17:38:43.466
> Expansion I@17:38:43.466
> Remove unused let-in defs I@17:38:43.467
> Running analyzers... I@17:38:43.468
> Introduced expression grades I@17:38:43.469
PASS #13: BoundedChecker I@17:38:43.469
<unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)] E@17:38:44.247
at.forsyte.apalache.infra.AdaptedException: <unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:39)
at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:135)
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)
Please report an issue at [https://github.com/informalsystems/apalache/issues]: at.forsyte.apalache.infra.AdaptedException: <unknown>: checker error: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
A bug report template has been generated at [/Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/Foobar.tla/2024-08-27T17-38-42_12136351957546524448/BugReport.md].
If you choose to use it, please complete the template with a description of the expected behavior and impact.
It took me 0 days 0 hours 0 min 1 sec I@17:38:44.252
Total time: 1.486 sec I@17:38:44.252
EXITCODE: ERROR (255)Exception
at.forsyte.apalache.tla.bmcmt.CheckerException: Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)]
at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:171)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.fieldsEq\$1(LazyEquality.scala:532)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.\$anonfun\$mkRowRecordEq\$1(LazyEquality.scala:536)
at scala.collection.StrictOptimizedIterableOps.map(StrictOptimizedIterableOps.scala:100)
at scala.collection.StrictOptimizedIterableOps.map\$(StrictOptimizedIterableOps.scala:87)
at scala.collection.immutable.TreeSet.map(TreeSet.scala:39)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.mkRowRecordEq(LazyEquality.scala:536)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:155)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.makeOne\$1(LazyEquality.scala:107)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.\$anonfun\$cacheEqConstraints\$2(LazyEquality.scala:110)
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.tla.bmcmt.LazyEquality.cacheEqConstraints(LazyEquality.scala:110)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.subsetEq(LazyEquality.scala:318)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.mkSetEq(LazyEquality.scala:247)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:145)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.fieldsEq\$1(LazyEquality.scala:532)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.\$anonfun\$mkRowRecordEq\$1(LazyEquality.scala:536)
at scala.collection.StrictOptimizedIterableOps.map(StrictOptimizedIterableOps.scala:100)
at scala.collection.StrictOptimizedIterableOps.map\$(StrictOptimizedIterableOps.scala:87)
at scala.collection.immutable.TreeSet.map(TreeSet.scala:39)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.mkRowRecordEq(LazyEquality.scala:536)
at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:155)
at at.forsyte.apalache.tla.bmcmt.rules.EqRule.apply(EqRule.scala:55)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.skolemExistsByPick(QuantRule.scala:300)
at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.apply(QuantRule.scala:53)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
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:251)
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:357)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
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:217)
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:211)
at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:123)
at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:62)
at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:128)
at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:81)
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:360)
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:135)
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)