Skip to content

Missing rewriter #3200

New issue
New issue
Open
Open
Missing rewriter#3200
Labels
bugeffort-mediumCan be completed within about 3 daystriagedThe issue has been triaged
@muenchnerkindl

Description

@muenchnerkindl
muenchnerkindl
opened on Oct 26, 2025

Impact

Trying to use Apalache for checking an inductive invariant. Not a big deal
because I already proved it using TLAPS but I thought maybe you'd like to know.

Input specification

-------------------- MODULE KumarTerminationDetection ------------------------
(****************************************************************************)
(* Termination detection algorithm due to D. Kumar as described in          *)
(* Kumar, Devendra. A class of termination detection algorithms for         *)
(* distributed computations. International Conference Foundations of        *)
(* Software Technology and Theoretical Computer Science. New Delhi, India,  *)
(* Springer LNCS 206, pp.73-100, 1985.                                      *)
(*                                                                          *)
(* The algorithm also appears as the "channel counting algorithm" in        *)
(* Mattern, Friedemann. Algorithms for distributed termination detection.   *)
(* Distributed Computing 2.3 (1987):161-175.                                *)
(*                                                                          *)
(* A daemon visits nodes in arbitrary order, waits for the node to become   *)
(* inactive, and then records how many messages the node has sent to and    *)
(* received from every other node. When the daemon sees that all numbers    *)
(* match, it declares that the system has terminated.                       *)
(****************************************************************************)
EXTENDS Naturals 

CONSTANT 
    \* @type: Int;
    N  \* number of nodes
ASSUME NAssumption == N \in Nat

Node == 0 .. N 

VARIABLES 
    \* active[p] is the activation status of p
    \* @type: Int -> Bool;
    active,
    \* sent[p][q] is the number of messages sent from p to q
    \* @type: Int -> (Int -> Int);
    sent,
    \* rcvd[p][q] is the number of messages received by p from q
    \* @type: Int -> (Int -> Int);
    rcvd,
    \* visited is the set of nodes already visited by the daemon
    \* @type: Set(Int);
    visited,
    \* ds[p][q] is the number of messages sent from p to q recorded by the daemon
    \* @type: Int -> (Int -> Int);
    ds,
    \* dr[p][q] is the number of messages received by p from q recorded by the daemon
    \* @type: Int -> (Int -> Int);
    dr

vars == <<active, sent, rcvd, visited, ds, dr>>

(****************************************************************************)
(* The system has globally terminated when all nodes are inactive and when  *)
(* all sent messages have been received.                                    *)
(****************************************************************************)
terminated == 
    /\ \A n \in Node : active[n] = FALSE 
    /\ \A p,q \in Node : sent[p][q] = rcvd[q][p]

TypeOK ==
    /\ active \in [Node -> BOOLEAN]
    /\ sent \in [Node -> [Node -> Nat]]
    /\ rcvd \in [Node -> [Node -> Nat]]
    /\ visited \in SUBSET Node 
    /\ ds \in [Node -> [Node -> Nat]]
    /\ dr \in [Node -> [Node -> Nat]]

(****************************************************************************)
(* The counters recorded by the daemon are consistent for a set Q of nodes  *)
(* if the numbers of sent and received messages agree. When the numbers are *)
(* consistent for all nodes and the daemon has visited all nodes then it    *)
(* declares global termination.                                             *)
(****************************************************************************)
Consistent(Q) ==
    \A p,q \in Q : ds[p][q] = dr[q][p]

terminationDetected == Consistent(Node) /\ visited = Node 

(****************************************************************************)
(* Initially some nodes are active, the daemon has not visited any node,    *)
(* and all counters are initialized to zero.                                *)
(****************************************************************************)
Init == 
    LET zero == [p \in Node |-> [q \in Node |-> 0]]
    IN  /\ active \in [Node -> BOOLEAN]
        /\ visited = {}
        /\ sent = zero 
        /\ rcvd = zero 
        /\ ds = zero 
        /\ dr = zero 

(****************************************************************************)
(* Local termination of a node.                                             *)
(****************************************************************************)
Terminate(n) ==
    /\ active' = [active EXCEPT ![n] = FALSE]
    /\ UNCHANGED <<sent, rcvd, visited, ds, dr>>

(****************************************************************************)
(* Node p sends a message to node q.                                        *)
(****************************************************************************)
Send(p,q) ==
    /\ active[p] = TRUE
    /\ sent' = [sent EXCEPT ![p][q] = @+1]
    /\ UNCHANGED <<active, rcvd, visited, ds, dr>>

