state_transfer_violation_trace.txt

<<
[
 _TEAction |-> [
   position |-> 1,
   name |-> "Initial predicate",
   location |-> "Unknown location"
 ],
aux_client_acked |-> <<>>,
aux_svc |-> 0,
clients |-> 1..1,
messages |-> <<>>,
rep_client_table |-> <<<<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<0, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<>>, <<>>, <<>>>>,
rep_op_number |-> <<0, 0, 0>>,
rep_peer_op_number |-> <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<Normal, Normal, Normal>>,
rep_svc_recv |-> <<{}, {}, {}>>,
rep_view_number |-> <<1, 1, 1>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 2,
   name |-> "ReceiveClientRequest",
   location |-> "line 359, col 5 to line 386, col 95 of module VSR"
 ],
aux_client_acked |-> (v1 :> FALSE),
aux_svc |-> 0,
clients |-> 1..1,
messages |-> ([view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1),
rep_client_table |-> <<<<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<0, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>, <<>>>>,
rep_op_number |-> <<1, 0, 0>>,
rep_peer_op_number |-> <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<Normal, Normal, Normal>>,
rep_svc_recv |-> <<{}, {}, {}>>,
rep_view_number |-> <<1, 1, 1>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 3,
   name |-> "TimerSendSVC",
   location |-> "line 543, col 5 to line 553, col 97 of module VSR"
 ],
aux_client_acked |-> (v1 :> FALSE),
aux_svc |-> 1,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1),
rep_client_table |-> <<<<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<0, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>, <<>>>>,
rep_op_number |-> <<1, 0, 0>>,
rep_peer_op_number |-> <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<Normal, Normal, ViewChange>>,
rep_svc_recv |-> <<{}, {}, {}>>,
rep_view_number |-> <<1, 1, 2>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 4,
   name |-> "TimerSendSVC",
   location |-> "line 543, col 5 to line 553, col 97 of module VSR"
 ],
aux_client_acked |-> (v1 :> FALSE),
aux_svc |-> 2,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1),
rep_client_table |-> <<<<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<0, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>, <<>>>>,
rep_op_number |-> <<1, 0, 0>>,
rep_peer_op_number |-> <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<Normal, Normal, ViewChange>>,
rep_svc_recv |-> <<{}, {}, {}>>,
rep_view_number |-> <<1, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 5,
   name |-> "ReceivePrepareMsg",
   location |-> "line 394, col 5 to line 416, col 80 of module VSR"
 ],
aux_client_acked |-> (v1 :> FALSE),
aux_svc |-> 2,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1),
rep_client_table |-> <<<<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<0, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>>>,
rep_op_number |-> <<1, 1, 0>>,
rep_peer_op_number |-> <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<Normal, Normal, ViewChange>>,
rep_svc_recv |-> <<{}, {}, {}>>,
rep_view_number |-> <<1, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 6,
   name |-> "ReceivePrepareOkMsg",
   location |-> "line 424, col 4 to line 432, col 102 of module VSR"
 ],
aux_client_acked |-> (v1 :> FALSE),
aux_svc |-> 2,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1),
rep_client_table |-> <<<<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<0, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>>>,
rep_op_number |-> <<1, 1, 0>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<Normal, Normal, ViewChange>>,
rep_svc_recv |-> <<{}, {}, {}>>,
rep_view_number |-> <<1, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 7,
   name |-> "ExecuteOp",
   location |-> "line 446, col 4 to line 458, col 111 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE),
