Bogus error with mutual recursive operators

[lemmy]

Apalache claims that TLA+ parser rejects (Error by TLA+ parser: Found a cyclic dependency among operators: IsEven, IsOdd) a spec that it doesn't:

---- MODULE F ----
EXTENDS Naturals

RECURSIVE IsEven(_)

RECURSIVE IsOdd(_)

IsEven(n) ==
    IF n = 0
    THEN TRUE
    ELSE IsOdd(n-1)

IsOdd(n) ==
    IF n = 0
    THEN FALSE
    ELSE IsEven(n-1)

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

java -cp ~/TLC/tla2tools_1-7-0.jar tla2sany.SANY F.tla

****** SANY2 Version 2.1 created 24 February 2014

Parsing file /Users/markus/src/TLA/_specs/ewd998/F.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module F

apalache-mc check F.tla                               
16:46:05.965 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd - Loading configuration
16:46:05.984 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -   > TLC config file found in specification directory. To enable it, pass --config=F.cfg.
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Output directory: /Users/markus/src/TLA/_specs/ewd998/_apalache-out/F.tla/2022-10-11T16-46-06_16504550803085844238
# APALACHE version: 0.29.2 | build: 8a342d2                       I@16:46:06.168
Tuning: search.outputTraces=false                                 I@16:46:06.186
PASS #0: SanyParser                                               I@16:46:06.323
Parsing file /Users/markus/src/TLA/_specs/ewd998/F.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Naturals.tla
Check the dependency graph in dependencies.dot. You can view it with graphviz. E@16:46:06.453
Error by TLA+ parser: Found a cyclic dependency among operators: IsEven, IsOdd E@16:46:06.455
It took me 0 days  0 hours  0 min  0 sec                          I@16:46:06.455
Total time: 0.285 sec                                             I@16:46:06.455
EXITCODE: ERROR (255)

[konnov]

Right. In this case, it is not the parser issue. What would be an optimal message in your opinion?

[lemmy]

"Apalache does not support recursive operators"

[thpani]

The current error message both indicates where Apalache fails (we detect cyclic dependencies in Apalache's parser pass), and gives a witness for the mutual recursion.

@lemmy Is your concern that the existing error message is too detailed, or that users might confuse the language fragment accepted by Apalache with SANY's capabilities?

[lemmy]

The point is that this is not a "TLA+ parser" (SANY) error, because (mutual) recursion in TLA+ is perfectly fine.

[thpani]

I asked because other constructs, such as Apalache's overrides, can cause cyclic dependencies that Apalache rejects in the same way.
So we cannot make the error message about recursive operators.

IIUC, simply dropping the Error by TLA+ parser: prefix from this error message would resolve this issue?

[lemmy]

Based on the critique TLC receives for its poor error messages, I suggest telling Apalache's overrides apart from recursively declared operators in Apalache's error reporting.

[thpani]

That's good input, improving Apalache's output is something we take very serious!

In the current case, the example you reported is at the intersection of two language fragments that Apalache rejects: (1) cyclic use-defs and (2) recursion. It is simply a matter of what is checked first.
We could change that order, but I think it's quite obvious here that Found a cyclic dependency among operators: IsEven, IsOdd refers to mutual recursion. Support of recursion in Apalache is discussed at length in the manual: https://apalache.informal.systems/docs/apalache/principles/recursive.html

I also understood that this issue is really about identifying "TLA+ parser" with SANY, to which I offered a pragmatic solution above. I'd still appreciate your feedback there:

IIUC, simply dropping the Error by TLA+ parser: prefix from this error message would resolve this issue?

[shonfeder]

In #2242, these errors will instead be prefixed with Parse error and so not unfairly malign SANY :)

[thpani]

Closing this as fixed by #2242. If not, please reopen.