[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Simulation mode

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

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_*):


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?


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.