Fix handling of constant operators

[BGR360]

Fixes #2388
Closes #709

If this approach seems good to folks, I can clean it up and make this a not-so-draft PR. This fixes the issue for the two specs I posted in the original issue, but I have no idea if it's a really robust fix or not.

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entries added to ./unreleased/ for any new functionality

[codecov-commenter]

Codecov Report

Merging #2389 (3b6b03e) into main (64ca9bc) will decrease coverage by 0.02%.
The diff coverage is 50.00%.

@@            Coverage Diff             @@
##             main    #2389      +/-   ##
==========================================
- Coverage   78.35%   78.34%   -0.02%     
==========================================
  Files         441      441              
  Lines       15387    15388       +1     
  Branches     2464     2439      -25     
==========================================
- Hits        12057    12056       -1     
- Misses       3330     3332       +2     

Impacted Files	Coverage Δ
...at/forsyte/apalache/tla/imp/OpApplTranslator.scala	94.88% <50.00%> (-0.33%)	⬇️
...a/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala	93.75% <0.00%> (-2.09%)	⬇️

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

[konnov]

That's a neat solution! I thought it would require more effort to translate constant operators, though it has been a while since I have look at SanyImporter.

It looks good to me. The only thing is that logger.debug may produce lots of debugging messages. Perhaps, it's worth changing the logging level to TRACE. Could you also add a changelog entry. Apart from that, looks like to ready for review for me.

[Kukovec]

Also:
closes #709

[BGR360]

How does one enable TRACE-level logging when trying to debug things? The only documented thing I found was the --debug CLI flag.

Regardless, I didn't really intend to keep those log messages in. I just pushed the PR late at night as soon as I had fixed my problem lol

[thpani]

Hi @BGR360, thanks a lot for the excellent contribution!

If we can address the open comments, I think this is good to be merged!

Ben, would you like to see this across the finish line?

[thpani]

How does one enable TRACE-level logging when trying to debug things? The only documented thing I found was the --debug CLI flag.

Logback configuration is programmatic in LogbackConfigurator. We're current cutting off messages at DEBUG:

https://github.com/informalsystems/apalache/blob/4f9c17d86bf564e18f1a079d17a1d5b3d08820e8/mod-infra/src/main/scala/at/forsyte/apalache/infra/log/LogbackConfigurator.scala#L47-L49

But I think it's fine to remove these log messages before merging, as you suggested.

[BGR360]

Thanks for the review @thpani !

Ben, would you like to see this across the finish line?

I'm happy to, but it'll be on my own time, whenever I get to it. Perhaps this weekend. If you're offering to take it off my hands and push it through yourself, be my guest!!

Though I think this PR can't be called complete until we test whether it actually functions as expected (that you can substitute the higher-order operator when instantiating a spec and it works properly). Currently I've only tested the typechecking.

[thpani]

I'm happy to, but it'll be on my own time, whenever I get to it.

Let's do it! This is not super urgent on our side, and we're happy to see external contributions 😃
Let us know if you need any help or guidance @BGR360!

this PR can't be called complete until we test whether it actually functions as expected

Ah yes, I actually did a full instantiation of your integration test to make sure it passes model-checking. We should include something similar in this PR!

[thpani]

This is awesome, thanks a lot Ben!

I've made some small polishing changes, so @konnov @Kukovec PTAL!

(I also tried to add a test for a 2nd-order CONSTANT, but it does not seem to parse through SANY. So I'd leave it at this.)

[BGR360]

(I also tried to add a test for a 2nd-order CONSTANT, but it does not seem to parse through SANY. So I'd leave it at this.)

@thpani What do you mean by this? Something like this?

CONSTANTS
    \* @type: (Int, (Int) => Bool) => Bool;
    MapInt(_, MapFn(_))

[konnov]

This is awesome, thanks a lot Ben!

I've made some small polishing changes, so @konnov @Kukovec PTAL!

Looks great! Thanks a lot @BGR360 and @thpani!

(I also tried to add a test for a 2nd-order CONSTANT, but it does not seem to parse through SANY. So I'd leave it at this.)

I vaguely recall that 2nd order operators are not supported in TLA+.

[thpani]

@thpani What do you mean by this? Something like this?

CONSTANTS
    \* @type: (Int, (Int) => Bool) => Bool;
    MapInt(_, MapFn(_))

Yes, exactly!

[thpani]

(I also tried to add a test for a 2nd-order CONSTANT, but it does not seem to parse through SANY. So I'd leave it at this.)

I vaguely recall that 2nd order operators are not supported in TLA+.

They're defined in Specifying Systems, but idk about tool support.