Simulation mode

[je...@emptysquare.net]

Hello, I'm having some difficulty using the TLC "-simulate" option.

1. If I select "Simulation Mode" in the Toolbox's "TLC Options", the "Maximum number of traces" empty, then it runs indefinitely (as expected), but when I hit "Cancel" I don't see any trace output in the Toolbox GUI. I can't find any trace files either. How does simulation mode work by default in the Toolbox?
2. If I set "Maximum number of traces" to 100, then TLC logs "Progress(600) at 2021-08-05 11:14:00: 16221 states generated, -1 distinct states found, -1 states left on queue", then terminates. I still can't figure out how to view the traces it produced.
3. Switching to the command line, if I run "java -cp tla2tools.jar  tlc2.TLC MySpec.tla -simulate", it runs indefinitely as expected, and I hit Ctrl-C, I can't find the generated traces anywhere. The .out files in the .toolbox directory don't include any traces.
4. I tried passing "-simulate file=foo,num=100" but TLC complained, "Error: Error: more than one input files: MCSliceMerge and file=foo,num=100". I can't figure out what the syntax is for specifying an output file or number of traces, even after reading Current Versions of the TLA+ Tools and the source of TLC.java.

Thanks for your help.

[Markus Kuppe]

On 8/5/21 8:23 AM, je...@emptysquare.net wrote:
> Hello, I'm having some difficulty using the TLC "-simulate" option.
>

> 1. If I select "Simulation Mode" in the Toolbox's "TLC Options", the

> "Maximum number of traces" empty, then it runs indefinitely (as
> expected), but when I hit "Cancel" I don't see any trace output in
> the Toolbox GUI. I can't find any trace files either. How does
> simulation mode work by default in the Toolbox?

> 2. If I set "Maximum number of traces" to 100, then TLC logs

> "Progress(600) at 2021-08-05 11:14:00: 16221 states generated, -1
> distinct states found, -1 states left on queue", then terminates. I
> still can't figure out how to view the traces it produced.

> 3. Switching to the command line, if I run "java -cp tla2tools.jar

> tlc2.TLC MySpec.tla -simulate", it runs indefinitely as expected,
> and I hit Ctrl-C, I can't find the generated traces anywhere. The
> .out files in the .toolbox directory don't include any traces.

> 4. I tried passing "-simulate file=foo,num=100" but TLC complained,

> "Error: Error: more than one input files: MCSliceMerge and
> file=foo,num=100". I can't figure out what the syntax is for
> specifying an output file or number of traces, even after reading
> Current Versions of the TLA+ Tools

> <http://lamport.azurewebsites.net/tla/current-tools.pdf> and the
> source of TLC.java
> <https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/TLC.java>.


Hi Jesse,

TLC does *not* keep the traces that are generated by the simulator
unless you pass the "file" sub-command to the simulate command. Then,
you will get N files where N is the parameter of the "num" sub-command.
Below, this is how you write two traces to two files (ewd998.txt_0_*):

```shell

markus@banana:~/src/TLA/ewd998(main)$ java -jar tla2tools.jar -simulate
file=ewd998.txt,num=2 MCEWD998
TLC2 Version 2.16 of Day Month 20?? (rev: f56cf14)
Running Random Simulation with seed 3965791887613659699 with 1 worker on
16 cores with 7936MB heap and 64MB offheap memory [pid: 21775] (Linux
5.11.0-25-generic amd64, Ubuntu 11.0.11 x86_64).
...
Starting... (2021-08-05 09:07:51)
Computed 64 initial states...
Progress: 86 states checked, 2 traces generated (trace length: mean=10,
var(x)=1, sd=1)
Finished in 00s at (2021-08-05 09:07:51)

markus@banana:~/src/TLA/ewd998(main)$ ls ewd998.txt_0_*
ewd998.txt_0_0 ewd998.txt_0_1

markus@banana:~/src/TLA/ewd998(main)$ head ewd998.txt_0_0
---------------- MODULE ewd998.txt_0_0 -----------------
STATE_1 ==
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "black")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ token = [q |-> 0, color |-> "black", pos |-> 0]


STATE_2 ==
...

```

The file sub-command is not available in the Toolbox.


The format of the generated files might not be suitable for your
use-case. What is it that you want to do?


Markus

[A. Jesse Jiryu Davis]

Brilliant, thank you! The format is fine for me, my only goal is to read some random traces to check my understanding of my spec.

Is there a way to import one of these files into the Toolbox's trace viewer?

In "Current Versions of the TLA+ Tools" the option is described thus:

-simulate file = pname num = num

I think it would be more helpful to describe it like:

-simulate file=pname,num=num

... and also to emphasize somewhere in that PDF that the specfile name must come after all options.

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/cb6f7de9-2a4e-fb53-957b-dc97e58f4356%40lemmster.de.

[Markus Kuppe]

On 8/5/21 9:23 AM, A. Jesse Jiryu Davis wrote:
> Brilliant, thank you! The format is fine for me, my only goal is to read
> some random traces to check my understanding of my spec.
>
> Is there a way to import one of these files into the Toolbox's trace viewer?

The Toolbox can open the generated file, but SANY won't parse it.


Perhaps, a more useful approach to studying your spec with trace
exploration is to simulate your spec checking an "artificial" invariant
such as `TLCGet("level") < N`. You get a trace if you choose N less
than the diameter shown on the model's result page.
Additionally, formulate action- and state-constraints to direct the
simulator towards more interesting areas of the state space. This
requires a recent TLC nightly build, though.

Markus

[1]
https://github.com/tlaplus/tlaplus/commit/e7b17ad43db6e277c502840e2b0d1be8effea41b

[A. Jesse Jiryu Davis]

Great tips, thanks.

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/18a70444-91e4-ca26-df1b-79888216d91d%40lemmster.de.