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.On Tue, Jul 22, 2025, 4:32 AM Anatoliy Bilenko <anatoliy...@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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/b73476e7-b13b-43b7-a460-90d4ce942c7bn%40googlegroups.com.