How to configure TLA to emit event traces on command line only (no IDE)

[Shane Miller]

Hello,

I've got model checking working on the command line.

I'd like to configure using the command only what the IDE does in the Error Trace Specification box.

It starts or involves something like:

>java -cp tla2tools.jar tlc2.TLC -generateSpecTE  -config <config> <spec>

And then what? 

>java -jar tla2tools.jar tla2tools.jar -help

omits this information

[Markus Kuppe]

Running TLC with or without the `-generateSpecTE` flag on a spec MySpec.tla creates a trace specification MySpec_TTrace_<timestamp>.tla. for error trace/counterexample exploration:

1. Open MySpec_TTrace_<timestamp>.tla and update the `expression` definition with the trace expression(s) you want to evaluate (compare https://github.com/tlaplus/tlaplus/issues/485).

2. Run TLC on the trace spec: java -cp tla2tools.jar tlc2.TLC -config MySpec_TTrace_<timestamp>.tla MySpec_TTrace_<timestamp>.tla

This reproduces the counterexample and evaluates the trace expressions you added.

M.

Related: https://github.com/tlaplus/tlaplus/issues/555#issuecomment-893017495