Re: [tlaplus] Simulation mode

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 8/5/21 8:23 AM, je...@xxxxxxxxxxxxxxx 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

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