Author: Igor Konnov

Tags: specification tlaplus apalache tlc

This must be my shortest blog post ever. I just wanted to run TLC to check a specification that uses Apalache modules. For example, the typed version of two-phase commit MC3_TwoPhaseTyped.tla uses the module Variants. Sure, TLC can do that, but it requires a small trick.

Let’s do it step by step for MC3_TwoPhaseTyped.tla. Say, we want to see an example of all participants committing:

RMAllCommittedEx ==
    ~(\A rm \in RM: rmState[rm] = "committed")

Step 1. Checkout the Apalache repository, if you don’t have it already:

$ git clone git@github.com:apalache-mc/apalache.git
$ export APALACHE_HOME=$(pwd)/apalache

Step 2. Download TLA+ Tools:

$ wget https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
$ export TLC_HOME=$(pwd)

Step 3. Introduce a configuration file MC3_TwoPhaseTyped.cfg with the following content:

$ cd $APALACHE_HOME/test/tla
$ cat >MC3_TwoPhaseTyped.cfg <<EOF
INIT Init
NEXT Next
INVARIANT RMAllCommittedEx
EOF

Step 4. Run TLC with the option -cp, which extends the Java classpath. TLC will look for non-standard modules in the specified directory, that is, in the directory ${APALACHE_HOME}/src/tla. This is the trick!

$ java -cp ${TLC_HOME}/tla2tools.jar:${APALACHE_HOME}/src/tla \
  "-XX:+UseParallelGC" tlc2.TLC \
  -config MC3_TwoPhaseTyped.cfg MC3_TwoPhaseTyped.tla

As expected, TLC finds an example of RMAllCommittedEx:

Running breadth-first search Model-Checking...
...
State 11: <Next line 16, col 1 to line 16, col 22 of module MC3_TwoPhaseTyped>
/\ msgs = { [tag |-> "Commit", value |-> "0_OF_NIL"],
  [tag |-> "Prepared", value |-> "0_OF_RM"],
  [tag |-> "Prepared", value |-> "1_OF_RM"],
  [tag |-> "Prepared", value |-> "2_OF_RM"] }
/\ rmState = [0_OF_RM |-> "committed", 1_OF_RM |-> "committed", 2_OF_RM |-> "committed"]
/\ tmState = "committed"
/\ tmPrepared = {"0_OF_RM", "1_OF_RM", "2_OF_RM"}
...
1119 states generated, 287 distinct states found, 7 states left on queue.

Bottom line

This is it! If you have any questions, please feel free to reach out. I’m happy to help.

Need this kind of testing for your protocol?

I help teams turn distributed-system behavior into executable specs, model-checking campaigns, and CI-ready conformance harnesses.

Discuss your system →