From 712b1215b8f0c45f01b8949522d60e0e8d05b028 Mon Sep 17 00:00:00 2001
From: Zong Xun <63457492+Zxun2@users.noreply.github.com>
Date: Sat, 16 Nov 2024 22:59:45 +0800
Subject: [PATCH] Add traces

---
 traces.txt | 833 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 833 insertions(+)
 create mode 100644 traces.txt

diff --git a/traces.txt b/traces.txt
new file mode 100644
index 0000000..0309d03
--- /dev/null
+++ b/traces.txt
@@ -0,0 +1,833 @@
+// Scenario 0 Trace - No Error
+init
+start
+[if((global_elected_leader == 0])]  ------------------------------------------ checks if proposer is elected
+client_proposer.123 ---------------------------------------------------------- client proposed value 123
+[if![(global_id >=1]]
+prepare_channel[0].0.1.PASS -------------------------------------------------- proposer 0 send over prepare message with value 1 
+prepare_channel[1].0.1.PASS
+prepare_channel[2].0.1.PASS
+[if!(prepare_reads < quorums])] ---------------------------------------------- validation for number of successful prepare messages 
+[if(prepare_reads>=quorums)])
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if![[[acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)
+[if![((acceptor_prepare_status[1] == FAIL) II (acceptor_status[1] == FAIL]
+[if![[(acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL]
+promise_channel[0].1.-1.PASS ------------------------------------------------- acceptors send over promise message with value 1
+promise_channel[1].1.-1.PASS
+promise_channel[2].1.-1.PASS
+[if!(promise_received < quorums])] ------------------------------------------- validation for number of promise message received
+[if((promise_received >= quorums])]
+reset_promise_count
+[if!global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[ifflglobal_accepted_value == -(1)])]
+accept_channel[0].PASS.1.123.PASS -------------------------------------------- proposer sends accept message denoting the proposed value 123 and id 1
+accept_channel[1]PASS.1.123.PASS
+accept_channel[2]PASS.1.123.PASS
+proposer_did_not_fail_when_sending_accept ------------------------------------ if proposer did not fail when sending the accept messages, we need to let the model know
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learne[1].123.PASS
+accepted_channel_proposer.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+[if![(client_consensus == -[1])]
+learner_client.0.123 --------------------------------------------------------- learner received all the accepted messages and sends it to client
+accepted_channel_proposer.123.PASS
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if! global_terminate]]
+[if![retry]]
+accepted_channel_learner[1].123.PASS
+[if![[client_consensus == -{1])]
+learner_client.1.123 --------------------------------------------------------- learner received all the accepted messages and sends it to client
+finish
+
+// Scenario 1 Trace - Acceptor Fails
+init
+start
+[if[[[global_elected_leader == 0])] ------------------------------------------ checks if proposer is elected
+client_proposer.123 ---------------------------------------------------------- client proposed value 123
+[if![[global_id>=1])]
+prepare_channel[0].0.1.PASS -------------------------------------------------- proposer 0 send over prepare message with value 1 
+prepare_channel[1].0.1.PASS
+prepare_channel[2].0.1.PASS
+[if!(prepare_reads < quorums])] ---------------------------------------------- validation for number of successful prepare messages 
+[if(prepare_reads>=quorums)])
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if!(((acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)
+[if!(((acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL)
+[if!(((acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL)
+promise_channel[0].1.-1.PASS ------------------------------------------------- acceptors send over promise message with value 1
+promise_channel[1].1.-1.PASS
+promise_channel[2].1.-1.ACCEPTOR_FAILED -------------------------------------- acceptor 2 failed when sending promise message with value 1
+[if!((promise_received < quorums])]
+[if[[promise_received >= quorums])] ------------------------------------------ remains valid because promise_received >= quorums
+reset_promise_count
+[if!global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if([global_accepted_value == -(1))]
+accept_channel[0].PASS.1.123.PASS
+accept_channel[1].PASS.1.123.PASS
+accept_channel[2].PASS.1.123.FAIL -------------------------------------------- accept message failed to send
+proposer_did_not_fail_when_sending_accept ------------------------------------ if proposer did not fail when sending the accept messages, we need to let the model know
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer 123.PASS
+accepted_channel_learner[0].123.PASS
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer 123.PASS
+accepted_channel_learner[0].-1.NACK ------------------------------------------ NACK for accepted message if broadcast is from a failed acceptor node
+[if![[client_consensus == -[1])]
+learner_client.0.123 --------------------------------------------------------- learner received all the accepted messages and sends it to client
+accepted_channel_learner[1].-1.NACK
+[if![(client_consensus == -(1)])]
+learner_client.1.123
+finish
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if! global_terminate]]
+[if![retry]]
+
+// Scenario 2 - Redundant Learner
+init
+start
+[if((global_elected_leader == 0])]  ------------------------------------------ checks if proposer is elected
+client_proposer.123 ---------------------------------------------------------- client proposed value 123
+[if![(global_id >=1]]
+prepare_channel[0].0.1.PASS -------------------------------------------------- proposer 0 send over prepare message with value 1 
+prepare_channel[1].0.1.PASS
+prepare_channel[2].0.1.PASS
+[if!(prepare_reads < quorums])] ---------------------------------------------- validation for number of successful prepare messages 
+[if(prepare_reads>=quorums)])
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if![[[acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)
+[if![[[acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL)
+[if![[[acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL)
+promise_channel[0].1.-1.PASS ------------------------------------------------- acceptors send over promise message with value 1
+promise_channel[1].1.-1.PASS
+promise_channel[2].1.-1.PASS
+[if![promise_received < quorums])]
+[if[[promise_received >= quorums])] ------------------------------------------ remains valid because promise_received >= quorums
+reset_promise_count
+[if! global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if[[global_accepted_value == -(1)])]
+accept_channel[0].PASS.1.123.PASS
+accept_channel[1]PASS.1.123.PASS
+accept_channel[2]PASS.1.123.PASS
+proposer_did_not_fail_when_sending_accept ------------------------------------ if proposer did not fail when sending the accept messages, we need to let the model know
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learne[1].123.PASS
+accepted_channel_proposer.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer 123.PASS
+accepted_channel_proposer.123.PASS
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if! global_terminate]]
+[if![retry]]
+accepted_channel_learner[0].123.PASS
+[if![[client_consensus == -(1)])
+learner_client.1.123 --------------------------------------------------------- learner received all the accepted messages and sends it to client
+accepted_channel_learner[1].123.PASS
+[if![[client_consensus == -{1])]
+learner_client.1.FAIL -------------------------------------------------------- learner fails and cannot send to client
+finish
+
+// Scenario 3 - proposer fails
+init
+start
+[if((global_elected_leader == 0])]  ------------------------------------------ checks if proposer is elected
+client_proposer.123 ---------------------------------------------------------- client proposed value 123
+[if![(global_id >=1]]
+prepare_channel[0].0.1.PASS -------------------------------------------------- proposer 0 send over prepare message with value 1 
+prepare_channel[1].0.1.PASS
+prepare_channel[2].0.1.PASS
+[if!(prepare_reads < quorums])]
+[if(prepare_reads >=quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[i!![[(acceptor_prepare_status[0] == FAIL) II (acceptor_status[0] == FAIL]
+[if![[[acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL)
+[i!![[(acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL)
+promise_channel[0].1.-1.PASS ------------------------------------------------- acceptors send over promise message with value 1
+promise_channel[1].1.-1.PASS
+promise_channel[2].1.-1.PASS
+[if!(promise_received < quorums)]]
+[if((promise_received >= quorums)]
+reset_promise_count
+[if![global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if!([global_accepted_value == -(1)])]
+accept_channel[0].PASS.1.123.PASS
+proposer_fails --------------------------------------------------------------- proposer fails, all subsequent accept messages will fail as well (and accepted messages will NACK)
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer 123.PASS
+accept_channel[1].FAIL.1.123.PASS
+accept_channel[2].FAIL.1.123.PASS  ------------------------------------------- accept message failed
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.-1.NACK
+accepted_channel_learner[0].-1.NACK
+[if![(client_consensus == -[1])]
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+accepted_channel_learner[1].-1.NACK
+[if![(client_consensus == -(1)])]
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+accepted_channel_proposer.-1.NACK
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if[global_terminate]]
+[if((0== 0)]
+reset[0].1.FAIL
+reset[1].1.FAIL
+reset[2].1.FAIL
+elect_new_leader ------------------------------------------------------------- new leader elected, all acceptor states reset
+[if[[[global_elected_leader==1])] -------------------------------------------- check if current proposer is the elected leader
+client_does_not_propose_value
+[if!((global_id>=2)]]
+prepare_channel[0].1.2.PASS -------------------------------------------------- sends prepare message with value 2
+prepare_channel[1].1.2.PASS
+prepare_channel[2].1.2.PASS
+[if![[prepare_reads < quorums])]
+[if[[prepare_reads >=quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[i!![[[acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)
+[i!![[(acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL)
+[i!!(((acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL)
+promise_channel[0].2.123.PASS
+promise_channel[1].2.-1.PASS
+promise_channel[2].2.-1.PASS
+[if![[promise_received < quorums])]
+[if[[promise_received >= quorums])] ------------------------------------------ remains valid because promise_received >= quorums
+reset_promise_count
+[if! (global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if!((global_accepted_value == -(1)])]
+proposer_did_not_fail_when_sending_accept ------------------------------------ if proposer did not fail when sending the accept messages, we need to let the model know
+accept_channel[0].PASS.2.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accept_channel[1].PASS.2.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accept_channel[2].PASS.2.123.PASS
+accepted_channel_learner[1].123.PASS
+accepted_channel_leamer[0].123.PASS
+[if!((client_consensus == -(1)])]
+[if!(client_consensus == -(1)])]
+learner_client.1.123 --------------------------------------------------------- learner received all the accepted messages and sends it to client
+learner_client.1.123
+finish
+accepted_channel_proposer 123.PASS
+accepted_channel_proposer.123.PASS
+accepted_channel_proposer 123.PASS
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if![global_terminate]]
+[if![retry]]
+
+// Scenario 4 - multiple proposers conflict
+init
+start
+[if((global_elected_leader == 0])]  ------------------------------------------ checks if proposer is elected
+client_proposer.123 ---------------------------------------------------------- client proposed value 123
+[if![(global_id >=1]]
+prepare_channel[0].0.1.PASS -------------------------------------------------- proposer 0 send over prepare message with value 1 
+prepare_channel[1].0.1.PASS
+prepare_channel[2].0.1.PASS
+[if![[prepare_reads < quorums])]
+[if(prepare_reads >= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if![[[(acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL
+[if![[[[acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL
+[if![[[(acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL
+promise_channel[0].1.-1.PASS ------------------------------------------------- acceptors send over promise message with value 1
+promise_channel[1].1.-1.PASS
+promise_channel[2].1.-1.PASS
+[if!(promise_received < quorums])]
+[if((promise_received >=quorums])]
+reset_promise_count
+[if!(global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if[[global_accepted_value == -(1)])]
+proposer_fails --------------------------------------------------------------- proposer fails, all subsequent accept messages will fail as well (and accepted messages will NACK)
+accept_channel[0].FAIL.1.123.PASS
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.-1.NACK
+accept_channel[1].FAIL.1.123.PASS
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.-1.NACK
+accept_channel[2].FAIL.1.123.PASS  ------------------------------------------- accept message failed
+accepted_channel_learner[0].-1.NACK
+[if[[client_consensus == -[1])]
+accepted_channel_learner[1].-1.NACK
+[if[[(client_consensus == -[1])]
+accepted_channel_proposer.-1.NACK
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if[global_terminate]]
+[if((0 == 0)]
+reset[0].1.FAIL
+reset[1].1.FAIL
+reset[2].1.FAIL
+elect_new_leader ------------------------------------------------------------- new leader elected, all acceptor states reset
+[if[[[global_elected_leader==1])]
+client_does_not_propose_value
+[if!((global_id >= 2)]
+prepare_channel[0].1.2.PASS -------------------------------------------------- sends prepare message with value 2
+prepare_channel[1].1.2.PASS
+prepare_channel[2].1.2.PASS
+[if!((prepare_reads < quorums])]
+[if([prepare_reads >= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if!(((acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)
+[if!(((acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL)
+[ii![[[acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL)
+promise_channel[0].2.-1.PASS
+promise_channel[1].2.-1.PASS
+promise_channel[2].2.-1.PASS
+[if!(promise_received < quorums])]
+[if((promise_received >= quorums])]
+reset_promise_count
+[if![global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+recover
+reset[0].0.FAIL
+reset[1].0.FAIL
+reset[2].0.FAIL
+start
+[if[[global_elected_leader == 0])]
+client_does_not_propose_value
+[if[[(global_id >= 1 )]
+[if!((global_id >=2)]]
+prepare_channel[0].0.2.PASS -------------------------------------------------- proposer 0 sends a prepare message with value 2
+prepare_channel[1].0.2.PASS
+prepare_channel[2].0.2.PASS
+[if!(prepare_reads < quorums])]
+[if((prepare_reads >=quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[ii![[[acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)
+[if!(((acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL)
+[ii![[[acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL)
+promise_channel[0].2.-1.NACK ------------------------------------------------- promise received is a NACK, indicating that a previous id of higher or equal value has been promised
+promise_channel[1].2.-1.NACK
+promise_channel[2].2.-1.NACK
+[if!(promise_received < quorums])]
+[if((promise_received >= quorums])]
+reset_promise_count
+[if[global_terminate]]
+reset[0].0.FAIL
+reset[1].0.FAIL
+reset[2].0.FAIL
+[if[[global_id >=2)]]
+[if![[global_id>=3])]
+prepare_channel[0].0.3.PASS -------------------------------------------------- proposer 0 sends a prepare message with value 3
+prepare_channel[1].0.3.PASS
+prepare_channel[2].0.3.PASS
+[if![[prepare_reads < quorums])]
+[if([prepare_reads >= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[i!![[[[acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL
+[if![[[[acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL
+[I!![[[[acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL)
+promise_channel[0].3.-1.PASS
+promise_channel[1].3.-1.PASS
+promise_channel[2].3.-1.PASS
+[if!(promise_received < quorums])]
+[if(promise_received >= quorums])]
+reset_promise_count
+[if![global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if[[global_accepted_value == -(1))] ----------------------------------------- there will be two option, select the first one
+proposer_did_not_fail_when_sending_accept ------------------------------------ if proposer did not fail when sending the accept messages, we need to let the model know
+accept_channel[0].PASS,2.123.PASS
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.-1.NACK
+accept_channel[1].PASS,2.123.PASS
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.-1.NACK
+accept_channel[2].PASS.2.123.PASS
+accepted_channel_learner[1].-1.NACK
+[if[[client_consensus == -[1])]
+accepted_channel_learner[0].-1.NACK
+[if[[client_consensus == -{1])]
+accepted_channel_proposer.-1.NACK
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if! global_terminate]]
+[if[retry]]
+reset[0].1.FAIL
+reset[1].1.FAIL
+reset[2].1.FAIL
+[if[[global_id>=2)]]
+[if!((global_id >= 4)]
+prepare_channel[0].1.4.PASS
+prepare_channel[1].1.4.PASS
+prepare_channel[2].1.4.PASS
+[if![[prepare_reads < quorums])]
+[if([prepare_reads >= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[i!!(((acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)
+[i!![[[acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL]
+[i!!(((acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL)
+promise_channel[0].4.-1.PASS
+promise_channel[1].4.-1.PASS
+promise_channel[2].4.-1.PASS
+[if!((promise_received < quorums])]
+[if([promise_received >= quorums])]
+reset_promise_count
+[if! (global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if[[global_accepted_value == -(1)])]
+proposer_did_not_fail_when_sending_accept ------------------------------------ if proposer did not fail when sending the accept messages, we need to let the model know
+accept_channel[0].PASS,3.123.PASS -------------------------------------------- proposer 0 sends accept with value 3 but receives NACK
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.-1.NACK -------------------------------------------- there will be two on screen, please make sure to click the second one
+accept_channel[1].PASS.3.123.PASS
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.-1.NACK -------------------------------------------- there will be two on screen, please make sure to click the second one
+accept_channel[2].PASS.3.123.PASS 
+accepted_channel_learner[1].-1.NACK
+accepted_channel_learner[0].-1.NACK
+[if[[client_consensus == -(1)])]
+[if[[client_consensus == -(1)])]
+accepted_channel_proposer.-1.NACK --------------------------------------------- and so on ....
+
+// Scenario 5 - multiple Proposers conflict
+init
+start
+[if((global_elected_leader == 0])]  ------------------------------------------ checks if proposer is elected
+client_proposer.123 ---------------------------------------------------------- client proposed value 123
+[if![(global_id >=1]]
+prepare_channel[0].0.1.PASS -------------------------------------------------- proposer 0 send over prepare message with value 1 
+prepare_channel[1].0.1.PASS
+prepare_channel[2].0.1.PASS
+[if!((prepare_reads < quorums])]
+[if(prepare_reads >= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if!(((acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)
+[if![[[(acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL
+[if!(((acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL]
+promise_channel[0].1.-1.PASS ------------------------------------------------- acceptors send over promise message with value 1
+promise_channel[1].1.-1.PASS
+promise_channel[2].1.-1.PASS
+[if!(promise_received < quorums])]
+[if((promise_received >= quorums])]
+reset_promise_count
+[if!global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if[[global_accepted_value == -(1))]
+accept_channel[0].PASS.1.123.PASS -------------------------------------------- acceptor accepts the first value 
+proposer_fails --------------------------------------------------------------- proposer fails, all subsequent accept messages will fail as well (and accepted messages will NACK)
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer.123.PASS
+accept_channel[1].FAIL.1.123.PASS
+accept_channel[2].FAIL.1.123.PASS  ------------------------------------------- accept message failed
+accepted_channel_learner[0].1.NACK
+accepted_channel_learner[1].1.NACK
+accepted_channel_proposer.-1.NACK
+accepted_channel_learner[0].1.NACK
+[if![[client_consensus == -(1)])
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+accepted_channel_learner[1].-1.NACK
+[if![(client_consensus == -{1)])
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+accepted_channel_proposer.-1.NACK
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if[global_terminate]]
+[if((0 == 0)]
+reset[0].1.FAIL
+reset[1].1.FAIL
+reset[2].1.FAIL
+elect_new_leader ------------------------------------------------------------- new leader elected, all acceptor states reset
+propose_new_value
+start
+[if[[global_elected_leader ==1])]
+client_proposer 124
+[if!((global_id>=2)]]
+prepare_channel[0].1.2.FAIL -------------------------------------------------- prepare message did not reach acceptor 0
+prepare_channel[1].1.2.PASS
+prepare_channel[2].1.2.PASS
+[if![[prepare_reads < quorums)]
+[if((prepare_reads >= quorums)]]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if{{{{acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)
+[if![[[[acceptor_prepare_status[1] == FAIL) | (acceptor_status[1] == FAIL)
+[if![[[[acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL
+promise_channel[0].1.123.INACTIVE  ------------------------------------------- promise here is inactive since prepare was not received
+promise_channel[1].2.-1.PASS
+promise_channel[2].2.-1.PASS
+[if![promise_received < quorums])]
+[if((promise_received >= quorums)]]
+reset_promise_count
+[if![global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if[[global_accepted_value == -(1))]
+accept_channel[0].PASS,2.124.PASS -------------------------------------------- acceptor accepts the second value 
+accepted_channel_learner[1].124.PASS
+accepted_channel_learner[0].124.PASS
+accept_channel[1].PASS,2.124.PASS
+accepted_channel_learner[0].124.PASS
+accepted_channel_learner[1].124.PASS
+accepted_channel_proposer.124.PASS
+accepted_channel_proposer.124.PASS
+accept_channel[2].PASS.2.124.PASS
+accepted_channel_learner[0].124.PASS
+accepted_channel_learner[1].124.PASS
+[if![[client_consensus == -[1])]
+learner_client.0.124 --------------------------------------------------------- final read value is 124 (V2) 
+[if![(client_consensus == -(1))]
+learner_client.1.124
+finish
+proposer_did_not_fail_when_sending_accept ------------------------------------ if proposer did not fail when sending the accept messages, we need to let the model know
+accepted_channel_proposer.124.PASS
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if![global_terminate]]
+[if![retry]]
+
+// Scenario 6 Trace -  multi-identifier majority is insufficient
+init
+start
+[if((global_elected_leader == 0])]  ------------------------------------------ checks if proposer is elected
+client_proposer.123 ---------------------------------------------------------- client proposed value 123
+[if![(global_id >=1]]
+prepare_channel[0].0.1.PASS -------------------------------------------------- proposer 0 send over prepare message with value 1 
+prepare_channel[1].0.1.PASS
+prepare_channel[2].0.1.PASS
+prepare_channel[3].0.1.PASS
+prepare_channel[4].0.1.PASS
+[if!((prepare_reads < quorums)]
+[if[[prepare_reads >= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if![[[(acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL
+[if!(((acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL)
+[if![[[(acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL
+[if![[[[acceptor_prepare_status[3] == FAIL) || (acceptor_status[3] == FAIL
+[if![[[(acceptor_prepare_status[4] == FAIL) || (acceptor_status[4] == FAIL
+promise_channel[0].1.-1.PASS ------------------------------------------------- acceptors send over promise message with value 1
+promise_channel[1].1.-1.PASS
+promise_channel[2].1.-1.PASS
+promise_channel[3].1.-1.PASS
+promise_channel[4].1.-1.PASS
+[if!(promise_received < quorums)]]
+[if(promise_received >= quorums])]
+reset_promise_count
+[if!global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if[[global_accepted_value == -(1)])]
+accept_channel[0].PASS.1.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer 123.PASS
+proposer_fails --------------------------------------------------------------- proposer fails, all subsequent accept messages will fail as well (and accepted messages will NACK)
+accept_channel[1].FAIL.1.123.PASS
+accept_channel[2].FAIL.1.123.PASS  ------------------------------------------- accept message failed
+accept_channel[3].FAIL.1.123.PASS
+accept_channel[4].FAIL.1.123.PASS
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.-1.NACK
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.-1.NACK
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.-1.NACK
+accepted_channel_learner[0].-1.NACK
+[if![[client_consensus == -(1))]
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+accepted_channel_learner[1].-1.NACK
+[if![[client_consensus == -(1))]
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+accepted_channel_proposer.-1.NACK
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if[global_terminate]]
+[if((0== 0)]
+reset[0].1.FAIL
+reset[1].1.FAIL
+reset[2].1.FAIL
+reset[3].1.FAIL
+reset[4].1.FAIL
+elect_new_leader ------------------------------------------------------------- new leader elected, all acceptor states reset
+propose_new_value
+[if[[global_elected_leader==1])]
+client_proposer.124
+[if!((global_id>=2)]]
+prepare_channel[0].1.2.FAIL -------------------------------------------------- prepare message did not reach acceptor 0
+prepare_channel[1].1.2.PASS -------------------------------------------------- proposer 1 sends a prepare message with value 2
+prepare_channel[2].1.2.PASS
+prepare_channel[3].1.2.PASS
+prepare_channel[4].1.2.PASS
+[if!((prepare_reads < quorums])]
+[if[[prepare_reads >= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if[[[[acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)
+[if!(((acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL)
+[i!![[[(acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL
+[i!![[[acceptor_prepare_status[3] == FAIL) || (acceptor_status[3] == FAIL)
+[i!![[[[acceptor_prepare_status[4] == FAIL) || (acceptor_status[4] == FAIL
+promise_channel[0].1.123.INACTIVE  ------------------------------------------- promise here is inactive since prepare was not received
+promise_channel[1].2.-1.PASS
+promise_channel[2].2.-1.PASS
+promise_channel[3].2.-1.PASS
+promise_channel[4].2.-1.PASS
+[if!((promise_received < quorums])]
+[if((promise_received >= quorums])]
+reset_promise_count
+[if![global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if[[global_accepted_value == -(1)])]
+accept_channel[1].PASS,2.124.PASS
+accepted_channel_learner[0].124.PASS
+accepted_channel_learner[1].124.PASS
+accepted_channel_proposer 124.PASS
+proposer_fails --------------------------------------------------------------- proposer fails, all subsequent accept messages will fail as well (and accepted messages will NACK)
+accept_channel[0].FAIL.2.124.PASS
+accepted_channel_learner[0].123.NACK
+accepted_channel_learner[1].123.NACK
+accept_channel[2].FAIL.2.124.PASS
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accepted_channel_proposer.123.NACK
+accepted_channel_proposer.-1.NACK
+accept_channel[4].FAIL.2.124.PASS
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+accept_channel[3].FAIL.2.124.PASS
+accepted_channel_learner[0].-1.NACK
+accepted_channel_learner[1].-1.NACK
+[if![[client_consensus == -{1])]
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+[if![[client_consensus == -{1])]
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+accepted_channel_proposer.-1.NACK
+accepted_channel_proposer.-1.NACK
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if[global_terminate]]
+[if!(1 == 0)]
+[if!(1 == (PROPOSERS - 1])]
+[if(((0<1) & (1<(PROPOSERS - 1])]
+reset[0].2.FAIL
+reset[1].2.FAIL
+reset[2].2.FAIL
+reset[3].2.FAIL
+reset[4].2.FAIL
+elect_new_leader ------------------------------------------------------------- new leader elected, all acceptor states reset
+start
+[if[[global_elected_leader == 2])]
+client_does_not_propose_value
+[if![[global_id>=3)]]
+prepare_channel[0].2.3.PASS -------------------------------------------------- proposer 2 sends a prepare message with value 3
+prepare_channel[1].2.3.FAIL
+prepare_channel[2].2.3.PASS
+prepare_channel[3].2.3.PASS
+prepare_channel[4].2.3.PASS
+[if!((prepare_reads < quorums])]
+[if((prepare_reads>= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if![[[(acceptor_prepare_status[0] == FAIL) ll (acceptor_status[0] == FAIL
+[if![[[(acceptor_prepare_status[1] == FAIL) ll (acceptor_status[1] == FAIL)
+[if![[[(acceptor_prepare_status[2] == FAIL) ll (acceptor_status[2] == FAIL
+[if![[((acceptor_prepare_status[3] == FAIL) ll (acceptor_status[3] == FAIL
+[if![[[(acceptor_prepare_status[4] == FAIL) ll (acceptor_status[4] == FAIL
+promise_channel[0].3.123.PASS
+promise_channel[1].2.124.INACTIVE
+promise_channel[2].3.-1.PASS
+promise_channel[3].3.-1.PASS
+promise_channel[4].3.-1.PASS
+[if!(promise_received < quorums])]
+[if((promise_received >= quorums])]
+reset_promise_count
+[if![global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if![[[global_accepted_value = -(1)])]
+accept_channel[2].PASS,3.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer 123.PASS
+accept_channel[3].PASS.3.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer.123.PASS
+proposer_fails --------------------------------------------------------------- proposer fails, all subsequent accept messages will fail as well (and accepted messages will NACK)
+accept_channel[0].FAIL.3.123.PASS
+accepted_channel_learner[0].123.NACK
+accepted_channel_learner[1].123.NACK
+accepted_channel_proposer.123.NACK
+accept_channel[1].FAIL.3.123.PASS
+accepted_channel_learner[0].124.NACK
+accepted_channel_learner[1].124.NACK
+accepted_channel_proposer 124.NACK
+accept_channel[4].FAIL.3.123.PASS
+accepted_channel_learner[1].-1.NACK
+accepted_channel_learner[0].-1.NACK
+[if![[client_consensus == -(1)])
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+[if![(client_consensus == -(1)])
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+accepted_channel_proposer.-1.NACK
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if[global_terminate]]
+[if!((2==0)]]
+[if!((2 == (PROPOSERS - 1])]
+[if(((0<2) & (2< (PROPOSERS - 1])]
+reset[0].3.FAIL
+reset[1].3.FAIL
+reset[2].3.FAIL
+reset[3].3.FAIL
+reset[4].3.FAIL
+elect_new_leader ------------------------------------------------------------- new leader elected, all acceptor states reset
+start
+[if[[global_elected_leader == 3])]
+client_does_not_propose_value
+[if![[global_id>= 4)]]
+prepare_channel[0].3.4.PASS -------------------------------------------------- proposer 3 sends a prepare message with value 4
+prepare_channel[1].3.4.PASS
+prepare_channel[2].3.4.FAIL
+prepare_channel[3].3.4.FAIL
+prepare_channel[4].3.4.PASS
+[if!((prepare_reads < quorums)]
+[if[[prepare_reads >= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[i!![[[acceptor_prepare_status[0] == FAIL) II (acceptor_status[0] == FAIL)
+[i!![[[acceptor_prepare_status[1] == FAIL) II (acceptor_status[1] == FAIL)
+[if[[[[acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL)
+[if[[[[acceptor_prepare_status[3] == FAIL) || (acceptor_status[3] == FAIL)
+[i!![[[[acceptor_prepare_status[4] == FAIL) || (acceptor_status[4] == FAIL
+promise_channel[0].4.123.PASS
+promise_channel[1].4.124.PASS
+promise_channel[2].3.123.INACTIVE
+promise_channel[3].3.123.INACTIVE
+promise_channel[4].4.-1.PASS
+[if![[promise_received < quorums])]
+[if((promise_received >= quorums])]
+reset_promise_count
+[if![global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if![[global accepted_value == -(1)])]
+proposer_did_not_fail_when_sending_accept ------------------------------------ if proposer did not fail when sending the accept messages, we need to let the model know
+accept_channel[0].PASS.4.124.PASS
+accepted_channel_learner[0].124.PASS
+accepted_channel_learner[1].124.PASS
+accepted_channel_proposer.124.PASS
+accept_channel[1].PASS,4124.PASS
+accepted_channel_learner[0].124.PASS
+accepted_channel_learner[1].124.PASS
+accepted_channel_proposer.124.PASS
+accept_channel[2].PASS,4,124.PASS
+accepted_channel_learner[0].124.PASS
+accepted_channel_learner[1].124.PASS
+accepted_channel_proposer 124.PASS
+accept_channel[3].PASS,4.124.PASS
+accepted_channel_learner[0].124.PASS
+accepted_channel_learner[1].124.PASS
+accepted_channel_proposer 124.PASS
+accept_channel[4].PASS.4.124.PASS
+accepted_channel_learner[1].124.PASS
+accepted_channel_learner[0].124.PASS
+[if![[client_consensus == -(1)])]
+learner_client.0.124 --------------------------------------------------------- V2 is the final read value 
+[if![[client_consensus == -(1)])]
+learner_client.1.124
+finish
+accepted_channel_proposer 124.PASS
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if![global_terminate]]
+[if![retry]]
+
+// Scenario 7 Trace - existing consensus
+init
+start
+[if((global_elected_leader == 0])]  ------------------------------------------ checks if proposer is elected
+client_proposer.123 ---------------------------------------------------------- client proposed value 123
+[if![(global_id >=1]]
+prepare_channel[0].0.1.PASS -------------------------------------------------- proposer 0 send over prepare message with value 1 
+prepare_channel[1].0.1.PASS
+prepare_channel[2].0.1.PASS
+[if!((prepare_reads < quorums])]
+[if(prepare_reads >= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if![[[(acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL
+[if![[[(acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL
+[if![[[[[acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAI
+promise_channel[0].1.-1.PASS ------------------------------------------------- acceptors send over promise message with value 1
+promise_channel[1].1.-1.PASS
+promise_channel[2].1.-1.PASS
+[if!(promise_received < quorums])]
+[if((promise_received >= quorums])]
+reset_promise_count
+[if![global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if([global_accepted_value == -(1))]
+accept_channel[0].PASS.1.123.PASS
+accept_channel[1].PASS.1.123.PASS
+proposer_fails --------------------------------------------------------------- proposer fails, all subsequent accept messages will fail as well (and accepted messages will NACK)
+accept_channel[2].FAIL.1.123.PASS  ------------------------------------------- accept message failed
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer 123.PASS
+accepted_channel_learner[0].-1.NACK
+[if![(client_consensus == -(1)])]
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+accepted_channel_learner[1].-1.NACK
+[if!((client_consensus == -(1)])]
+reset_learner ---------------------------------------------------------------- reset learner so that it can receives the next message
+accepted_channel_proposer.-1.NACK
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if[global_terminate]]
+[if((0== 0])]
+reset[1].1.FAIL
+reset[0].1.FAIL
+reset[2].1.FAIL
+elect_new_leader ------------------------------------------------------------- new leader elected, all acceptor states reset
+start
+[if[[global_elected_leader == 1 )]
+client_does_not_propose_value
+[if!((global_id >= 2)]
+prepare_channel[0].1.2.FAIL -------------------------------------------------- prepare message did not reach acceptor 0
+prepare_channel[1].1.2.PASS
+prepare_channel[2].1.2.PASS
+[if!((prepare_reads < quorums])]
+[if((prepare_reads >= quorums])]
+prepare_ends ----------------------------------------------------------------- prepare phase ends
+[if[[[acceptor_prepare_status[0] == FAIL) || (acceptor_status[0] == FAIL)]
+[if![[[(acceptor_prepare_status[1] == FAIL) || (acceptor_status[1] == FAIL
+[i!![[[[acceptor_prepare_status[2] == FAIL) || (acceptor_status[2] == FAIL
+promise_channel[0].1.123.INACTIVE  ------------------------------------------- promise here is inactive since prepare was not received
+promise_channel[1].2.123.PASS
+promise_channel[2].2.-1.PASS
+[if!(promise_received < quorums])]
+[if((promise_received >= quorums])]
+reset_promise_count
+[if![global_terminate]]
+promise_phase_ends ----------------------------------------------------------- promise phase ends
+[if![[global_accepted_value == (1))]
+proposer_did_not_fail_when_sending_accept ------------------------------------ if proposer did not fail when sending the accept messages, we need to let the model know
+accept_channel[0].PASS.2.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+accepted_channel_proposer.123.PASS
+accept_channel[1].PASS.2.123.PASS
+accepted_channel_learner[1].123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_proposer.123.PASS
+accept_channel[2].PASS,2.123.PASS
+accepted_channel_learner[0].123.PASS ----------------------------------------- acceptor broadcast accepted message to learner 1, learner 2 and proposer
+accepted_channel_learner[1].123.PASS
+[if![[client_consensus == -(1)])]
+learner_client.1.123 --------------------------------------------------------- V1 value is read
+[if![[client_consensus == -(1)])]
+learner_client.1.123 --------------------------------------------------------- learner received all the accepted messages and sends it to client
+finish
+accepted_channel_proposer.123.PASS
+end_of_broadcast ------------------------------------------------------------- acceptors finish broadcasting
+[if![global_terminate]]
+[if![retry)]