[BUG] Unroller produces stack overflow due to a bug in SANY

[konnov]

Following #67, we tried to run the unstable version against the light client spec as follows:

apalache-mc check --config=MC3-PrecisionInv.cfg MC2nodes3blocks.tla

Blockchain.tla contains a recursive operator PowerOfSet, which we did not have produce annotations for. The tool should have complained about missing annotations. Instead, it throws a stack overflow:

PASS #1: ConfigurationPass                                        I@11:30:37.199
  > Loading TLC configuration from MC2nodes3blocks.tla            I@11:30:37.201
  > Could not parse TLC configuration in MC2nodes3blocks.tla: unexpected character E@11:30:37.238
PASS #2: UnrollPass                                               I@11:30:37.297
  > Unroller                                                      I@11:30:37.299
PASS #3: InlinePass                                               I@11:30:37.325
  > InlinerOfUserOper                                             I@11:30:37.327
(Please report an issue at: [https://github.com/konnov/apalache/issues],java.lang.StackOverflowError)
Unhandled exception                                               E@11:30:37.576
java.lang.StackOverflowError: null
	at scala.collection.immutable.HashMap.get(HashMap.scala:53)
	at at.forsyte.apalache.tla.lir.transformations.standard.InlinerOfUserOper.$anonfun$transform$1(InlinerOfUserOper.scala:34)

[Kukovec]

The issue is not with Unroller but with INSTANCE-imported recursive operators not being marked recursive (i.e. having .isRecursive = false). See attached minimal example.

[Kukovec]

test.txt

[konnov]

@Kukovec do you know whether this has been fixed?

[konnov]

This is still an issue. For the moment, we will introduce a workaround. This should have been fixed in SANY, but we have to check that.

[Kukovec]

Redirecting this to @konnov, since it's not an Unroller issue.

[konnov]

We should reproduce it again and submit to tlaplus, if the bug is still there.

[konnov]

We are going to stop supporting recursive operators and functions. The users should use folds instead. Closing this issue.

[thpani]

Reopening, there's still clean-up notes for this:

https://github.com/informalsystems/apalache/blob/91ad7b4edff727f1e8579ca5b2fac1ac2c41bb15/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/ModuleTranslator.scala#L89-L91

https://github.com/informalsystems/apalache/blob/91ad7b4edff727f1e8579ca5b2fac1ac2c41bb15/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterInstances.scala#L351-L353