[BUG] Recursive operator doesn't work

[andrey-kuprianov]

I wanted to define a recursive operator that computes a sum over a set of integers; this results in an unhandled exception:

---------------------------- MODULE sum --------------------------
EXTENDS Integers, FiniteSets

(* APALACHE *)
a <: b == a

RECURSIVE SumReduce(_, _)
SumReduce(S, value) == IF S = ({}<:{Int}) THEN value
                              ELSE LET s == CHOOSE s \in S : TRUE
                              IN SumReduce(S \ {s}, s + value)

Sum(S) == SumReduce(S, 0)
         
UNROLL_TIMES_SumReduce == 3
UNROLL_DEFAULT_SumReduce == 0

VARIABLE
  set,
  sum

Init ==
  /\ set = {1,2,3}
  /\ sum = 0

Next ==
  /\ sum' = Sum(set)
  /\ UNCHANGED(<<set>>)

Inv == sum = 0 \/ sum = 6 

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

Command-line parameters:

apalache-mc --debug check --inv=Inv sum.tla

Tool output

# Tool home: /home/andrey/tools/apalache
# Package:   /home/andrey/tools/apalache/mod-distribution/target/apalache-pkg-0.7.3-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -DTLA-Library=/home/andrey/tools/apalache/src/tla
#
# APALACHE version 0.7.3-SNAPSHOT build v0.7.0-62-gb643cc4
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]

Checker options: filename=sum.tla, init=, next=, inv=Inv          I@10:39:23.918
PASS #0: SanyParser                                               I@10:39:24.411
Parsing file /home/andrey/Documents/Verification/TLA+Blog/001-choose/sum.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
PASS #1: ConfigurationPass                                        I@10:39:24.882
  > Loading TLC configuration from sum.cfg                        I@10:39:24.883
  > No TLC configuration found. Skipping.                         I@10:39:24.888
PASS #2: UnrollPass                                               I@10:39:24.935
  > Unroller                                                      I@10:39:24.944
PASS #3: InlinePass                                               I@10:39:25.048
  > InlinerOfUserOper                                             I@10:39:25.049
  > LetInExpander                                                 I@10:39:25.066
PASS #4: PrimingPass                                              I@10:39:25.109
  > Introducing InitPrimed for Init'                              I@10:39:25.112
PASS #5: VCGen                                                    I@10:39:25.132
  > Producing verification conditions from the invariant Inv      I@10:39:25.133
  > VCGen produced 1 verification condition(s)                    I@10:39:25.134
PASS #6: PreprocessingPass                                        I@10:39:25.175
  > Before preprocessing: unique renaming                         I@10:39:25.175
 > Applying standard transformations:                             I@10:39:25.191
  > Desugarer                                                     I@10:39:25.192
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],at.forsyte.apalache.tla.lir.UnexpectedLanguageError: Predicate FlatLanguagePred does not accept the expression: LET t_1 ≜ LET t_1 ≜ LET t_1 ≜ LET t_1 ≜ 0 IN IF ((((S ∖ {s()}) ∖ {s()}) ∖ {s()}) = (BMC!<:({}, {Int}))) THEN (s() + (s() + (s() + value))) ELSE LET s ≜ CHOOSE s ∈ (((S ∖ {s()}) ∖ {s()}) ∖ {s()}) : TRUE IN t_1() IN IF (((S ∖ {s()}) ∖ {s()}) = (BMC!<:({}, {Int}))) THEN (s() + (s() + value)) ELSE LET s ≜ CHOOSE s ∈ ((S ∖ {s()}) ∖ {s()}) : TRUE IN t_1() IN IF ((S ∖ {s()}) = (BMC!<:({}, {Int}))) THEN (s() + value) ELSE LET s ≜ CHOOSE s ∈ (S ∖ {s()}) : TRUE IN t_1() IN IF (S = (BMC!<:({}, {Int}))) THEN value ELSE LET s ≜ CHOOSE s ∈ S : TRUE IN t_1())
Unhandled exception                                               E@10:39:25.207
at.forsyte.apalache.tla.lir.UnexpectedLanguageError: Predicate FlatLanguagePred does not accept the expression: LET t_1 ≜ LET t_1 ≜ LET t_1 ≜ LET t_1 ≜ 0 IN IF ((((S ∖ {s()}) ∖ {s()}) ∖ {s()}) = (BMC!<:({}, {Int}))) THEN (s() + (s() + (s() + value))) ELSE LET s ≜ CHOOSE s ∈ (((S ∖ {s()}) ∖ {s()}) ∖ {s()}) : TRUE IN t_1() IN IF (((S ∖ {s()}) ∖ {s()}) = (BMC!<:({}, {Int}))) THEN (s() + (s() + value)) ELSE LET s ≜ CHOOSE s ∈ ((S ∖ {s()}) ∖ {s()}) : TRUE IN t_1() IN IF ((S ∖ {s()}) = (BMC!<:({}, {Int}))) THEN (s() + value) ELSE LET s ≜ CHOOSE s ∈ (S ∖ {s()}) : TRUE IN t_1() IN IF (S = (BMC!<:({}, {Int}))) THEN value ELSE LET s ≜ CHOOSE s ∈ S : TRUE IN t_1()
	at at.forsyte.apalache.tla.lir.transformations.LanguageWatchdog.check(LanguageWatchdog.scala:18)
	at at.forsyte.apalache.tla.pp.Desugarer.apply(Desugarer.scala:25)
	at at.forsyte.apalache.tla.pp.Desugarer.apply(Desugarer.scala:22)
	at at.forsyte.apalache.tla.lir.transformations.standard.ModuleByExTransformer.$anonfun$apply$1(ModuleByExTransformer.scala:15)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:285)
	at scala.collection.immutable.List.foreach(List.scala:431)
	at scala.collection.generic.TraversableForwarder.foreach(TraversableForwarder.scala:38)
	at scala.collection.generic.TraversableForwarder.foreach$(TraversableForwarder.scala:38)
	at scala.collection.mutable.ListBuffer.foreach(ListBuffer.scala:47)
	at scala.collection.TraversableLike.map(TraversableLike.scala:285)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:278)
	at scala.collection.AbstractTraversable.map(Traversable.scala:108)
	at at.forsyte.apalache.tla.lir.transformations.standard.ModuleByExTransformer.apply(ModuleByExTransformer.scala:23)
	at at.forsyte.apalache.tla.lir.transformations.standard.ModuleByExTransformer.apply(ModuleByExTransformer.scala:11)
	at at.forsyte.apalache.tla.pp.passes.PreproPassImpl.$anonfun$execute$1(PreproPassImpl.scala:64)
	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.pp.passes.PreproPassImpl.execute(PreproPassImpl.scala:61)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:23)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:38)
	at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:147)
	at at.forsyte.apalache.tla.Tool$.$anonfun$run$2(Tool.scala:81)
	at at.forsyte.apalache.tla.Tool$.$anonfun$run$2$adapted(Tool.scala:81)
	at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:196)
	at at.forsyte.apalache.tla.Tool$.run(Tool.scala:81)
	at at.forsyte.apalache.tla.Tool$.main(Tool.scala:42)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)
It took me 0 days  0 hours  0 min  1 sec                          I@10:39:25.209
Total time: 1.342 sec                                             I@10:39:25.209
EXITCODE: ERROR (99)

Log files
detailed.log

[konnov]

@Kukovec do you like to investigate?