Skip to content

Instantly share code, notes, and snippets.

@Alexander-N

Alexander-N/good-trace.out

Created April 9, 2021 00:22
Show Gist options
  • Save Alexander-N/ea7bbe6ddadf10f6d1500316b643a354 to your computer and use it in GitHub Desktop.
Save Alexander-N/ea7bbe6ddadf10f6d1500316b643a354 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
good-trace.out
.* Event = "(?<event>.*)"(.|\n)*?Host = (?<host>.*)(.|\n)*?VectorClock = "(?<clock>.*)"(.|\n)*?value = (?<values>.*)
@!@!@ENDMSG 2264 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ localVectorClock = ( Database :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = (ClientA :> Null @@ ClientB :> Null)
/\ pc = ( ClientA :> "SendDatabase" @@
ClientB :> "SendDatabase" @@
Database :> "Receive" @@
Cache :> "Receive" )
/\ receivedMessage = (Database :> Null @@ Cache :> Null)
/\ localVectorClock_ = ( ClientA :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ Event = Null
/\ Host = Null
/\ VectorClock = (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0)
/\ received = (Database :> 0 @@ Cache :> 0)
/\ Messages = (ClientA :> <<>> @@ ClientB :> <<>> @@ Database :> <<>> @@ Cache :> <<>>)
/\ value = (Database :> Null @@ Cache :> Null)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <SendDatabase line 140, col 23 to line 155, col 74 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = (ClientA :> Null @@ ClientB :> Null)
/\ pc = ( ClientA :> "SendDatabase" @@
ClientB :> "GetAckDatabase" @@
Database :> "Receive" @@
Cache :> "Receive" )
/\ receivedMessage = (Database :> Null @@ Cache :> Null)
/\ localVectorClock_ = ( ClientA :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0) )
/\ Event = "SendDatabase"
/\ Host = ClientB
/\ VectorClock = "{\"ClientA\":0,\"ClientB\":1,\"Database\":0,\"Cache\":0}"
/\ received = (Database :> 0 @@ Cache :> 0)
/\ Messages = ( ClientA :> <<>> @@
ClientB :> <<>> @@
Database :>
<< [ clock |->
(ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientB,
destination |-> Database,
source |-> ClientB ] >> @@
Cache :> <<>> )
/\ value = (Database :> Null @@ Cache :> Null)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
3: <SendDatabase line 140, col 23 to line 155, col 74 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = (ClientA :> Null @@ ClientB :> Null)
/\ pc = ( ClientA :> "GetAckDatabase" @@
ClientB :> "GetAckDatabase" @@
Database :> "Receive" @@
Cache :> "Receive" )
/\ receivedMessage = (Database :> Null @@ Cache :> Null)
/\ localVectorClock_ = ( ClientA :> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0) )
/\ Event = "SendDatabase"
/\ Host = ClientA
/\ VectorClock = "{\"ClientA\":1,\"ClientB\":0,\"Database\":0,\"Cache\":0}"
/\ received = (Database :> 0 @@ Cache :> 0)
/\ Messages = ( ClientA :> <<>> @@
ClientB :> <<>> @@
Database :>
<< [ clock |->
(ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientB,
destination |-> Database,
source |-> ClientB ],
[ clock |->
(ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] >> @@
Cache :> <<>> )
/\ value = (Database :> Null @@ Cache :> Null)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
4: <Receive line 205, col 18 to line 216, col 71 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 1 @@ Cache :> 0) @@
Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = (ClientA :> Null @@ ClientB :> Null)
/\ pc = ( ClientA :> "GetAckDatabase" @@
ClientB :> "GetAckDatabase" @@
Database :> "SendAck" @@
Cache :> "Receive" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientB,
destination |-> Database,
source |-> ClientB ] @@
Cache :> Null )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0) )
/\ Event = "Receive"
/\ Host = Database
/\ VectorClock = "{\"ClientA\":0,\"ClientB\":1,\"Database\":1,\"Cache\":0}"
/\ received = (Database :> 1 @@ Cache :> 0)
/\ Messages = ( ClientA :> <<>> @@
ClientB :> <<>> @@
Database :>
<< [ clock |->
(ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] >> @@
Cache :> <<>> )
/\ value = (Database :> ClientB @@ Cache :> Null)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
5: <SendAck line 218, col 18 to line 235, col 61 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0) @@
Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = (ClientA :> Null @@ ClientB :> Null)
/\ pc = ( ClientA :> "GetAckDatabase" @@
ClientB :> "GetAckDatabase" @@
Database :> "Receive" @@
Cache :> "Receive" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientB,
destination |-> Database,
source |-> ClientB ] @@
Cache :> Null )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0) )
/\ Event = "SendAck"
/\ Host = Database
/\ VectorClock = "{\"ClientA\":0,\"ClientB\":1,\"Database\":2,\"Cache\":0}"
/\ received = (Database :> 1 @@ Cache :> 0)
/\ Messages = ( ClientA :> <<>> @@
ClientB :>
<< [ clock |->
(ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] >> @@
Database :>
<< [ clock |->
(ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] >> @@
Cache :> <<>> )
/\ value = (Database :> ClientB @@ Cache :> Null)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
6: <Receive line 205, col 18 to line 216, col 71 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 3 @@ Cache :> 0) @@
Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = (ClientA :> Null @@ ClientB :> Null)
/\ pc = ( ClientA :> "GetAckDatabase" @@
ClientB :> "GetAckDatabase" @@
Database :> "SendAck" @@
Cache :> "Receive" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :> Null )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0) )
/\ Event = "Receive"
/\ Host = Database
/\ VectorClock = "{\"ClientA\":1,\"ClientB\":1,\"Database\":3,\"Cache\":0}"
/\ received = (Database :> 2 @@ Cache :> 0)
/\ Messages = ( ClientA :> <<>> @@
ClientB :>
<< [ clock |->
(ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] >> @@
Database :> <<>> @@
Cache :> <<>> )
/\ value = (Database :> ClientA @@ Cache :> Null)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
7: <SendAck line 218, col 18 to line 235, col 61 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = (ClientA :> Null @@ ClientB :> Null)
/\ pc = ( ClientA :> "GetAckDatabase" @@
ClientB :> "GetAckDatabase" @@
Database :> "Done" @@
Cache :> "Receive" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :> Null )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0) )
/\ Event = "SendAck"
/\ Host = Database
/\ VectorClock = "{\"ClientA\":1,\"ClientB\":1,\"Database\":4,\"Cache\":0}"
/\ received = (Database :> 2 @@ Cache :> 0)
/\ Messages = ( ClientA :>
<< [ clock |->
(ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientA,
source |-> Database ] >> @@
ClientB :>
<< [ clock |->
(ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] >> @@
Database :> <<>> @@
Cache :> <<>> )
/\ value = (Database :> ClientA @@ Cache :> Null)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
8: <GetAckDatabase line 157, col 25 to line 169, col 59 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = ( ClientA :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientA,
source |-> Database ] @@
ClientB :> Null )
/\ pc = ( ClientA :> "SendCache" @@
ClientB :> "GetAckDatabase" @@
Database :> "Done" @@
Cache :> "Receive" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :> Null )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 2 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 0 @@ Cache :> 0) )
/\ Event = "GetAckDatabase"
/\ Host = ClientA
/\ VectorClock = "{\"ClientA\":2,\"ClientB\":1,\"Database\":4,\"Cache\":0}"
/\ received = (Database :> 2 @@ Cache :> 0)
/\ Messages = ( ClientA :> <<>> @@
ClientB :>
<< [ clock |->
(ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] >> @@
Database :> <<>> @@
Cache :> <<>> )
/\ value = (Database :> ClientA @@ Cache :> Null)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
9: <GetAckDatabase line 157, col 25 to line 169, col 59 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = ( ClientA :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientA,
source |-> Database ] @@
ClientB :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] )
/\ pc = ( ClientA :> "SendCache" @@
ClientB :> "SendCache" @@
Database :> "Done" @@
Cache :> "Receive" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :> Null )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 2 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 2 @@ Database :> 2 @@ Cache :> 0) )
/\ Event = "GetAckDatabase"
/\ Host = ClientB
/\ VectorClock = "{\"ClientA\":0,\"ClientB\":2,\"Database\":2,\"Cache\":0}"
/\ received = (Database :> 2 @@ Cache :> 0)
/\ Messages = (ClientA :> <<>> @@ ClientB :> <<>> @@ Database :> <<>> @@ Cache :> <<>>)
/\ value = (Database :> ClientA @@ Cache :> Null)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
10: <SendCache line 171, col 20 to line 186, col 71 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = ( ClientA :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientA,
source |-> Database ] @@
ClientB :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] )
/\ pc = ( ClientA :> "GetAckCache" @@
ClientB :> "SendCache" @@
Database :> "Done" @@
Cache :> "Receive" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :> Null )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 2 @@ Database :> 2 @@ Cache :> 0) )
/\ Event = "SendCache"
/\ Host = ClientA
/\ VectorClock = "{\"ClientA\":3,\"ClientB\":1,\"Database\":4,\"Cache\":0}"
/\ received = (Database :> 2 @@ Cache :> 0)
/\ Messages = ( ClientA :> <<>> @@
ClientB :> <<>> @@
Database :> <<>> @@
Cache :>
<< [ clock |->
(ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> ClientA,
destination |-> Cache,
source |-> ClientA ] >> )
/\ value = (Database :> ClientA @@ Cache :> Null)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
11: <Receive line 205, col 18 to line 216, col 71 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 1) )
/\ receivedMessage_ = ( ClientA :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientA,
source |-> Database ] @@
ClientB :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] )
/\ pc = ( ClientA :> "GetAckCache" @@
ClientB :> "SendCache" @@
Database :> "Done" @@
Cache :> "SendAck" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :>
[ clock |-> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> ClientA,
destination |-> Cache,
source |-> ClientA ] )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 2 @@ Database :> 2 @@ Cache :> 0) )
/\ Event = "Receive"
/\ Host = Cache
/\ VectorClock = "{\"ClientA\":3,\"ClientB\":1,\"Database\":4,\"Cache\":1}"
/\ received = (Database :> 2 @@ Cache :> 1)
/\ Messages = (ClientA :> <<>> @@ ClientB :> <<>> @@ Database :> <<>> @@ Cache :> <<>>)
/\ value = (Database :> ClientA @@ Cache :> ClientA)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
12: <SendAck line 218, col 18 to line 235, col 61 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2) )
/\ receivedMessage_ = ( ClientA :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientA,
source |-> Database ] @@
ClientB :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] )
/\ pc = ( ClientA :> "GetAckCache" @@
ClientB :> "SendCache" @@
Database :> "Done" @@
Cache :> "Receive" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :>
[ clock |-> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> ClientA,
destination |-> Cache,
source |-> ClientA ] )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 2 @@ Database :> 2 @@ Cache :> 0) )
/\ Event = "SendAck"
/\ Host = Cache
/\ VectorClock = "{\"ClientA\":3,\"ClientB\":1,\"Database\":4,\"Cache\":2}"
/\ received = (Database :> 2 @@ Cache :> 1)
/\ Messages = ( ClientA :>
<< [ clock |->
(ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2),
value |-> Ack,
destination |-> ClientA,
source |-> Cache ] >> @@
ClientB :> <<>> @@
Database :> <<>> @@
Cache :> <<>> )
/\ value = (Database :> ClientA @@ Cache :> ClientA)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
13: <GetAckCache line 188, col 22 to line 200, col 56 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2) )
/\ receivedMessage_ = ( ClientA :>
[ clock |-> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2),
value |-> Ack,
destination |-> ClientA,
source |-> Cache ] @@
ClientB :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] )
/\ pc = ( ClientA :> "Done" @@
ClientB :> "SendCache" @@
Database :> "Done" @@
Cache :> "Receive" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :>
[ clock |-> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> ClientA,
destination |-> Cache,
source |-> ClientA ] )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 4 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 2 @@ Database :> 2 @@ Cache :> 0) )
/\ Event = "GetAckCache"
/\ Host = ClientA
/\ VectorClock = "{\"ClientA\":4,\"ClientB\":1,\"Database\":4,\"Cache\":2}"
/\ received = (Database :> 2 @@ Cache :> 1)
/\ Messages = (ClientA :> <<>> @@ ClientB :> <<>> @@ Database :> <<>> @@ Cache :> <<>>)
/\ value = (Database :> ClientA @@ Cache :> ClientA)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
14: <SendCache line 171, col 20 to line 186, col 71 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2) )
/\ receivedMessage_ = ( ClientA :>
[ clock |-> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2),
value |-> Ack,
destination |-> ClientA,
source |-> Cache ] @@
ClientB :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] )
/\ pc = ( ClientA :> "Done" @@
ClientB :> "GetAckCache" @@
Database :> "Done" @@
Cache :> "Receive" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :>
[ clock |-> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0),
value |-> ClientA,
destination |-> Cache,
source |-> ClientA ] )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 4 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 3 @@ Database :> 2 @@ Cache :> 0) )
/\ Event = "SendCache"
/\ Host = ClientB
/\ VectorClock = "{\"ClientA\":0,\"ClientB\":3,\"Database\":2,\"Cache\":0}"
/\ received = (Database :> 2 @@ Cache :> 1)
/\ Messages = ( ClientA :> <<>> @@
ClientB :> <<>> @@
Database :> <<>> @@
Cache :>
<< [ clock |->
(ClientA :> 0 @@ ClientB :> 3 @@ Database :> 2 @@ Cache :> 0),
value |-> ClientB,
destination |-> Cache,
source |-> ClientB ] >> )
/\ value = (Database :> ClientA @@ Cache :> ClientA)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
15: <Receive line 205, col 18 to line 216, col 71 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 3 @@ ClientB :> 3 @@ Database :> 4 @@ Cache :> 3) )
/\ receivedMessage_ = ( ClientA :>
[ clock |-> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2),
value |-> Ack,
destination |-> ClientA,
source |-> Cache ] @@
ClientB :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] )
/\ pc = ( ClientA :> "Done" @@
ClientB :> "GetAckCache" @@
Database :> "Done" @@
Cache :> "SendAck" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 3 @@ Database :> 2 @@ Cache :> 0),
value |-> ClientB,
destination |-> Cache,
source |-> ClientB ] )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 4 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 3 @@ Database :> 2 @@ Cache :> 0) )
/\ Event = "Receive"
/\ Host = Cache
/\ VectorClock = "{\"ClientA\":3,\"ClientB\":3,\"Database\":4,\"Cache\":3}"
/\ received = (Database :> 2 @@ Cache :> 2)
/\ Messages = (ClientA :> <<>> @@ ClientB :> <<>> @@ Database :> <<>> @@ Cache :> <<>>)
/\ value = (Database :> ClientA @@ Cache :> ClientB)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
16: <SendAck line 218, col 18 to line 235, col 61 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 3 @@ ClientB :> 3 @@ Database :> 4 @@ Cache :> 4) )
/\ receivedMessage_ = ( ClientA :>
[ clock |-> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2),
value |-> Ack,
destination |-> ClientA,
source |-> Cache ] @@
ClientB :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 1 @@ Database :> 2 @@ Cache :> 0),
value |-> Ack,
destination |-> ClientB,
source |-> Database ] )
/\ pc = ( ClientA :> "Done" @@
ClientB :> "GetAckCache" @@
Database :> "Done" @@
Cache :> "Done" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 3 @@ Database :> 2 @@ Cache :> 0),
value |-> ClientB,
destination |-> Cache,
source |-> ClientB ] )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 4 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2) @@
ClientB :> (ClientA :> 0 @@ ClientB :> 3 @@ Database :> 2 @@ Cache :> 0) )
/\ Event = "SendAck"
/\ Host = Cache
/\ VectorClock = "{\"ClientA\":3,\"ClientB\":3,\"Database\":4,\"Cache\":4}"
/\ received = (Database :> 2 @@ Cache :> 2)
/\ Messages = ( ClientA :> <<>> @@
ClientB :>
<< [ clock |->
(ClientA :> 3 @@ ClientB :> 3 @@ Database :> 4 @@ Cache :> 4),
value |-> Ack,
destination |-> ClientB,
source |-> Cache ] >> @@
Database :> <<>> @@
Cache :> <<>> )
/\ value = (Database :> ClientA @@ Cache :> ClientB)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
17: <GetAckCache line 188, col 22 to line 200, col 56 of module dual_writes_vector_clock>
/\ localVectorClock = ( Database :> (ClientA :> 1 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 0) @@
Cache :> (ClientA :> 3 @@ ClientB :> 3 @@ Database :> 4 @@ Cache :> 4) )
/\ receivedMessage_ = ( ClientA :>
[ clock |-> (ClientA :> 3 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2),
value |-> Ack,
destination |-> ClientA,
source |-> Cache ] @@
ClientB :>
[ clock |-> (ClientA :> 3 @@ ClientB :> 3 @@ Database :> 4 @@ Cache :> 4),
value |-> Ack,
destination |-> ClientB,
source |-> Cache ] )
/\ pc = ( ClientA :> "Done" @@
ClientB :> "Done" @@
Database :> "Done" @@
Cache :> "Done" )
/\ receivedMessage = ( Database :>
[ clock |-> (ClientA :> 1 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0),
value |-> ClientA,
destination |-> Database,
source |-> ClientA ] @@
Cache :>
[ clock |-> (ClientA :> 0 @@ ClientB :> 3 @@ Database :> 2 @@ Cache :> 0),
value |-> ClientB,
destination |-> Cache,
source |-> ClientB ] )
/\ localVectorClock_ = ( ClientA :> (ClientA :> 4 @@ ClientB :> 1 @@ Database :> 4 @@ Cache :> 2) @@
ClientB :> (ClientA :> 3 @@ ClientB :> 4 @@ Database :> 4 @@ Cache :> 4) )
/\ Event = "GetAckCache"
/\ Host = ClientB
/\ VectorClock = "{\"ClientA\":3,\"ClientB\":4,\"Database\":4,\"Cache\":4}"
/\ received = (Database :> 2 @@ Cache :> 2)
/\ Messages = (ClientA :> <<>> @@ ClientB :> <<>> @@ Database :> <<>> @@ Cache :> <<>>)
/\ value = (Database :> ClientA @@ Cache :> ClientB)
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2218:4 @!@!@
18: Stuttering
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment