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

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

From: Shane Miller <gshanemiller6@xxxxxxxxx>
Date: Thu, 25 Sep 2025 19:58:52 -0700 (PDT)

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

--
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/93c840ec-821a-4ab2-849d-36d8b24b5c3en%40googlegroups.com.

Follow-Ups:
- Re: [tlaplus] How to configure TLA to emit event traces on command line only (no IDE)
  - From: Markus Kuppe

Prev by Date: [tlaplus] TLA+ Validation Test Suite Now Available - Enabling ISO 26262 Certification for TLC
Next by Date: [tlaplus] Re: Confused about depth-first search
Previous by thread: Re: [tlaplus] TLA+ Validation Test Suite Now Available - Enabling ISO 26262 Certification for TLC
Next by thread: Re: [tlaplus] How to configure TLA to emit event traces on command line only (no IDE)
Index(es):
- Date
- Thread