learning_tla/learn_tla/core/04-parameterizing-specs.md

4. Parameterizing specs

• CONSTANT and CONSTANTS take their value at model run time, from the model configuration, not the spec.
• Assign values in *.cfg, like:
  • CONSTANT S = {1, 2, 3, 4, 5}
  • CONSTANT S = 1.10 should work but fails in the IntelliJ plugin

When defining constants in the configuration, the spec should always include ASSUME checks to validate the received configuration, to:

• prevent errors
• help readers understand the role of the constant

---- MODULE duplicates ----
EXTENDS Integers, Sequences, TLC, FiniteSets
CONSTANT S
ASSUME Cardinality(S) >= 3
====

Symmetry sets

Declaring a symmetry for a set of values will usually reduce the number of visibles states, making the evaluation shorter.

However, identifying the symmetries to prune the state list may be longer than actually evaluating them, so it is NOT ALWAYS an optimization.

Helper constants

A boolean DEBUG constant can be helpful:

---- MODULE foo ----
CONSTANT DEBUG
ASSUME DEBUG \in BOOLEAN

\* ...

macro print_if_debug(str) begin
  if DEBUG then
    print str;
  end if;
\* Another thing you can do is restrict multiple starting states with DEBUG:

Inputs ==
IF DEBUG
THEN {<<1, 2, 3, 4>>}
ELSE S \X S \X S \X S
====