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

TLA+'s Error-Trace window is not showing variables in states


I run into this problem. I’m using TLA+ GUI to check a model with about 50 variables. When an error is detected (an assert error), the Error-Trace shows many states, but only the Initial predicate is expandable, and I can’t figure out how to see the variables of other states. I tried clicking these states, double-clicking, and right-clicking, but nothing works. So far I’m stuck. I know the location of the assertion, but can’t figure out the steps that lead to this assertion failure.

I’ve attached a screenshot.

Thanks in advance.