## Assignments and symbolic transitions

Let us go back to the example
`test/tla/y2k.tla`

and run `apalache`

against
`test/tla/y2k_override.tla`

:

```
$ apalache check y2k_override.tla
```

We can check the detailed output of the `TransitionFinderPass`

in the file
`_apalache-out/y2k_override.tla/<timestamp>/09_OutTransition.tla`

, where
`<timestamp>`

looks like `2021-12-01T12-07-41_1998641578103809179`

:

```
---------------------------- MODULE y2k_override ----------------------------
(*
* One way to instantiate constants for apalache is to use the OVERRIDE prefix.
*)
EXTENDS y2k
OVERRIDE_BIRTH_YEAR == 80
OVERRIDE_LICENSE_AGE == 18
=============================================================================
\* Modification History
\* Last modified Tue Jan 07 11:24:55 CET 2020 by igor
\* Created Tue Jan 07 11:16:18 CET 2020 by igor
```

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

- 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$0`

. We call these expressions**assignments**. - It has factored the operator
`Next`

into two operators`Next$0`

and`Next$1`

. 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 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/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 (99)
```