Here's how I do it. This requires the community modules, which
come default with the VSCode extension. First, I create a new file
named TraceDiehard.tla:
---- MODULE
TraceDiehard ----
EXTENDS TLC, TLCExt, Sequences, Json, Diehard \* Replace with
name of spec to trace
ASSUME
/\ TLCSet(1, <<>>)
/\ TLCSet(2, <<>>)
Record ==
/\ LET old_trace == TLCGet(1) IN
/\ Len(old_trace) > Len(Trace) =>
/\ TLCSet(2, Append(TLCGet(2), old_trace))
/\ TLCSet(1, Trace)
Final ==
/\ JsonSerialize("trace-" \o ToString(JavaTime) \o ".json",
Append(TLCGet(2), TLCGet(1))
)
====
Then, in TraceDiehard.cfg:
SPECIFICATION Spec
CONSTRAINT Record
POSTCONDITION Final
Run this with simulate "num=3" -depth 42, and you'll get test-time.json with your behaviors. How this works:
1. The Assume sets TLCGet(1) to the current trace (empty) and a sequence containing all completed simulations (also empty).
2. CONSTRAINT Record runs on on every step of the simulation. It checks to see if the current trace is shorter than the previous stored trace. If that happens, we must have finished one run of the simulation, so we append the last run to the sequence of completed simulations.
3. POSTCONDITION Final runs Final after the
simulation finishes, which then writes all of the traces to a json
file. It needs to append TLCGet(1) Record
doesn't add it (since there's no new trace to trigger the length
check).
If you want to include metadata in your run, pass a record to JsonSerialize:
Final ==
/\ JsonSerialize("trace-" \o ToString(JavaTime) \o ".json",
[Metadata |-> TK,
Traces |->
Append(TLCGet(2), TLCGet(1))
]
)
H
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.