Set filter over SUBSET with uninterpreted types not supported

[edwardcwang]

Description

Using CHOOSE to select a subset from a set of an uninterpreted type with a set filter results in a NotImplementedError.
The same operation over e.g. finite Set(Int) works fine. e.g. CHOOSE T \in SUBSET FiniteIntSet : Cardinality(T) = 4

The same specification works fine with TLC (TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802))

echo -e "SPECIFICATION Spec\nCONSTANT MySet <- MySetTLC\nINVARIANT MyInvariant" > UninterpretedSetSubset.cfg
java -jar tla2tools.jar -config UninterpretedSetSubset.cfg UninterpretedSetSubset.tla

Possibly related: #841

Impact

It's possible to work around by either avoiding uninterpreted types (not always desirable or possible) or with a clunky and verbose workaround like this one:

ps == MySet
p1 == Guess(ps)
p2 == Guess(ps \ {p1})
p3 == Guess(ps \ {p1, p2})
p4 == Guess(ps \ {p1, p2, p3})
ChosenSubset == {p1,p2,p3,p4}

Input specification

\* apalache-mc check --debug --write-intermediate --cinit=MySetInit --inv=MyInvariant UninterpretedSetSubset.tla
\* echo -e "SPECIFICATION Spec\nCONSTANT MySet <- MySetTLC\nINVARIANT MyInvariant" > UninterpretedSetSubset.cfg
\* [tla2tools.jar] -config UninterpretedSetSubset.cfg UninterpretedSetSubset.tla

------------------------------- MODULE UninterpretedSetSubset -------------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Option

VARIABLES
  \* @type: Set(MYTYPE);
  myvar

CONSTANT
  \* @type: Set(MYTYPE);
  MySet

MySetTLC == 1..6
MySetInit ==
  /\ MySet = {"1_OF_MYTYPE", "2_OF_MYTYPE", "3_OF_MYTYPE", "4_OF_MYTYPE", "5_OF_MYTYPE", "6_OF_MYTYPE"}

ChosenSubset == CHOOSE T \in SUBSET MySet : Cardinality(T) = 4

MyInvariant == TRUE

Init ==
  /\ myvar = ChosenSubset

Next ==
  \/ \E v \in myvar: myvar' = myvar \ {v}
  \/ UNCHANGED myvar

Spec ==
  /\ Init
  /\ [][Next]_myvar
=============================================================================

The command line parameters used to run the tool

--debug --write-intermediate --cinit=MySetInit --inv=MyInvariant

Expected behavior

Working specification like TLC, or a purposeful error message to the user explaining why Apalache doesn't support this when TLC does.

Log files

Details

