TLC Invariant violation not showing state steps in Error Trace window

[Ashish Negi]

Hi

When TLC finds a failure for invariant X, i don't see anything in Error Trace window ?

This is happening sometimes. I tried manipulating my spec to fail on some other condition and then TLC generates the error trace correctly.

Is this bug in TLC or some other issue ?

Thanks

Ashish

[Markus Kuppe]

Hi Ashish,

please open an issue [1] with the spec & model attached.

Thanks,
Markus

[1] https://github.com/tlaplus/tlaplus/issues