Model based testing

[Anatoliy Bilenko]

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.

[Hillel Wayne]

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

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...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/b73476e7-b13b-43b7-a460-90d4ce942c7bn%40googlegroups.com.

[Markus Kuppe]

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

[Anatoliy Bilenko]

Greetings,

Fantastic! Thank you for the quick responses!

- TraceDiehard was instrumental in capturing all state transitions explored by the simulator during its execution.
- The dumptrace option enabled exporting traces whenever a property or invariant was violated.

Also, I found this loop in TLC code which dumps the trace I expected to be dumped in JSON. 

Is it worth adding a JSON output for dumps? Maybe, I can do it.

Thanks,

Anatoliy.

[Markus Kuppe]

Yes, this would be the place to incorporate trace dumping into the simulation for formats other than TLA+. The majority of the infrastructure is already in place. In essence, you can follow the implementation of `-dumptrace`. In fact, calling `tool.checkPostConditionWithCounterExample(new CounterExample(curState));` from the for loop is almost sufficient.

I suggest that we move the technical discussion to an issue on GitHub at github.com/tlaplus/issues.

M.

[Jordan Halterman]

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. 

[1] – https://github.com/tlaplus/CommunityModules

--

[William Schultz]

We also wrote a bit about our recent experiences applying model-based test case generation to WiredTiger, a key-value storage engine used within MongoDB (code repo). Basically, our approach dumps the entire state graph to a JSON format and then computes path coverings in this graph to generate a suite of test cases.