(****************************************************************************)
(* Node q receives a message from node p.                                   *)
(****************************************************************************)
Recv(p,q) ==
    /\ sent[p][q] > rcvd[q][p]
    /\ active' = [active EXCEPT ![q] = TRUE]
    /\ rcvd' = [rcvd EXCEPT ![q][p] = @+1]
    /\ UNCHANGED <<sent, visited, ds, dr>>

(****************************************************************************)
(* When termination has not yet been detected, the daemon visits a node n   *)
(* and records its counters provided that n is inactive.                    *)
(****************************************************************************)
Record(n) == 
\*    /\ ~ terminationDetected
    /\ active[n] = FALSE 
    /\ visited' = visited \union {n}
    /\ ds' = [ds EXCEPT ![n] = sent[n]]
    /\ dr' = [dr EXCEPT ![n] = rcvd[n]]
    /\ UNCHANGED <<active, sent, rcvd>> 

(****************************************************************************)
(* The overall specification.                                               *)
(****************************************************************************)
Next == 
    \/ \E n \in Node : Terminate(n) \/ Record(n)
    \/ \E p,q \in Node : Send(p,q) \/ Recv(p,q)

Spec == Init /\ [][Next]_vars /\ \A n \in Node : WF_vars(Record(n))

------------------------------------------------------------------------------
(****************************************************************************)
(* Invariant about counter values:                                          *)
(* - rcvd counters are bounded by the corresponding sent counters,          *)
(* - daemon counters are bounded by the counters of the processes.          *)
(****************************************************************************)
CounterInv == \A p,q \in Node :
    /\ rcvd[q][p] <= sent[p][q]
    /\ ds[p][q] <= sent[p][q]
    /\ dr[p][q] <= rcvd[p][q]

(****************************************************************************)
(* A set Q of nodes is stale if it either contains an active node or some   *)
(* node that has sent or received more messages than the daemon has seen.   *)
(* The following invariant asserts that if a set Q of visited nodes is      *)
(* consistent and stale then some node in Q must have received a message    *)
(* from some node outside Q that was not recorded by the daemon.            *)
(****************************************************************************)
Stale(Q) == \E q \in Q :
    \/ active[q] = TRUE
    \/ \E n \in Node : ds[q][n] # sent[q][n]
    \/ \E n \in Node : dr[q][n] # rcvd[q][n]

StaleInv == \A Q \in SUBSET visited : 
    Consistent(Q) /\ Stale(Q)
    => \E q \in Q : \E n \in Node \ Q : dr[q][n] # rcvd[q][n]

(****************************************************************************)
(* The main correctness property of the algorithm.                          *)
(****************************************************************************)
TDCorrect == terminationDetected => terminated

\* non-invariants
NeverTD == ~ terminationDetected
NeverSent == terminationDetected => \A p,q \in Node : ds[p][q] = 0
------------------------------------------------------------------------------

\* state constraint for TLC: bound number of sent messages
StateConstraint == \A p,q \in Node : sent[p][q] <= 2

\* check inductiveness of StaleInv w.r.t. TypeOK and CounterInv using Apalache
CInit == N=3
StaleInit == TypeOK /\ CounterInv /\ StaleInv

==============================================================================

The command line parameters used to run the tool

--cinit=CInit --init=StaleInit --inv=StaleInv

Expected behavior

Log files

