Debug/release: conditional compilation

This chapter builds on the toy project discussed in the previous chapter. It might be useful to be familiar with it, especially if this is your first time reading this.

Matla's conditional compilation is tied to the Matla module discussed in the previous chapter. If you remember, Matla.tla is generated by matla init among your project's sources.

Just like we did back then, let's pretend this module only defines assert and none of its variants, all of which are handled the same by matla's conditional compilation anyway.

> cat Matla.tla
---- MODULE Matla ----
\* Matla helpers, mostly for assertions and debug/release conditional compilation.

\* TLC!Assertions are built on top of the standard `TLC' module.
LOCAL TLC == INSTANCE TLC
---- MODULE dbg ----
\* All functions in this module do nothing in `release' mode.

\* Checks some predicate.
assert(
    \* Predicate that must be true.
    pred,
    \* Message issued when the predicate is false.
    message
) ==
    TLC!Assert(pred, message)

====
\* End of module `dbg'.

\* Contains debug-only functions.
dbg == INSTANCE dbg

\* Checks some predicate.
\*
\* Active in debug and release.
assert(
    \* Predicate that must be true.
    pred,
    \* Message issued when the predicate is false.
    message
) ==
    TLC!Assert(pred, message)

====
\* End of module `Matla'.

The two versions, Matla!assert and Matla!dbg!assert, behave exactly the same in debug mode, which is matla run's default mode. They differ in release mode however, activated by matla run --release, in that Matla!dbg!asserts will be compiled away (replaced by TRUE) while Matla!asserts will still cause TLC to check them, and fail if they do not hold.

Let's illustrate this on our running stopwatch project, sources available here.

> exa
Matla.tla  Matla.toml  sw_0.cfg  sw_0.tla  target

> bat sw_0.cfg
───────┬────────────────────────────────────────────────────────────────────────
       │ File: sw_0.cfg
───────┼────────────────────────────────────────────────────────────────────────
   1   │ INIT init
   2   │ NEXT next
   3   │
   4   │ INVARIANTS
   5   │     inv_cnt_pos
   6   │     inv_reset
───────┴────────────────────────────────────────────────────────────────────────

Module sw_0 defines a next action:

> bat -r 17:27 sw_0.tla
───────┬────────────────────────────────────────────────────────────────────────
       │ File: sw_0.tla
───────┼────────────────────────────────────────────────────────────────────────
  17   │ next ==
  18   │     bool(reset')
  19   │     /\ bool(start_stop')
  20   │     /\ (
  21   │         IF start_stop' THEN counting' = ~counting
  22   │         ELSE UNCHANGED counting
  23   │     ) /\ (
  24   │         IF reset' THEN cnt' = 0
  25   │         ELSE IF counting' /\ cnt < 59 THEN cnt' = cnt + 1
  26   │         ELSE UNCHANGED cnt
  27   │     )
───────┴────────────────────────────────────────────────────────────────────────

Let's add a non-debug check that we expect to fail:

> bat -r 17:29 sw_0.tla
───────┬────────────────────────────────────────────────────────────────────────
       │ File: sw_0.tla
───────┼────────────────────────────────────────────────────────────────────────
  17 ~ │ LOCAL Matla == INSTANCE Matla
  18   │ next ==
  19   │     bool(reset')
  20   │     /\ bool(start_stop')
  21 + │     /\ Matla!assert(reset')
  22   │     /\ (
  23   │         IF start_stop' THEN counting' = ~counting
  24   │         ELSE UNCHANGED counting
  25   │     ) /\ (
  26   │         IF reset' THEN cnt' = 0
  27   │         ELSE IF counting' /\ cnt < 59 THEN cnt' = cnt + 1
  28   │         ELSE UNCHANGED cnt
  29   │     )
───────┴────────────────────────────────────────────────────────────────────────

Running matla again, we get

Error: an assertion failed with "that's probably going to fail"

- triggered at
  module sw_0, 20:8 → 20:60
        |        vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv
     20 |     /\ Matla!assert(reset', "that's probably going to fail")
        |

- while exploring this trace
  ┌───┐
  │ 0 │ initial state
  └─┬─┘
    │ cnt       : 0
    │ counting  : false
    │ reset     : false
    │ start_stop: false
    ┴
specification is unsafe

Let's make sure debug/release modes work for Matla!dbg!assert. Project sources available here.

> bat -r 17:29 sw_0.tla
───────┬────────────────────────────────────────────────────────────────────────
       │ File: sw_0.tla
───────┼────────────────────────────────────────────────────────────────────────
  17   │ LOCAL Matla == INSTANCE Matla
  18   │ next ==
  19   │     bool(reset')
  20   │     /\ bool(start_stop')
  21 ~ │     /\ Matla!dbg!assert(reset')
  22   │     /\ (
  23   │         IF start_stop' THEN counting' = ~counting
  24   │         ELSE UNCHANGED counting
  25   │     ) /\ (
  26   │         IF reset' THEN cnt' = 0
  27   │         ELSE IF counting' /\ cnt < 59 THEN cnt' = cnt + 1
  28   │         ELSE UNCHANGED cnt
  29   │     )
───────┴────────────────────────────────────────────────────────────────────────

Running in debug mode (without --release) should still fail:

> matla run -w 1
Error: an assertion failed with "that's probably going to fail"

- triggered at
  module sw_0, 20:8 → 20:64
        |        vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv
     20 |     /\ Matla!dbg!assert(reset', "that's probably going to fail")
        |

- while exploring this trace
  ┌───┐
  │ 0 │ initial state
  └─┬─┘
    │ cnt       : 0
    │ counting  : false
    │ reset     : false
    │ start_stop: false
    ┴
specification is unsafe

Running in release mode should succeed however, since besides the assertion line 21 the specification is safe:

> matla run -w 1 --release
specification is safe