aux_svc |-> 2,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1),
rep_client_table |-> <<<<[request_number |-> 1, op_number |-> 1, executed |-> TRUE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<1, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>>>,
rep_op_number |-> <<1, 1, 0>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<Normal, Normal, ViewChange>>,
rep_svc_recv |-> <<{}, {}, {}>>,
rep_view_number |-> <<1, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 8,
   name |-> "ReceiveClientRequest",
   location |-> "line 359, col 5 to line 386, col 95 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE),
aux_svc |-> 2,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<1, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>>>,
rep_op_number |-> <<2, 1, 0>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<Normal, Normal, ViewChange>>,
rep_svc_recv |-> <<{}, {}, {}>>,
rep_view_number |-> <<1, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 9,
   name |-> "ReceiveHigherSVC",
   location |-> "line 566, col 5 to line 576, col 89 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE),
aux_svc |-> 2,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<1, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>>>,
rep_op_number |-> <<2, 1, 0>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<ViewChange, Normal, ViewChange>>,
rep_svc_recv |-> <<{[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3]}, {}, {}>>,
rep_view_number |-> <<3, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 10,
   name |-> "ReceiveMatchingSVC",
   location |-> "line 589, col 5 to line 597, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE),
aux_svc |-> 2,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<1, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>>>,
rep_op_number |-> <<2, 1, 0>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<ViewChange, Normal, ViewChange>>,
rep_svc_recv |-> <<{[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3]}, {}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<3, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 11,
   name |-> "SendDVC",
   location |-> "line 612, col 5 to line 632, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE),
aux_svc |-> 2,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 1),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<1, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>>>,
rep_op_number |-> <<2, 1, 0>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<TRUE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<ViewChange, Normal, ViewChange>>,
rep_svc_recv |-> <<{[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3]}, {}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<3, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 12,
   name |-> "TimerSendSVC",
   location |-> "line 543, col 5 to line 553, col 97 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 1),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<1, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>>>,
rep_op_number |-> <<2, 1, 0>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, FALSE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<ViewChange, Normal, ViewChange>>,
rep_svc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 13,
   name |-> "SendDVC",
   location |-> "line 612, col 5 to line 632, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 1),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<1, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>>>,
rep_op_number |-> <<2, 1, 0>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, TRUE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<ViewChange, Normal, ViewChange>>,
rep_svc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 14,
   name |-> "ReceiveMatchingDVC",
   location |-> "line 660, col 5 to line 666, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<1, 0, 0>>,
rep_dvc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0], [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<0, 0, 0>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<>>>>,
rep_op_number |-> <<2, 1, 0>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, TRUE>>,
rep_sent_sv |-> <<FALSE, FALSE, FALSE>>,
rep_status |-> <<ViewChange, Normal, ViewChange>>,
rep_svc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 15,
   name |-> "SendSV",
   location |-> "line 699, col 5 to line 723, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 0, op_number |-> 0, executed |-> TRUE]>>>>,
rep_commit_number |-> <<1, 0, 1>>,
rep_dvc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0], [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<0, 0, 3>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>>>,
rep_op_number |-> <<2, 1, 2>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, TRUE>>,
rep_sent_sv |-> <<FALSE, FALSE, TRUE>>,
rep_status |-> <<ViewChange, Normal, Normal>>,
rep_svc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 16,
   name |-> "ReceiveClientRequest",
   location |-> "line 359, col 5 to line 386, col 95 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE @@ v3 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 3, executed |-> FALSE]>>>>,
rep_commit_number |-> <<1, 0, 1>>,
rep_dvc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0], [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<0, 0, 3>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1]>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1]>>>>,
rep_op_number |-> <<2, 1, 3>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, TRUE>>,
rep_sent_sv |-> <<FALSE, FALSE, TRUE>>,
rep_status |-> <<ViewChange, Normal, Normal>>,
rep_svc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 1, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 17,
   name |-> "SendGetState",
   location |-> "line 472, col 5 to line 494, col 80 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE @@ v3 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 3, type |-> GetStateMsg, op_number |-> 0, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 3, executed |-> FALSE]>>>>,
rep_commit_number |-> <<1, 0, 1>>,
rep_dvc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0], [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<0, 3, 3>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1]>>>>,
rep_op_number |-> <<2, 0, 3>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, TRUE>>,
rep_sent_sv |-> <<FALSE, FALSE, TRUE>>,
rep_status |-> <<ViewChange, Normal, Normal>>,
rep_svc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 3, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 18,
   name |-> "ReceiveHigherSVC",
   location |-> "line 566, col 5 to line 576, col 89 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE @@ v3 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 3, type |-> GetStateMsg, op_number |-> 0, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 3, executed |-> FALSE]>>>>,
