Translate quint variable initialization as equality, not assignment #2864
Conversation
We need to track both the names of nullary operators in scope and whether or not we in are in the scope of the `q::init` operator. The latter is require so that we can ensure all assignments in the init operator are unprimed. So we expand the reader to store both these bits of data
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.
|
Codecov ReportAttention: Patch coverage is
❗ Your organization needs to install the Codecov GitHub app to enable full functionality.
|
|
This isn't a full fix for #2863 yet: it only ensures primes are not added to assignments that occur within the body of the init predicate. For the general case, we need to ensure primes do not appear in any operator that is used by the init predicate. We can solve that this way:
Some additional care will need to be take about where the init-relevant operators are placed back into the sequence of converted operators, in case there other operators that refer to them, which must occur later. Placing the init-relevant operators after all variable declarations but before any others should be safe, since they are guaranteed not to refer to other operators. Alternatively, a different strategy could be employed on the quint side to remove the need for this complexity, as suggested on #2863. Unfortunately, I won't have time to complete this work, as I am losing my company access to github etc. now. <3 |
Fixes #2863
Note that this presupposes #2860, and should be rebased on main after that is merged in.
make fmt-fix(or had formatting run automatically on all files edited)./unreleased/for any new functionality