Agent Voter1:
LOCAL: [Voter1_vote]
PERSISTENT: [Voter1_vote]
INITIAL: []
init q0
vote1: q0 -> q1 [Voter1_vote:=1]
shared[2] gv_1_Voter1[gv_1_Voter1]: q1 [Voter1_vote==1] -> q2
vote2: q0 -> q1 [Voter1_vote:=2]
shared[2] gv_2_Voter1[gv_2_Voter1]: q1 [Voter1_vote==2] -> q2
vote3: q0 -> q1 [Voter1_vote:=3]
shared[2] gv_3_Voter1[gv_3_Voter1]: q1 [Voter1_vote==3] -> q2
shared[2] ng_Voter1[ng_Voter1]: q1 -> q2
shared[2] pun_Voter1[pn_Voter1]: q2 -> q3
shared[2] npun_Voter1[pn_Voter1]: q2 -> q3
idle: q3->q3

Agent Voter2:
LOCAL: [Voter2_vote]
PERSISTENT: [Voter2_vote]
INITIAL: []
init q0
vote1: q0 -> q1 [Voter2_vote:=1]
shared[2] gv_1_Voter2[gv_1_Voter2]: q1 [Voter2_vote==1] -> q2
vote2: q0 -> q1 [Voter2_vote:=2]
shared[2] gv_2_Voter2[gv_2_Voter2]: q1 [Voter2_vote==2] -> q2
vote3: q0 -> q1 [Voter2_vote:=3]
shared[2] gv_3_Voter2[gv_3_Voter2]: q1 [Voter2_vote==3] -> q2
shared[2] ng_Voter2[ng_Voter2]: q1 -> q2
shared[2] pun_Voter2[pn_Voter2]: q2 -> q3
shared[2] npun_Voter2[pn_Voter2]: q2 -> q3
idle: q3->q3

Agent Coercer1:
LOCAL: [Coercer1_Voter1_vote, Coercer1_Voter1_gv, Coercer1_pun1, Coercer1_npun1,Coercer1_Voter2_vote, Coercer1_Voter2_gv, Coercer1_pun2, Coercer1_npun2, Coercer1_Voter1_finish]
PERSISTENT: [Coercer1_Voter1_vote, Coercer1_Voter1_gv, Coercer1_pun1, Coercer1_npun1,Coercer1_Voter2_vote, Coercer1_Voter2_gv, Coercer1_pun2, Coercer1_npun2, Coercer1_Voter1_finish]
INITIAL: []
init q0
shared[2] gv_1_Voter1[g_Voter1]: q0 -> q1 [Coercer1_Voter1_vote:=1, Coercer1_Voter1_gv:=1]    
shared[2] gv_2_Voter1[g_Voter1]: q0 -> q1 [Coercer1_Voter1_vote:=2, Coercer1_Voter1_gv:=1]    
shared[2] gv_3_Voter1[g_Voter1]: q0 -> q1 [Coercer1_Voter1_vote:=3, Coercer1_Voter1_gv:=1]    
shared[2] ng_Voter1[g_Voter1]: q0 -> q1 [Coercer1_Voter1_gv:=2]
shared[2] pun_Voter1[pun_Voter1]: q2 -> q3 [Coercer1_pun1:=1, Coercer1_Voter1_finish:=1]
shared[2] npun_Voter1[npun_Voter1]: q2 -> q3 [Coercer1_npun1:=1, Coercer1_Voter1_finish:=1]
shared[2] gv_1_Voter2[g_Voter2]: q1 -> q2 [Coercer1_Voter2_vote:=1, Coercer1_Voter2_gv:=1]    
shared[2] gv_2_Voter2[g_Voter2]: q1 -> q2 [Coercer1_Voter2_vote:=2, Coercer1_Voter2_gv:=1]    
shared[2] gv_3_Voter2[g_Voter2]: q1 -> q2 [Coercer1_Voter2_vote:=3, Coercer1_Voter2_gv:=1]    
shared[2] ng_Voter2[g_Voter2]: q1 -> q2 [Coercer1_Voter2_gv:=2]
shared[2] pun_Voter2[pun_Voter2]: q3 -> q4 [Coercer1_pun2:=1]
shared[2] npun_Voter2[npun_Voter2]: q3 -> q4 [Coercer1_npun2:=1]

FORMULA: <<Coercer1>>[](Coercer1_Voter1_finish==0 || (Voter1_vote==1 && &K_Coercer1(Voter1_vote==1)) )