A set filter over PowSet[FinSet[Int]] is not implemented
thpani opened this issue · 0 comments
thpani commented
Spin-out from #878, which contained two reports in a single issue.
Apalache throws A set filter over PowSet[FinSet[Int]] is not implemented
------- MODULE Foo -------
EXTENDS Integers
CONSTANT
\* @type: Set(Int);
S
ConstInit ==
LET ss == SUBSET {1,2}
sss == ss \ {{}}
IN S \in sss
VARIABLE
\* @type: Set(Int);
x
Init ==
x = S
Next ==
UNCHANGED x
Inv ==
x # {}
==========================markus@avocado:~$ apalache check --cinit=ConstInit --inv=Inv Foo
# Tool home: /home/markus/src/TLA/_community/apalache
# Package: /home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.15.9-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -DTLA-Library=/home/markus/src/TLA/_community/apalache/src/tla
#
# APALACHE version 0.15.9-SNAPSHOT build v0.15.8-3-g6a26844
#
# WARNING: This tool is in the experimental stage.
# Please report bugs at: [https://github.com/informalsystems/apalache/issues]
#
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.
Checker options: filename=Foo, init=, next=, inv=Inv I@15:14:36.647
Tuning: I@15:14:37.142
PASS #0: SanyParser I@15:14:37.143
Parsing file /home/markus/src/TLA/_specs/models/tutorials/BlockingQueueTLA/Foo.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/Naturals.tla
PASS #1: TypeCheckerSnowcat I@15:14:37.899
> Running Snowcat .::. I@15:14:37.900
> Your types are great! I@15:14:38.032
> All expressions are typed I@15:14:38.033
PASS #2: ConfigurationPass I@15:14:38.099
> Foo: Loading TLC configuration I@15:14:38.102
> No TLC configuration found. Skipping. I@15:14:38.108
> Command line option --init is not set. Using Init I@15:14:38.108
> Command line option --next is not set. Using Next I@15:14:38.108
> Set the initialization predicate to Init I@15:14:38.109
> Set the constant initialization predicate to ConstInit I@15:14:38.110
> Set the transition predicate to Next I@15:14:38.110
> Set an invariant to Inv I@15:14:38.111
PASS #3: DesugarerPass I@15:14:38.169
> Desugaring... I@15:14:38.176
PASS #4: UnrollPass I@15:14:38.254
> Unroller I@15:14:38.300
PASS #5: PrimingPass I@15:14:38.352
> Introducing ConstInitPrimed for ConstInit' I@15:14:38.361
> Introducing InitPrimed for Init' I@15:14:38.371
PASS #6: CoverAnalysisPass I@15:14:38.410
PASS #7: InlinePass I@15:14:38.419
> InlinerOfUserOper I@15:14:38.426
> LetInExpander I@15:14:38.436
> FoldOperLetinizer I@15:14:38.440
> InlinerOfUserOper I@15:14:38.443
Leaving only relevant operators: ConstInit, ConstInitPrimed, Init, InitPrimed, Inv, Next I@15:14:38.445
PASS #8: VCGen I@15:14:38.507
> Producing verification conditions from the invariant Inv I@15:14:38.508
> VCGen produced 1 verification condition(s) I@15:14:38.520
PASS #9: PreprocessingPass I@15:14:38.566
> Before preprocessing: unique renaming I@15:14:38.567
> Applying standard transformations: I@15:14:38.575
> PrimePropagation I@15:14:38.576
> Desugarer I@15:14:38.621
> UniqueRenamer I@15:14:38.717
> Normalizer I@15:14:38.837
> Keramelizer I@15:14:38.918
> After preprocessing: UniqueRenamer I@15:14:39.033
PASS #10: TransitionFinderPass I@15:14:39.085
> Found 1 initializing transitions I@15:14:39.179
> Found 1 transitions I@15:14:39.182
> Found constant initializer ConstInit I@15:14:39.182
> Applying unique renaming I@15:14:39.185
PASS #11: OptimizationPass I@15:14:39.221
> Applying optimizations: I@15:14:39.263
> ConstSimplifier I@15:14:39.265
> ExprOptimizer I@15:14:39.271
> ConstSimplifier I@15:14:39.275
PASS #12: AnalysisPass I@15:14:39.291
> Marking skolemizable existentials and sets to be expanded... I@15:14:39.294
> SkolemizationMarker I@15:14:39.298
> ExpansionMarker I@15:14:39.301
> Running analyzers... I@15:14:39.311
> Introduced expression grades I@15:14:39.335
> Introduced 0 formula hints I@15:14:39.335
PASS #13: PostTypeCheckerSnowcat I@15:14:39.336
> Running Snowcat .::. I@15:14:39.336
> Your types are great! I@15:14:39.503
> All expressions are typed I@15:14:39.504
PASS #14: BoundedChecker I@15:14:39.526
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],scala.NotImplementedError: A set filter over PowSet[FinSet[Int]] is not implemented)
Unhandled exception E@15:14:39.964
scala.NotImplementedError: A set filter over PowSet[FinSet[Int]] is not implemented
at at.forsyte.apalache.tla.bmcmt.rules.SetFilterRule.apply(SetFilterRule.scala:29)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:336)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:367)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:401)
at at.forsyte.apalache.tla.bmcmt.rules.LetInRule.bindOperator(LetInRule.scala:44)
at at.forsyte.apalache.tla.bmcmt.rules.LetInRule.$anonfun$apply$1(LetInRule.scala:25)
at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
at scala.collection.immutable.List.foldLeft(List.scala:91)
at at.forsyte.apalache.tla.bmcmt.rules.LetInRule.apply(LetInRule.scala:25)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:336)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:367)
at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:401)
at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.initializeConstants(TransitionExecutorImpl.scala:60)
at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.initializeConstants(FilteredTransitionExecutor.scala:96)
at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.initializeConstants(ConstrainedTransitionExecutor.scala:90)
at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:44)
at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:131)
at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:98)
at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:22)
at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:37)
at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:187)
at at.forsyte.apalache.tla.Tool$.$anonfun$run$3(Tool.scala:95)
at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:322)
at at.forsyte.apalache.tla.Tool$.run(Tool.scala:95)
at at.forsyte.apalache.tla.Tool$.main(Tool.scala:45)
at at.forsyte.apalache.tla.Tool.main(Tool.scala)
It took me 0 days 0 hours 0 min 3 sec I@15:14:39.966
Total time: 3.398 sec I@15:14:39.967
EXITCODE: ERROR (255)Originally posted by @lemmy in #878 (comment)