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

[Yan Li <elliot....@xxxxxxxxx>]

Hi,

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.

—

Elliot