Re: [tlaplus] TLA+'s Error-Trace window is not showing variables in states

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 07.08.2015 03:44, Yan Li wrote:
> 
> 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.

Hi Elliot,

this doesn't appear to be a bug in the UI. The states - that cannot be
expanded - are special states to indicate a cycle. However, there should
only be a single special state.

Can you share your spec/model with me or at least the corresponding text
output shown in the TLC Console?

Thanks
Markus