Init and project layout

Matla project sources for this section available here.

Let's dive in on an non-matla TLA+ toy project. From this point, we assume you have performed matla's setup.

> ls -a
.gitignore  sw_0.cfg  sw_0.tla

> bat .gitignore
───────┬────────────────────────────────────────────────────────────────────────
       │ File: .gitignore
───────┼────────────────────────────────────────────────────────────────────────
   1   │ # Ignore macos trash files
   2   │ .DS_Store
───────┴────────────────────────────────────────────────────────────────────────

For the sake of reproducibility, here is the content of the .tla file. It encodes a stopwatch (sw) system counting time with cnt, featuring reset and start_stop buttons, and an "internal" counting flag. The counter saturates at 59.

\* sw_0.tla
---- MODULE sw_0 ----

LOCAL INSTANCE Integers

VARIABLES cnt, reset, start_stop, counting

svars == <<cnt, reset, start_stop, counting>>

bool(stuff) == stuff \in { TRUE, FALSE }

init ==
    bool(reset)
    /\ bool(start_stop)
    /\ (cnt = 0)
    /\ (counting = start_stop)

next ==
    bool(reset')
    /\ bool(start_stop')
    /\ (
        IF start_stop' THEN counting' = ~counting
        ELSE UNCHANGED counting
    ) /\ (
        IF reset' THEN cnt' = 0
        ELSE IF counting' /\ cnt < 59 THEN cnt' = cnt + 1
        ELSE UNCHANGED cnt
    )

inv_cnt_pos == cnt >= 0
inv_reset == reset => (cnt = 0)

cnt_leq_10 == cnt <= 10

 ====

And the .cfg file:

\* sw_0.cfg
INIT init
NEXT next

INVARIANTS
    inv_cnt_pos
    inv_reset