^(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} ] }