Re: [tlaplus] Êrror-Trace Exploration not working

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

On 23.08.2017 18:40, Christian Spann wrote:
> I am trying to explore an error trace by adding some expressions to the Error-Trace Explorer. I used that feature some months ago but now I am failing to get it running. Even the simplest expressions like "Cardinality( someset )" fail without any error. The only reproducible result is that I cannot run the model after exploring my expression and the file TE.tla mentioned here [1] seems not to be created. I have to restart the Toolbox to get the model running again.
>
> Has anyone any idea what I am missing

Hi Christian,

are you running the Unicode beta of the Toolbox or the regular 1.5.3
release? Can you share the spec and model (if necessary privately) that
cause the problem?

Does the Toolbox's .log file indicate as to what is happening? The .log
file is located in the Toolbox's workspace/.metadata/ directory, which
is normally located inside the Toolbox installation directory.

Thanks

Markus