rep_commit_number |-> <<1, 0, 1>>,
rep_dvc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0], [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<0, 3, 3>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1]>>>>,
rep_op_number |-> <<2, 0, 3>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, TRUE>>,
rep_sent_sv |-> <<FALSE, FALSE, TRUE>>,
rep_status |-> <<ViewChange, ViewChange, Normal>>,
rep_svc_recv |-> <<{}, {[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1]}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 4, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 19,
   name |-> "ReceiveMatchingSVC",
   location |-> "line 589, col 5 to line 597, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE @@ v3 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 3, type |-> GetStateMsg, op_number |-> 0, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 3, executed |-> FALSE]>>>>,
rep_commit_number |-> <<1, 0, 1>>,
rep_dvc_recv |-> <<{}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0], [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<0, 3, 3>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1]>>>>,
rep_op_number |-> <<2, 0, 3>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<FALSE, FALSE, TRUE>>,
rep_sent_sv |-> <<FALSE, FALSE, TRUE>>,
rep_status |-> <<ViewChange, ViewChange, Normal>>,
rep_svc_recv |-> <<{[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2]}, {[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1]}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 4, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 20,
   name |-> "SendDVC",
   location |-> "line 612, col 5 to line 632, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE @@ v3 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 3, type |-> GetStateMsg, op_number |-> 0, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 3, executed |-> FALSE]>>>>,
