[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

TLA+ Toolbox 1.5.3 not displaying error trace



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.