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

[tlaplus] Fail to visualize my own error trace in ShiViz

Dear all,

I am trying the "error-trace visualization" features introduced in the new TLC version (1.6.0 of 10 July 2019),
following Issue #267: Self-referential error trace exploration: _TEPosition and _TETrace operators.

I succeeded in visualizing error-trace.txt provided as an example in ShiViz.

However, I failed to visualize my own error-trace (see the attachment) and got the following error info:
"The parser RegExp you entered does not capture any events for the execution".
I don't quite understand the regexp and I just modify the one in the example file.

What is wrong with my error trace file?

Best regards,
hengxin

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/574f7b98-9c48-4053-b34b-e629256088e6%40googlegroups.com.
^(State ){0,1}(\d*): <(?<event>(?!Initial predicate).*)>\n\/\\ Clock = (?<clock>.*)\n\/\\ pc = (.*)\n\/\\ state = (.*)\n\/\\ Host = (?<host>.*)\n\/\\ msgs = (?<msgs>.*)

1: <Initial predicate>
/\ Clock = {"'p1':'0'", "'p2':'0'", "'p3':'0'"}
/\ pc = (p1 :> 0 @@ p2 :> 0 @@ p3 :> 0)
/\ state = ( p1 :>
      ( p1 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p2 :>
      ( p1 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p3 :>
      ( p1 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) )
/\ Host = "Init"
/\ msgs = {}

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
p1 Prepare
2: <next_1564409667341417000 line 396, col 3 to line 465, col 2 of module TE>
/\ Clock = {"'p2':'0'", "'p3':'0'", "'p1':'1'"}
/\ pc = (p1 :> 1 @@ p2 :> 0 @@ p3 :> 0)
/\ state = ( p1 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p2 :>
      ( p1 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p3 :>
      ( p1 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) )
/\ Host = p1
/\ msgs = { [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Prepare",
    from |-> p1,
    to |-> {p1, p2, p3} ] }

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
p2 OnMessage from p1
3: <next_1564409667341417000 line 467, col 3 to line 549, col 2 of module TE>
/\ Clock = {"'p3':'0'", "'p1':'1'", "'p2':'1'"}
/\ pc = (p1 :> 1 @@ p2 :> 1 @@ p3 :> 0)
/\ state = ( p1 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p2 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p3 :>
      ( p1 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) )
/\ Host = p2
/\ msgs = { [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Prepare",
    from |-> p1,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p2,
    to |-> {p1} ] }

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
p2 Accept (0, 0, v1)
4: <next_1564409667341417000 line 551, col 3 to line 647, col 2 of module TE>
/\ Clock = {"'p3':'0'", "'p1':'1'", "'p2':'2'"}
/\ pc = (p1 :> 1 @@ p2 :> 2 @@ p3 :> 0)
/\ state = ( p1 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p2 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p3 :>
      ( p1 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) )
/\ Host = p2
/\ msgs = { [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Prepare",
    from |-> p1,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p2,
    to |-> {p1} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Accept",
    from |-> p2,
    to |-> {p1, p2, p3} ] }

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
p1 OnMessage: chosen = {v1}
5: <next_1564409667341417000 line 649, col 3 to line 759, col 2 of module TE>
/\ Clock = {"'p3':'0'", "'p2':'2'", "'p1':'2'"}
/\ pc = (p1 :> 2 @@ p2 :> 2 @@ p3 :> 0)
/\ state = ( p1 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p2 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p3 :>
      ( p1 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) )
/\ Host = p1
/\ msgs = { [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Prepare",
    from |-> p1,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p2,
    to |-> {p1} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Accept",
    from |-> p2,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p1,
    to |-> {p2} ] }

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
p3 OnMessage (from p1)
6: <next_1564409667341417000 line 761, col 3 to line 885, col 2 of module TE>
/\ Clock = {"'p2':'2'", "'p1':'2'", "'p3':'1'"}
/\ pc = (p1 :> 2 @@ p2 :> 2 @@ p3 :> 1)
/\ state = ( p1 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p2 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p3 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] ) )
/\ Host = p3
/\ msgs = { [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Prepare",
    from |-> p1,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p3,
    to |-> {p1} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p2,
    to |-> {p1} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Accept",
    from |-> p2,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p1,
    to |-> {p2} ] }

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
p3 Accept (0, 0, v2)
7: <next_1564409667341417000 line 887, col 3 to line 1025, col 2 of module TE>
/\ Clock = {"'p2':'2'", "'p1':'2'", "'p3':'2'"}
/\ pc = (p1 :> 2 @@ p2 :> 2 @@ p3 :> 2)
/\ state = ( p1 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p2 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p3 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v2] ) )
/\ Host = p3
/\ msgs = { [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Prepare",
    from |-> p1,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p3,
    to |-> {p1} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v2] ),
    type |-> "Accept",
    from |-> p3,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p2,
    to |-> {p1} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Accept",
    from |-> p2,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p1,
    to |-> {p2} ] }

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
p2 OnMessage (from p3): chosen = {v1, v2}
8: <next_1564409667341417000 line 1027, col 3 to line 1179, col 2 of module TE>
/\ Clock = {"'p1':'2'", "'p3':'2'", "'p2':'3'"}
/\ pc = (p1 :> 2 @@ p2 :> 3 @@ p3 :> 2)
/\ state = ( p1 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
        p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ) @@
  p2 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v2] @@
        p3 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v2] ) @@
  p3 :>
      ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
        p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
        p3 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v2] ) )
/\ Host = p2
/\ msgs = { [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Prepare",
    from |-> p1,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p3,
    to |-> {p1} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v2] ),
    type |-> "Accept",
    from |-> p3,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p2,
    to |-> {p1} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "Accept",
    from |-> p2,
    to |-> {p1, p2, p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> -1, maxVVal |-> None] @@
          p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v2] @@
          p3 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v2] ),
    type |-> "ACK",
    from |-> p2,
    to |-> {p3} ],
  [ state |->
        ( p1 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p2 :> [maxBal |-> 0, maxVBal |-> 0, maxVVal |-> v1] @@
          p3 :> [maxBal |-> -1, maxVBal |-> -1, maxVVal |-> None] ),
    type |-> "ACK",
    from |-> p1,
    to |-> {p2} ] }