Re: [tlaplus] Model based testing

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

There are several ways to serialize traces into other machine-readable formats such as json. The simplest approach is to run TLC in a loop with the `-dumptrace` parameter enabled. For example:

for i in {1..5}; do tlc -note DieHard.tla -simulate num=3 -depth 42 -dumptrace json DieHard_$i.json; done

Markus

> On Jul 22, 2025, at 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/16BA9AB1-AE1C-48B8-AF74-9EAEBA9DC2E7%40lemmster.de.