TLA+ Toolbox 1.5.3 not displaying error trace

[Andrew Helwer]

I installed 1.5.3, and on a fairly complicated spec it does not display the error trace in the GUI:



Double-clicking those states does nothing and provides no further details. Weirdly, if I look inside MC.out I see the state trace just fine:

@!@!@STARTMSG 2110:1 @!@!@
Invariant inv_149384363400123000 is violated.
@!@!@ENDMSG 2110 @!@!@
@!@!@STARTMSG 2121:1 @!@!@
The behavior up to this point is:
@!@!@ENDMSG 2121 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ IsNodeUp = (n1 :> TRUE @@ n2 :> TRUE @@ n3 :> TRUE)
/\ NetworkPath = ( <<n1, n1>> :> TRUE @@
  <<n1, n2>> :> TRUE @@
  <<n1, n3>> :> TRUE @@
  <<n2, n1>> :> TRUE @@
  <<n2, n2>> :> TRUE @@
  <<n2, n3>> :> TRUE @@
  <<n3, n1>> :> TRUE @@
  <<n3, n2>> :> TRUE @@
  <<n3, n3>> :> TRUE )
/\ LockTimeout = FALSE
/\ BackupLock = None
/\ IsTakingBackup = (n1 :> FALSE @@ n2 :> FALSE @@ n3 :> FALSE)
/\ Leader = None

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <Action line 138, col 24 to line 138, col 37 of module NodeBackup>
/\ IsNodeUp = (n1 :> TRUE @@ n2 :> TRUE @@ n3 :> TRUE)
/\ NetworkPath = ( <<n1, n1>> :> TRUE @@
  <<n1, n2>> :> TRUE @@
  <<n1, n3>> :> TRUE @@
  <<n2, n1>> :> TRUE @@
  <<n2, n2>> :> TRUE @@
  <<n2, n3>> :> TRUE @@
  <<n3, n1>> :> TRUE @@
  <<n3, n2>> :> TRUE @@
  <<n3, n3>> :> TRUE )
/\ LockTimeout = FALSE
/\ BackupLock = None
/\ IsTakingBackup = (n1 :> FALSE @@ n2 :> FALSE @@ n3 :> FALSE)
/\ Leader = n1

@!@!@ENDMSG 2217 @!@!@
(and so on)

It just doesn't appear to make its way into the error trace in the GUI.

[Markus Alexander Kuppe]

On 03.05.2017 22:46, Andrew Helwer wrote:
> I installed 1.5.3, and on a fairly complicated spec it does not
> display the error trace in the GUI:

Hi Andrew,

I opened an issue on Github [1] to track progress. Please attach the
corresponding spec and model to the issue or send it to me privately.

Thanks
Markus

[1] https://github.com/tlaplus/tlaplus/issues/47