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

[tlaplus] Simulation mode

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.

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/a19099ed-1465-4893-9d76-dff1e6f10d1fn%40googlegroups.com.