TLA+ (Temporal Logic of Actions) is a formal specification language, used for specifying and checking systems and algorithms for corectness. As I’m further exploring it (see my last post about modelling subscription throttling), I’m ocasionally running into situations where I think there may be an issue with the current specification as they unexpectedly do not terminate, but without a clear reason.

In programming languages it is common to fire up a debugger and step through the program execution, inspecting instruction flow and variable values. With TLC there is no clear way to do so, at least I was unable to find any. TLC will only provide an error trace for errors it does find, however if TLC execution does not terminate this is of little use.

In TLC Command-line options I found the -dump <file> option, which dumps out every reached state into the specified file. There is no equivalent GUI option in “TLA+ Toolbox’s” TLC options, so it has to be specified as a TLC command line parameter in Model > Advanced Options > TLC Options > TLC command line parameters.

The dump file itself consists of plaintext state values, so it is certainly human readable. For a tautology checking spec when run with the -dump states.txt:

VARIABLES P, Q

F1(A, B) == A => B
F2(A, B) == ~A \/ B

ValuesEquivalent == F1(P, Q) <=> F2(P, Q)

Init ==
    /\ P \in BOOLEAN
    /\ Q \in BOOLEAN
    
Next ==
    /\ P' \in BOOLEAN
    /\ Q' \in BOOLEAN
    
Spec ==
    Init /\ [][Next]_<<P, Q>>

The dump file in <SPEC_PATH>/<SPEC_NAME>.toolbox/<MODEL_NAME>/states.txt.dump contains:

State 1:
/\ P = FALSE
/\ Q = FALSE

State 2:
/\ P = FALSE
/\ Q = TRUE

State 3:
/\ P = TRUE
/\ Q = FALSE

State 4:
/\ P = TRUE
/\ Q = TRUE

It’s a low-tech approach, it still is difficult to follow execution in cases with many states, but it has helped me get a better grasp on which states TLC is exploring and clarify issue suspicions. One thing to note is that depending on the size of a state and the number of states, the filesize may quickly grow into gigabytes range, so in certain cases it may be impractical to dump all distinct states, requiring early termination of TLC.

This is a very basic method, but if you have better ways of debugging specs themselves - please do let me know!