traces.txt

// 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)]