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.