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

Assignments in quint init operators need to be unprimed #2863

Open
shonfeder opened this issue Mar 14, 2024 · 2 comments
Open

Assignments in quint init operators need to be unprimed #2863

shonfeder opened this issue Mar 14, 2024 · 2 comments
Assignees
Labels
feature A new feature or functionality

Comments

@shonfeder
Copy link
Contributor

We are currently translating all cases of quint's assign operator, _' = _ as _' := _ in the apalache IR:

https://github.com/informalsystems/apalache/blob/efb30eaf2f1fc76249e1116ee72e659485483823/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala#L614

But in the init operator these should not be primed.

@shonfeder shonfeder added the feature A new feature or functionality label Mar 14, 2024
@shonfeder shonfeder self-assigned this Mar 14, 2024
@shonfeder
Copy link
Contributor Author

This is not super straightforward in the general case. Consider a quint spec like

var x: int
var y: int

def foo = x' = 0
def bar = y' = 0

def init = all{ foo, bar }

In order to ensure that we translate the variable initialization into equalities (as needed by TLC) instead of "assignments" (as we are currently doing), we will need to track all operators that are used in init (transitively) and ensure that we treat quint assignment application one way in those contexts, but treat them as apalache assignments in all other contexts. This is totally doable of course, but it will complicate the translation a lot. We may want to consider something on the quint side instead, that gives us different operators for these two different cases.

FYI @bugarela

shonfeder pushed a commit that referenced this issue Mar 15, 2024
Closes #2863

Fixes an incorrect translation that was translating initialization of
state variables in quint init predicates into assignments, when they
should only be equalities.
@bugarela
Copy link
Collaborator

I also thought about doing this in Quint side. However, I accidentally just bumped into this, which might be a promising way of doing it in the Apalache side:
https://github.com/informalsystems/apalache/blob/9295b5b6cdc76b991e99a5546a6c62e62e7dfd39/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/ReTLAToVMTTranspilePassImpl.scala#L42

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature A new feature or functionality
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants