An example TLA+ specification

We introduce a TLA+ specification that we use to discuss features of Apalache in the following sections. Its source code can be found in test/tla/y2k.tla:

-------------------------------- MODULE y2k --------------------------------
(*
* A simple specification of a year counter that is subject to the Y2K problem.
* In this specification, a registration office keeps records of birthdays and
* issues driver's licenses. As usual, a person may get a license, if they
* reached a certain age, e.g., age of 18. The software engineers never thought
* of their program being used until the next century, so they stored the year
* of birth using only two digits (who would blame them, the magnetic tapes
* were expensive!). The new millenium came with new bugs.
*
* This is a made up example, not reflecting any real code.
*
* Igor Konnov, January 2020
*)

EXTENDS Integers

CONSTANT
\* @type: Int;
\* @type: Int;

ASSUME(BIRTH_YEAR \in 0..99)

VARIABLE
\* @type: Int;
year,
\* @type: Bool;

Age == year - BIRTH_YEAR

Init ==
/\ year = BIRTH_YEAR

NewYear ==
/\ year' = (year + 1) % 100 \* the programmers decided to use two digits