Nonsensical "used before it is assigned" error with grouped-variable UNCHANGED spec

[edwardcwang]

Description

If we use a grouped-variable UNCHANGED with Apalache, we get a nonsensical Assignment error: [...] is used before it is assigned variable.

The exact same specification works fine with TLC (TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802))

echo "SPECIFICATION Spec" > UsedBeforeAssigned.cfg
java -jar tla2tools.jar -config UsedBeforeAssigned.cfg UsedBeforeAssigned.tla

Impact

This can be worked around by not using grouped-variable UNCHANGED statements but it increases the verbosity of the spec. This is likely an Apalache-specific bug, since the same spec works unchanged in TLC.

myList1 == <<myVar1, myVar2>>
myList2 == <<myVar3, myVar4>>
\* This works, but is unnecessarily verbose/clunky
\*vars == <<myVar1, myVar2, myVar3, myVar4>>
\* Error, even though it's supported by TLC/TLA+
vars == <<myList1, myList2>>

Input specification

\* apalache-mc check --debug --write-intermediate UsedBeforeAssigned.tla
\* echo "SPECIFICATION Spec" > UsedBeforeAssigned.cfg
\* [tla2tools.jar] -config UsedBeforeAssigned.cfg UsedBeforeAssigned.tla
------------------------------- MODULE UsedBeforeAssigned -------------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Option

VARIABLES
  \* @type: Bool;
  myVar1,
  \* @type: Str;
  myVar2

myList1 == <<myVar1, myVar2>>

VARIABLES
  \* @type: Int;
  myVar3,
  \* @type: Str;
  myVar4

myList2 == <<myVar3, myVar4>>

\* Workaround in Apalache
\*vars == <<myVar1, myVar2, myVar3, myVar4>>

\* Error despite being supported by TLC
vars == <<myList1, myList2>>

Init ==
  /\ myVar1 = TRUE
  /\ myVar2 = ""
  /\ myVar3 = 0
  /\ myVar4 = ""

Next == UNCHANGED vars

Spec ==
  /\ Init
  /\ [][Next]_vars

=============================================================================

The command line parameters used to run the tool

check --debug --write-intermediate UsedBeforeAssigned.tla

Expected behavior

This should either work fine as it's part of TLA+ and supported by TLC, or if it's explicitly intended to be unsupported by Apalache, this should emit a user-friendly error message with correct source locators along with documentation as to why it's not supported by Apalache despite being support by TLC.

Log files

PASS #1: TypeCheckerSnowcat                                       I@23:39:54.812
 > Running Snowcat .::.                                           I@23:39:54.812
 > Your types are purrfect!                                       I@23:39:55.366
 > All expressions are typed                                      I@23:39:55.366
PASS #2: ConfigurationPass                                        I@23:39:55.418
  > Set the initialization predicate to Init                      I@23:39:55.423
  > Set the transition predicate to Next                          I@23:39:55.423
PASS #3: DesugarerPass                                            I@23:39:55.454
  > Desugaring...                                                 I@23:39:55.454
PASS #4: InlinePass                                               I@23:39:55.660
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next I@23:39:55.660
PASS #5: TemporalPass                                             I@23:39:55.729
  > Rewriting temporal operators...                               I@23:39:55.730
  > No temporal property specified, nothing to encode             I@23:39:55.730
PASS #6: InlinePass                                               I@23:39:55.735
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next I@23:39:55.735
PASS #7: PrimingPass                                              I@23:39:55.740
  > Introducing InitPrimed for Init'                              I@23:39:55.743
PASS #8: VCGen                                                    I@23:39:55.755
  > No invariant given. Only deadlocks will be checked            I@23:39:55.755
PASS #9: PreprocessingPass                                        I@23:39:55.758
  > Before preprocessing: unique renaming                         I@23:39:55.759
 > Applying standard transformations:                             I@23:39:55.767
  > PrimePropagation                                              I@23:39:55.768
  > Desugarer                                                     I@23:39:55.777
  > UniqueRenamer                                                 I@23:39:55.784
  > Normalizer                                                    I@23:39:55.794
  > Keramelizer                                                   I@23:39:55.801
  > After preprocessing: UniqueRenamer                            I@23:39:55.809
PASS #10: TransitionFinderPass                                    I@23:39:55.818
  > Found 1 initializing transitions                              I@23:39:55.831
To understand the error, read the manual:                         I@23:39:55.834
  [https://apalache-mc.org/docs/apalache/principles/assignments.html] I@23:39:55.835
Assignment error: UsedBeforeAssigned.tla:13:14-13:19: myVar1' is used before it is assigned. See https://apalache-mc.org/docs/apalache/principles/assignments.html E@23:39:55.835
It took me 0 days  0 hours  0 min  1 sec                          I@23:39:55.836
Total time: 1.604 sec                                             I@23:39:55.836
EXITCODE: ERROR (255)

System information

• Apalache version: 56462d3 build 56462d3 (revision 56462d384d63853ceb503c8eb86a4eff02572529 from main branch)
• OS: Ubuntu Linux x86_64 24.04
• JDK version: 21.0.3

Triage checklist (for maintainers)

• Reproduce the bug on the main development branch.
• Add the issue to the apalache GitHub project.
• If the bug is high impact, ensure someone available is assigned to fix it.

[konnov]

Confirmed. This requires an additional desugaring step that decomposes tuples in UNCHANGED.