Re: [tlaplus] Model based testing

I've done a bit of work on model-based testing in the past, and I've played with a couple different ways to get the states for testing.

One approach I've used is to run TLC with the -dot flag which will output the graph of states to a .dot file. You should then be able to find a dotfile parser to parse the states and could even convert them to JSON from there.

Alternatively, the community modules[1] include a JSON module which you can use to encode states to JSON. You can write a next state action to serialize whatever state you're interested in and append it to a file.

All that said, it's been quite some time since I last worked on this problem, so it's entirely possible the community has developed a more elegant solution for getting the states and I've just missed it. I'm sure others will chime in if that's the case.

[1] – https://github.com/tlaplus/CommunityModules

On Tue, Jul 22, 2025, 4:32 AM Anatoliy Bilenko <anatoliy.bilenko@xxxxxxxxx> wrote:

I've written a TLA+ model for my algorithm and am now experimenting with state exploration using TLC's -simulate mode. The goal is to observe various execution paths for an implementation of the algorithm written in another language.

As an initial test, I used the DieHard.tla model available on Lemmy's GitHub and ran the following command:

tlc -config DieHard.cfg -simulate 'file=dump.txt,num=3' -depth 42 DieHard.tla

(Note: I'll explore the -depth, -aril, and -seed options more thoroughly later.)

This produced a set of dump files in the working directory:

$ ls dump.txt*
dump.txt_0_0 dump.txt_0_1 dump.txt_0_2 dump.txt_0_3 dump.txt_0_4
dump.txt_0_5 dump.txt_0_6 dump.txt_0_7 dump.txt_0_8 dump.txt_0_9

Each file contains output in the following format:

STATE_2 ==
/\ big = 0
/\ small = 3

STATE_3 ==
/\ big = 0
/\ small = 3

STATE_4 ==
/\ big = 0
/\ small = 3

STATE_5 ==
/\ big = 5
/\ small = 3
...

Question:
Is there a library or built-in TLA+ functionality that can convert this TLC dump format into a machine-readable format like JSON?

Thanks in advance,
Anatoliy.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/b73476e7-b13b-43b7-a460-90d4ce942c7bn%40googlegroups.com.