Details 
2025-10-26T17:08:05,633 [main] INFO  a.f.a.t.Tool\$ - # APALACHE version: 0.50.1 | build: cd35919
2025-10-26T17:08:05,644 [main] INFO  a.f.a.t.t.o.CheckCmd - Tuning: search.outputTraces=false
2025-10-26T17:08:05,760 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser
2025-10-26T17:08:05,905 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser [OK]
2025-10-26T17:08:05,905 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat
2025-10-26T17:08:05,905 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
2025-10-26T17:08:06,066 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Your types are purrfect!
2025-10-26T17:08:06,066 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > All expressions are typed
2025-10-26T17:08:06,066 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat [OK]
2025-10-26T17:08:06,066 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass
2025-10-26T17:08:06,069 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to StaleInit
2025-10-26T17:08:06,069 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
2025-10-26T17:08:06,069 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the constant initialization predicate to CInit
2025-10-26T17:08:06,069 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set an invariant to StaleInv
2025-10-26T17:08:06,071 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass [OK]
2025-10-26T17:08:06,071 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass
2025-10-26T17:08:06,071 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
2025-10-26T17:08:06,185 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass [OK]
2025-10-26T17:08:06,185 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass
2025-10-26T17:08:06,186 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInit, CInitPrimed, Next, StaleInit, StaleInitPrimed, StaleInv
2025-10-26T17:08:06,209 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass [OK]
2025-10-26T17:08:06,209 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass
2025-10-26T17:08:06,210 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > Rewriting temporal operators...
2025-10-26T17:08:06,210 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > No temporal property specified, nothing to encode
2025-10-26T17:08:06,210 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass [OK]
2025-10-26T17:08:06,210 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass
2025-10-26T17:08:06,210 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInit, CInitPrimed, Next, StaleInit, StaleInitPrimed, StaleInv
2025-10-26T17:08:06,214 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass [OK]
2025-10-26T17:08:06,214 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass
2025-10-26T17:08:06,215 [main] INFO  a.f.a.t.p.a.PrimingPassImpl -   > Introducing CInitPrimed for CInit'
2025-10-26T17:08:06,217 [main] INFO  a.f.a.t.p.a.PrimingPassImpl -   > Introducing StaleInitPrimed for StaleInit'
2025-10-26T17:08:06,218 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass [OK]
2025-10-26T17:08:06,218 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen
2025-10-26T17:08:06,219 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > Producing verification conditions from the invariant StaleInv
2025-10-26T17:08:06,221 [main] INFO  a.f.a.t.b.VCGenerator -   > VCGen produced 1 verification condition(s)
2025-10-26T17:08:06,222 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen [OK]
2025-10-26T17:08:06,222 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass
2025-10-26T17:08:06,222 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
2025-10-26T17:08:06,225 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
2025-10-26T17:08:06,225 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
2025-10-26T17:08:06,227 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
2025-10-26T17:08:06,231 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
2025-10-26T17:08:06,236 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
2025-10-26T17:08:06,239 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
2025-10-26T17:08:06,247 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
2025-10-26T17:08:06,264 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass [OK]
2025-10-26T17:08:06,264 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass
2025-10-26T17:08:06,273 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found 1 initializing transitions
2025-10-26T17:08:06,275 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found 4 transitions
2025-10-26T17:08:06,275 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found constant initializer CInit
2025-10-26T17:08:06,276 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Applying unique renaming
2025-10-26T17:08:06,279 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass [OK]
2025-10-26T17:08:06,279 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass
2025-10-26T17:08:06,282 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
2025-10-26T17:08:06,282 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2025-10-26T17:08:06,286 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
2025-10-26T17:08:06,290 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > SetMembershipSimplifier
2025-10-26T17:08:06,290 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2025-10-26T17:08:06,294 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass [OK]
2025-10-26T17:08:06,294 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass
2025-10-26T17:08:06,298 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
2025-10-26T17:08:06,298 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Skolemization
2025-10-26T17:08:06,298 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Expansion
2025-10-26T17:08:06,300 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Remove unused let-in defs
2025-10-26T17:08:06,302 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
2025-10-26T17:08:06,305 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
2025-10-26T17:08:06,305 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass [OK]
2025-10-26T17:08:06,306 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #13: BoundedChecker
2025-10-26T17:08:06,317 [main] DEBUG a.f.a.t.b.s.Z3SolverContext - Creating Z3 solver context 0
2025-10-26T17:08:06,887 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Initializing CONSTANTS
2025-10-26T17:08:06,905 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
2025-10-26T17:08:06,905 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT
2025-10-26T17:08:06,923 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - Adapted exception intercepted: 
at.forsyte.apalache.tla.bmcmt.RewriterException: Rewriting for the type FinFunSet[CellTFrom(Set(Int)), FinFunSet[CellTFrom(Set(Int)), InfSet[CellTFrom(Int)]]] is not implemented. Raise an issue.
	at at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick.pick(CherryPick.scala:71)
	at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.skolemExistsByPick(QuantRule.scala:293)
	at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.apply(QuantRule.scala:56)
	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.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:247)
	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.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:247)
	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:192)
	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)
2025-10-26T17:08:06,925 [main] ERROR a.f.a.t.Tool\$ - <unknown>: rewriter error: Rewriting for the type FinFunSet[CellTFrom(Set(Int)), FinFunSet[CellTFrom(Set(Int)), InfSet[CellTFrom(Int)]]] is not implemented. Raise an issue.
at.forsyte.apalache.infra.AdaptedException: <unknown>: rewriter error: Rewriting for the type FinFunSet[CellTFrom(Set(Int)), FinFunSet[CellTFrom(Set(Int)), InfSet[CellTFrom(Int)]]] is not implemented. Raise an issue.
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:39)
	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: 0.50.1 build cd35919
  • OS: Mac OS X
  • JDK version: 21.0.2

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugeffort-mediumCan be completed within about 3 daystriagedThe issue has been triaged

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions