Assignments and symbolic transitions

Let us go back to the example test/tla/y2k.tla and run apalache-mc against test/tla/y2k_override.tla while instructing Apalache to write intermediate output files:

$ apalache-mc check --write-intermediate=true y2k_override.tla

We can check the detailed output of the TransitionFinderPass in the file _apalache-out/y2k_override.tla/<timestamp>/intermediate/<pass>_OutTransitionFinderPass.tla, where <timestamp> looks like 2021-12-01T12-07-41_1998641578103809179, and <pass> is a two-digit number like 08:

--------------------------- MODULE 09_OutTransition ---------------------------

EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache

VARIABLE
  (*
    @type: Int;
  *)
  year

VARIABLE
  (*
    @type: Bool;
  *)
  hasLicense

(*
  @type: (() => Bool);
*)
ASSUME(80 \in 0 .. 99)

(*
  @type: (() => Bool);
*)
ASSUME(18 \in 1 .. 99)

(*
  @type: (() => Bool);
*)
Init_si_0000 == year' := 80 /\ hasLicense' := FALSE

(*
  @type: (() => Bool);
*)
Next_si_0000 == year' := ((year + 1) % 100) /\ hasLicense' := hasLicense

(*
  @type: (() => Bool);
*)
Next_si_0001 == year - 80 >= 18 /\ hasLicense' := TRUE /\ year' := year

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

As you can see, the model checker did two things:

  1. It has translated several expressions that look like x' = e into x' := e. For instance, you can see year' := 80 and hasLicense' := FALSE in Init_si_0000. We call these expressions assignments.
  2. It has factored the operator Next into two operators Next_si_0000 and Next_si_0001. We call these operators symbolic transitions.

Pure TLA+ does not have the notions of assignments and symbolic transitions. However, TLC sometimes treats expressions x' = e and x' \in S as if they were assigning a value to the variable x'. TLC does so dynamically, during the breadth-first search. Apalache looks statically for assignments among the expressions x' = e and x' \in S.

When factoring out operators into symbolic transitions, Apalache splits the action operators Init and Next into disjunctions (e.g., A_0 \/ ... \/ A_n), represented in the concrete syntax as a sequence of operator definitions of the form

A$0 == ...
...
A$n == ...

The main contract between the assignments and symbolic transitions is as follows:

For every variable x declared with VARIABLE, there is exactly one assignment of the form x' := e in every symbolic transition A_n.

If Apalache cannot find expressions with the above properties, it fails. Consider the example test/tla/Assignments20200309.tla:

----- MODULE Assignments20200309 -----
VARIABLE
    \* @type: Int;
    a

\* this specification fails, as it has no expression
\* that can be treated as an assignment
Init == TRUE
Next == a' = a
Inv == FALSE
===============

Run the checker with:

apalache-mc check Assignments20200309.tla

Apalache reports an error as follows:

...
PASS #9: TransitionFinderPass
To understand the error, [check the
manual](https://apalache.informal.systems/docs/apalache/principles/assignments.html):
Assignment error: No assignments found for: a
It took me 0 days  0 hours  0 min  1 sec
Total time: 1.88 sec
EXITCODE: ERROR (255)

More details

Check Assignments and Symbolic Transitions in Depth.