A set filter over PowSet[FinSet[Int]] is not implemented

[thpani]

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)