rep_commit_number |-> <<1, 0, 1>>,
rep_dvc_recv |-> <<{[view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0], [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<0, 3, 3>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1]>>>>,
rep_op_number |-> <<2, 0, 3>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<TRUE, FALSE, TRUE>>,
rep_sent_sv |-> <<FALSE, FALSE, TRUE>>,
rep_status |-> <<ViewChange, ViewChange, Normal>>,
rep_svc_recv |-> <<{[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2]}, {[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1]}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 4, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 21,
   name |-> "SendDVC",
   location |-> "line 612, col 5 to line 632, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE @@ v3 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 3, type |-> GetStateMsg, op_number |-> 0, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0 @@ [view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 1, source |-> 2, log |-> <<>>, last_normal_vn |-> 3] :> 1),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 3, executed |-> FALSE]>>>>,
rep_commit_number |-> <<1, 0, 1>>,
rep_dvc_recv |-> <<{[view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0], [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<0, 3, 3>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1]>>>>,
rep_op_number |-> <<2, 0, 3>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<TRUE, TRUE, TRUE>>,
rep_sent_sv |-> <<FALSE, FALSE, TRUE>>,
rep_status |-> <<ViewChange, ViewChange, Normal>>,
rep_svc_recv |-> <<{[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2]}, {[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1]}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 4, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 22,
   name |-> "ReceiveMatchingDVC",
   location |-> "line 660, col 5 to line 666, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE @@ v3 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 3, type |-> GetStateMsg, op_number |-> 0, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0 @@ [view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 1, source |-> 2, log |-> <<>>, last_normal_vn |-> 3] :> 0),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 3, executed |-> FALSE]>>>>,
rep_commit_number |-> <<1, 0, 1>>,
rep_dvc_recv |-> <<{[view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 1, source |-> 2, log |-> <<>>, last_normal_vn |-> 3], [view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0], [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<0, 3, 3>>,
rep_log |-> <<<<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, <<>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1]>>>>,
rep_op_number |-> <<2, 0, 3>>,
rep_peer_op_number |-> <<<<0, 1, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<TRUE, TRUE, TRUE>>,
rep_sent_sv |-> <<FALSE, FALSE, TRUE>>,
rep_status |-> <<ViewChange, ViewChange, Normal>>,
rep_svc_recv |-> <<{[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2]}, {[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1]}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 4, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 23,
   name |-> "SendSV",
   location |-> "line 699, col 5 to line 723, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE @@ v3 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 3, type |-> GetStateMsg, op_number |-> 0, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 4, type |-> StartViewMsg, op_number |-> 0, commit_number |-> 1, dest |-> 2, source |-> 1, log |-> <<>>] :> 1 @@ [view_number |-> 4, type |-> StartViewMsg, op_number |-> 0, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<>>] :> 1 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0 @@ [view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 1, source |-> 2, log |-> <<>>, last_normal_vn |-> 3] :> 0),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 3, executed |-> FALSE]>>>>,
rep_commit_number |-> <<1, 0, 1>>,
rep_dvc_recv |-> <<{[view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 1, source |-> 2, log |-> <<>>, last_normal_vn |-> 3], [view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}, {}, {[view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 3, source |-> 3, log |-> <<>>, last_normal_vn |-> 0], [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}>>,
rep_last_normal_view |-> <<4, 3, 3>>,
rep_log |-> <<<<>>, <<>>, <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1]>>>>,
rep_op_number |-> <<0, 0, 3>>,
rep_peer_op_number |-> <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<TRUE, TRUE, TRUE>>,
rep_sent_sv |-> <<TRUE, FALSE, TRUE>>,
rep_status |-> <<Normal, ViewChange, Normal>>,
rep_svc_recv |-> <<{[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2]}, {[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1]}, {[view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1]}>>,
rep_view_number |-> <<4, 4, 3>>,
replicas |-> 1..3
],
[
 _TEAction |-> [
   position |-> 24,
   name |-> "ReceiveSV",
   location |-> "line 737, col 5 to line 756, col 67 of module VSR"
 ],
aux_client_acked |-> (v1 :> TRUE @@ v2 :> FALSE @@ v3 :> FALSE),
aux_svc |-> 3,
clients |-> 1..1,
messages |-> ([view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 2, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 1, source |-> 3] :> 0 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareOkMsg, op_number |-> 1, dest |-> 1, source |-> 2] :> 0 @@ [view_number |-> 3, type |-> GetStateMsg, op_number |-> 0, dest |-> 3, source |-> 2] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 2, source |-> 1] :> 0 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], op_number |-> 1, commit_number |-> 0, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 1] :> 1 @@ [view_number |-> 1, type |-> PrepareMsg, message |-> [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2], op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 1, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> PrepareMsg, message |-> [view_number |-> 3, operation |-> v3, client_id |-> 1, request_number |-> 1], op_number |-> 3, commit_number |-> 1, dest |-> 2, source |-> 3] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 3, type |-> StartViewMsg, op_number |-> 2, commit_number |-> 1, dest |-> 2, source |-> 3, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>] :> 1 @@ [view_number |-> 4, type |-> StartViewMsg, op_number |-> 0, commit_number |-> 1, dest |-> 2, source |-> 1, log |-> <<>>] :> 1 @@ [view_number |-> 4, type |-> StartViewMsg, op_number |-> 0, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<>>] :> 0 @@ [view_number |-> 3, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 3, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0] :> 0 @@ [view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 1, source |-> 2, log |-> <<>>, last_normal_vn |-> 3] :> 0),
rep_client_table |-> <<<<[request_number |-> 2, op_number |-> 2, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 1, executed |-> FALSE]>>, <<[request_number |-> 1, op_number |-> 3, executed |-> FALSE]>>>>,
rep_commit_number |-> <<1, 0, 1>>,
rep_dvc_recv |-> <<{[view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 0, commit_number |-> 0, dest |-> 1, source |-> 2, log |-> <<>>, last_normal_vn |-> 3], [view_number |-> 4, type |-> DoViewChangeMsg, op_number |-> 2, commit_number |-> 1, dest |-> 1, source |-> 1, log |-> <<[view_number |-> 1, operation |-> v1, client_id |-> 1, request_number |-> 1], [view_number |-> 1, operation |-> v2, client_id |-> 1, request_number |-> 2]>>, last_normal_vn |-> 0]}, {}, {}>>,
rep_last_normal_view |-> <<4, 3, 4>>,
rep_log |-> <<<<>>, <<>>, <<>>>>,
rep_op_number |-> <<0, 0, 0>>,
rep_peer_op_number |-> <<<<0, 0, 0>>, <<0, 0, 0>>, <<0, 0, 0>>>>,
rep_sent_dvc |-> <<TRUE, TRUE, FALSE>>,
rep_sent_sv |-> <<TRUE, FALSE, FALSE>>,
rep_status |-> <<Normal, ViewChange, Normal>>,
rep_svc_recv |-> <<{[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 1, source |-> 2]}, {[view_number |-> 4, type |-> StartViewChangeMsg, dest |-> 2, source |-> 1]}, {}>>,
rep_view_number |-> <<4, 4, 4>>,
replicas |-> 1..3
]
>>