Assignments in quint init operators need to be unprimed

[shonfeder]

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

apalache/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala

Line 614 in efb30ea

case "assign" => binaryApp(opName, (lhs, rhs) => tla.assign(tla.prime(lhs), rhs))

But in the init operator these should not be primed.

[shonfeder]

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

[bugarela]

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:

apalache/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/ReTLAToVMTTranspilePassImpl.scala

Line 42 in 9295b5b

val deprime = ReplaceFixed(tracker).withFun { case OperEx(TlaActionOper.prime, arg) => arg }