-simulate file = pname num = num
-simulate file=pname,num=num
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.