Is it worth adding a JSON output for dumps? Maybe, I can do it.
Anatoliy.
On Tuesday, July 22, 2025 at 9:23:18 PM UTC+3 Markus Kuppe wrote:
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...@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.