[tlaplus] Model based testing

[Anatoliy Bilenko <anatoliy.bilenko@xxxxxxxxx>]

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.