Re: [tlaplus] How to configure TLA to emit event traces on command line only (no IDE)

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

> On Sep 25, 2025, at 7:58 PM, Shane Miller <gshanemiller6@xxxxxxxxx> wrote:
> 
> 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


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

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/70B41271-C387-40BA-9528-C896C0BD5879%40lemmster.de.