Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixes for compilation to TLA+ #2891

Merged
merged 10 commits into from
May 6, 2024
Merged

Fixes for compilation to TLA+ #2891

merged 10 commits into from
May 6, 2024

Conversation

bugarela
Copy link
Collaborator

@bugarela bugarela commented May 3, 2024

Hello :octocat:

This includes 4 fixes for the Quint/JSON -> TLA+ compilation.

  1. slice was incorrectly making an increment on the last argument. From the Quint manual:
replaceAt(l, start, end)
// Slice a list from `start` until `end`.
// Equivalent to SubSeq(lst, start + 1, end) in TLA+.
  1. The produced TLA+ module was lacking type annotations required by Apalache. We now include them.
  2. Apalache transforms all operators given to folds in let in expressions. See: https://github.com/informalsystems/apalache/blob/9295b5b6cdc76b991e99a5546a6c62e62e7dfd39/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala#L121-L129
    However, this is not valid TLA+ and won't be parsed by SANY. To avoid touching Apalache internals, and as I can't really invest in forking the translation process right now, I'm simply fixing this with a regex replacement before printing. Not a great solution, but super low-risk as this only affects what is printed by the compilation command, which is only used by Quint.
  3. We had some leftover :: separators in our names, which is not parseable by SANY. They were coming from exists/forall expressions, so I'm making sure we also sanitize the names on those.
  • Tests added for any new code
    • I couldn't add tests for (2) and (3). The setup we have for testing server commands doesn't have enough instrumentation, and I'd have to learn a lot of things in order to make it work with tests for this.
  • 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
Copy link

codecov-commenter commented May 3, 2024

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 78.89%. Comparing base (4ae3445) to head (8636a57).

Additional details and impacted files
@@            Coverage Diff             @@
##             main    #2891      +/-   ##
==========================================
- Coverage   78.89%   78.89%   -0.01%     
==========================================
  Files         467      467              
  Lines       15966    15975       +9     
  Branches     2573     2556      -17     
==========================================
+ Hits        12597    12604       +7     
- Misses       3369     3371       +2     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@bugarela bugarela marked this pull request as ready for review May 3, 2024 19:41
@bugarela bugarela requested a review from p-offtermatt May 3, 2024 19:42
@@ -209,7 +209,7 @@ class PrettyWriter(
val sign = PrettyWriter.bindingOps(op)
val doc =
group(
group(text(sign) <> space <> text(x.toString) <> space <>
group(text(sign) <> space <> text(sanatizeID(x.toString)) <> space <>
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: should it be sanitize?

Copy link
Collaborator

@p-offtermatt p-offtermatt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@bugarela bugarela enabled auto-merge May 6, 2024 11:17
@bugarela bugarela merged commit d5dd0ad into main May 6, 2024
10 checks passed
@bugarela bugarela deleted the gabriela/compile-to-tla-fixes branch May 6, 2024 11:54
@apalache-bot apalache-bot mentioned this pull request May 6, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants