[BUG] Bug in the assignment finder

[konnov]

See #468. Use the following spec instead:

\*SPECIFICATION Spec
INIT Init
NEXT Next

INVARIANT AllValuesEqual

CONSTANTS
    MAX_TIMESTAMP = 3
    KEYS = {key}
    VALUES = {value}
    N_NODES = 2

PROPERTIES
    EventuallyConsistent

The transition pass fails as follows:

PASS #8: TransitionFinderPass                                     I@22:14:43.403
  > Found 1 initializing transitions                              I@22:14:43.433
To understand the error, read the manual:                         I@22:14:43.439
  [https://apalache.informal.systems/docs/apalache/principles.html#assignments] I@22:14:43.439
Assignment error: crdt.tla:36:3-37:45: timestamp' is used before it is assigned. See https://apalache.informal.systems/docs/apalache/principles.html#assignments E@22:14:43.440

[Kukovec]

Not a bug in the assignment solver as such. The underlying cause for this seems to be the syntax

\E <<a,b>> \in S \X T : p

The Desugarer should rewrite this into \E a \in S : \E b \in T : p

[konnov]

Let's fix it at the level of Desugarer

[konnov]

The fix is merged now