2025-08-26T00:22:09,288 [main] INFO  a.f.a.t.Tool\$ - # APALACHE version: 56462d3 | build: 56462d3
2025-08-26T00:22:09,316 [main] INFO  a.f.a.t.t.o.CheckCmd - Tuning: search.outputTraces=false
2025-08-26T00:22:09,576 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser
2025-08-26T00:22:10,177 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser [OK]
2025-08-26T00:22:10,178 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat
2025-08-26T00:22:10,178 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
2025-08-26T00:22:10,947 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Your types are purrfect!
2025-08-26T00:22:10,947 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > All expressions are typed
2025-08-26T00:22:10,981 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat [OK]
2025-08-26T00:22:10,981 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass
2025-08-26T00:22:10,984 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to Init
2025-08-26T00:22:10,985 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
2025-08-26T00:22:10,985 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the constant initialization predicate to MySetInit
2025-08-26T00:22:10,985 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set an invariant to MyInvariant
2025-08-26T00:22:11,029 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass [OK]
2025-08-26T00:22:11,030 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass
2025-08-26T00:22:11,030 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
2025-08-26T00:22:11,483 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass [OK]
2025-08-26T00:22:11,484 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass
2025-08-26T00:22:11,485 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: Init, InitPrimed, MyInvariant, MySetInit, MySetInitPrimed, Next
2025-08-26T00:22:11,579 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass [OK]
2025-08-26T00:22:11,580 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass
2025-08-26T00:22:11,580 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > Rewriting temporal operators...
2025-08-26T00:22:11,581 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > No temporal property specified, nothing to encode
2025-08-26T00:22:11,592 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass [OK]
2025-08-26T00:22:11,592 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass
2025-08-26T00:22:11,592 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: Init, InitPrimed, MyInvariant, MySetInit, MySetInitPrimed, Next
2025-08-26T00:22:11,610 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass [OK]
2025-08-26T00:22:11,610 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass
2025-08-26T00:22:11,617 [main] INFO  a.f.a.t.p.a.PrimingPassImpl -   > Introducing MySetInitPrimed for MySetInit'
2025-08-26T00:22:11,633 [main] INFO  a.f.a.t.p.a.PrimingPassImpl -   > Introducing InitPrimed for Init'
2025-08-26T00:22:11,644 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass [OK]
2025-08-26T00:22:11,644 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen
2025-08-26T00:22:11,645 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > Producing verification conditions from the invariant MyInvariant
2025-08-26T00:22:11,652 [main] INFO  a.f.a.t.b.VCGenerator -   > VCGen produced 1 verification condition(s)
2025-08-26T00:22:11,663 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen [OK]
2025-08-26T00:22:11,663 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass
2025-08-26T00:22:11,664 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
2025-08-26T00:22:11,683 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
2025-08-26T00:22:11,685 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
2025-08-26T00:22:11,697 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
2025-08-26T00:22:11,708 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
2025-08-26T00:22:11,726 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
2025-08-26T00:22:11,743 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
2025-08-26T00:22:11,764 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
2025-08-26T00:22:11,785 [main] ERROR a.f.a.t.l.s.SourceLocator - No source location for expr@12681: ¬TRUE
2025-08-26T00:22:11,788 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass [OK]
2025-08-26T00:22:11,788 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass
2025-08-26T00:22:11,817 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found 1 initializing transitions
2025-08-26T00:22:11,825 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found 2 transitions
2025-08-26T00:22:11,826 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found constant initializer MySetInit
2025-08-26T00:22:11,831 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Applying unique renaming
2025-08-26T00:22:11,845 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass [OK]
2025-08-26T00:22:11,846 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass
2025-08-26T00:22:11,865 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
2025-08-26T00:22:11,867 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2025-08-26T00:22:11,871 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
2025-08-26T00:22:11,872 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > SetMembershipSimplifier
2025-08-26T00:22:11,874 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2025-08-26T00:22:11,883 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass [OK]
2025-08-26T00:22:11,884 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass
2025-08-26T00:22:11,889 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
2025-08-26T00:22:11,890 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Skolemization
2025-08-26T00:22:11,892 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Expansion
2025-08-26T00:22:11,893 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Remove unused let-in defs
2025-08-26T00:22:11,896 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
2025-08-26T00:22:11,913 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
2025-08-26T00:22:11,913 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass [OK]
2025-08-26T00:22:11,913 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #13: BoundedChecker
2025-08-26T00:22:11,967 [main] DEBUG a.f.a.t.b.s.Z3SolverContext - Creating Z3 solver context 0
2025-08-26T00:22:12,681 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Initializing CONSTANTS
2025-08-26T00:22:12,782 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
2025-08-26T00:22:12,782 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT
2025-08-26T00:22:12,796 [main] ERROR a.f.a.t.Tool\$ - Unhandled exception
scala.NotImplementedError: A set filter over PowSet[Set(MYTYPE)] is not implemented
	at at.forsyte.apalache.tla.bmcmt.rules.SetFilterRule.apply(SetFilterRule.scala:32)
	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.ChooseOrGuessRule.apply(ChooseOrGuessRule.scala:43)
	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.AssignmentRule.apply(AssignmentRule.scala:37)
	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:138)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:91)
	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:136)
	at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:139)
	at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:119)
	at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)

System information

• Apalache version: 56462d3 build 56462d3 (revision 56462d384d63853ceb503c8eb86a4eff02572529 from main branch)
• OS: Ubuntu Linux x86_64 24.04
• JDK version: 21.0.8

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.

[konnov]

This is a known issue, which is hard to solve with the current SMT encoding. As an alternative, I would recommend using Gen:

Init ==
  /\ myvar = Gen(4)
  /\ myvar \in SUBSET MySet

Basically, myvar is initialized with a data structure of the proper type, where each child collection has at most 4 elements. Hence, we have to further constrain the contents of this free data structure.

As you noticed in #3165, this behavior is not equivalent to CHOOSE, as CHOOSE is completely deterministic.