[BUG] Stack overflow when checking model

[dwwmmn]

Describe the bug
See attached trace. Doesn't seem to be related to #18 but I'm not sure.

detailed.log

To Reproduce
Unfortunately I can't provide the specification. Hopefully this issue is still helpful and not just annoying... if more information is really needed I could maybe replace some names and post excerpts.

Desktop (please complete the following information):
Docker on Ubuntu 18.04:

apalache/mc                             latest                                       dbcd1f597a4f        3 weeks ago         954MB

[konnov]

Thanks for your report! We will try to see how this stack overflow could happen.

[konnov]

Just trying to figure out, how this could happen. Do you use recursive operators or recursive functions in your spec?

[dwwmmn]

Yes, there is a recursive function.

[konnov]

We are adding support for recursive operators, see #67. The recursive functions are harder to support than we thought, see #84. In any case, the tool should not produce stack overflow.

[dwwmmn]

I was curious to see if the tool worked without recursive functions, so I tried running on an older version of the specification and got a really surprising error. In this older version, the only recursive function left was defined as such:

RECURSIVE Sum(_)
Sum(seq) == IF Len(seq) = 0 THEN 0 ELSE Head(seq) + Sum(Tail(seq))

I simply commented out the definition and some properties which used it and ran Apalache. This was the result:

user@host:~/Desktop$ alias
alias apalache='docker run --rm -v /home/user/Desktop:/var/apalache apalache/mc'
 
user@host:~/Desktop$ apalache check --debug phase5b.tla
Assuming you bind-mounted your local directory into /var/apalache...
# Tool home: /opt/apalache
# Package:   /opt/apalache/mod-distribution/target/apalache-pkg-0.6.1-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -Djava.library.path=/opt/apalache/3rdparty/lib
#
Picked up _JAVA_OPTIONS: -Djdk.net.URLClassPath.disableClassPathURLCheck=true
# APALACHE version 0.6.1-SNAPSHOT build v0.6.0-10-g6ef08e1
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/konnov/apalache/issues]
 
Checker options: filename=phase5b.tla, init=Init, next=Next, inv= I@19:36:02.956
PASS #0: SanyParser                                               I@19:36:04.591
Parsing file /var/apalache/phase5b.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Bags.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Naturals.tla
(This should not have happened, but it did. REPORT IT: [https://github.com/konnov/apalache/issues],at.forsyte.apalache.tla.imp.SanyImporterException: User operator Sum is not found in the translation context: line 80, col 5 to line 80, col 56 of module Bags)
Unhandled exception                                               E@19:36:06.014
at.forsyte.apalache.tla.imp.SanyImporterException: User operator Sum is not found in the translation context: line 80, col 5 to line 80, col 56 of module Bags
        at at.forsyte.apalache.tla.imp.OpApplTranslator.translateNonRec$1(OpApplTranslator.scala:82)
        at at.forsyte.apalache.tla.imp.OpApplTranslator.translateUserOperator(OpApplTranslator.scala:98)
        at at.forsyte.apalache.tla.imp.OpApplTranslator.translate(OpApplTranslator.scala:50)
        at at.forsyte.apalache.tla.imp.ExprOrOpArgNodeTranslator.translate(ExprOrOpArgNodeTranslator.scala:33)
        at at.forsyte.apalache.tla.imp.OpApplTranslator.mkBoundCtorBuiltin(OpApplTranslator.scala:313)
        at at.forsyte.apalache.tla.imp.OpApplTranslator.translateBuiltin(OpApplTranslator.scala:183)
        at at.forsyte.apalache.tla.imp.OpApplTranslator.translate(OpApplTranslator.scala:44)
        at at.forsyte.apalache.tla.imp.ExprOrOpArgNodeTranslator.translate(ExprOrOpArgNodeTranslator.scala:33)
        at at.forsyte.apalache.tla.imp.OpDefTranslator.translate(OpDefTranslator.scala:37)
        at at.forsyte.apalache.tla.imp.ModuleTranslator.eachOpDefSecondPass$1(ModuleTranslator.scala:56)
        at at.forsyte.apalache.tla.imp.ModuleTranslator.$anonfun$translate$4(ModuleTranslator.scala:64)
        at at.forsyte.apalache.tla.imp.ModuleTranslator.$anonfun$translate$4$adapted(ModuleTranslator.scala:64)
        at scala.collection.immutable.List.foreach(List.scala:378)
        at at.forsyte.apalache.tla.imp.ModuleTranslator.translate(ModuleTranslator.scala:64)
        at at.forsyte.apalache.tla.imp.SanyImporter.$anonfun$loadFromFile$1(SanyImporter.scala:39)
        at scala.collection.mutable.ArrayOps$ofRef.foldLeft(ArrayOps.scala:193)
        at at.forsyte.apalache.tla.imp.SanyImporter.loadFromFile(SanyImporter.scala:38)
        at at.forsyte.apalache.tla.imp.passes.SanyParserPassImpl.execute(SanyParserPassImpl.scala:42)
        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:118)
        at at.forsyte.apalache.tla.Tool$.$anonfun$main$2(Tool.scala:57)
        at at.forsyte.apalache.tla.Tool$.$anonfun$main$2$adapted(Tool.scala:57)
        at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:167)
        at at.forsyte.apalache.tla.Tool$.main(Tool.scala:57)
        at at.forsyte.apalache.tla.Tool.main(Tool.scala)
It took me 0 days  0 hours  0 min  3 sec                          I@19:36:06.020
Total time: 3.274 sec                                             I@19:36:06.020

I almost opened an issue because it seems like a completely different problem, but what is the likelihood of the two problem operators having the same name?!

Another thing - I can't seem to find a good way to extract /tmp/Bags.tla from the container so I'm not sure what line 80, col 5 to line 80, col 56 of module Bags looks like. Is Bags.tla supported?

[konnov]

That seems to be related to #49, as Bags.tla is calling the local operator called Sum.

We have added support for recursive operators. This needs some annotations.

For the Bags module, we don't support it yet. But it should be relatively easy to add Bags. See #128.

[konnov]

It looks like the main issue was about Bags. We still have them planned in #128. But it looks like we have the prerequisites to implement Bags, at least, some of their operators. I will close this issue. If you are interested in progress, tune to #128.