Testing fragments of TLA+

Graham Hay

As your specs grow, you quickly reach a point where the feedback loop of running the whole model (even with restricted inputs) is too slow.

If you are using the Toolbox (GUI), it’s pretty easy to set up a scratchfile; but it is also possible to write some “unit” tests for any helper functions:

---- MODULE syn_tests ----
EXTENDS syn

VARIABLE x

I == FALSE /\ x = 0 
N == FALSE /\ x' = x 

...

\* AllRegisteredForNode

ASSUME LET l == ("n1" :> <<>> @@ "n2" :> [a |-> 0, b |-> 2] @@ "n3" :> [c |-> 1])
       res == AllRegisteredForNode(l)
       IN res = {"a", "b", "c"}

\* Duplicates

ASSUME LET l == ("n1" :> <<>> @@ "n2" :> [a |-> 0] @@ "n3" :> [a |-> 1])
       res == Duplicates(DOMAIN l, l, {})
       IN res = {"a"}
====

We need to override the Init and Next functions with this config file (syn_tests.cfg), to prevent the existing model from running:

INIT I
NEXT N

If the assumptions are all valid:

$ docker run --rm -it -v $PWD:/app -w /app amazoncorretto:8-alpine3.17-jdk java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC -workers auto -cleanup scratch.tla
TLC2 Version 2.18 of 20 March 2023 (rev: 3ea3222)
...
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 0.0
0 states generated, 0 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 1.
Finished in 00s at (2024-01-17 14:16:36)

The failure output isn’t very useful:

Starting... 
Error: Assumption line 17, col 8 to line 19, col 18 of module syn_tests is false.
Finished in 00s

But you can output values to debug, using PrintT:

ASSUME ... IN PrintT(res) /\ res = {}

Starting...
{"a"}
Error: Assumption line 17, col 8 to line 19, col 33 of module syn_tests is false.

There are some more examples here.

Leave a comment