Group 1:
Agent Voter1:
init: q0
LOCAL: [Voter1_vote, Voter1_reported, Voter1_pun]
INTERFACE: [Coercer_pun_1]
vote1: q0 -> q1 [Voter1_vote=1]
vote2: q0 -> q1 [Voter1_vote=2]
give: q1 -> q2 [Voter1_reported=?Voter1_vote]
ngive: q1 -> q2 [Voter1_reported=-1]
pun: q2 -[Coercer_pun_1 == 1]> q3 [Voter1_pun=1]
npun: q2 -[Coercer_pun_1 == -1]> q3 [Voter1_pun=-1]
loop: q3->q3

FORMULA: <<Voter1>>F(Voter1_vote=1 | Voter1_pun=-1)

Group 2:
Agent Voter2:
init: q0
LOCAL: [Voter2_vote, Voter2_reported, Voter2_pun]
INTERFACE: [Coercer_pun_2]
vote1: q0 -> q1 [Voter2_vote=1]
vote2: q0 -> q1 [Voter2_vote=2]
give: q1 -> q2 [Voter2_reported=?aID_vote]
ngive: q1 -> q2 [Voter2_reported=-1]
pun: q2 -[Coercer_pun_2 == 1]> q3 [Voter2_pun=1]
npun: q2 -[Coercer_pun_2 == -1]> q3 [Voter2_pun=-1]
loop: q3->q3

Agent Coercer:
init: q0
LOCAL: [Coercer_pun_1, Coercer_pun_2]
INTERFACE: [Voter1_reported, Voter2_reported]
pun_Voter1: q0 -[Voter1_reported != 0 and Coercer_pun_1 == 0]> q0 [Coercer_pun_1=1]
npun_Voter1: q0 -[Voter1_reported != 0 and Coercer_pun_1 == 0]> q0 [Coercer_pun_1=-1]
pun_Voter2: q0 -[Voter2_reported != 0 and Coercer_pun_2 == 0]> q0 [Coercer_pun_2=1]
npun_Voter2: q0 -[Voter2_reported != 0 and Coercer_pun_2 == 0]> q0 [Coercer_pun_2=-1]

PERSISTENT: [Voter1_vote, Voter1_reported, Voter1_pun, Coercer_pun_1, Voter2_vote, Voter2_reported, Voter2_pun, Coercer_pun_2]
INITIAL: [Voter1_vote=0, Voter1_reported=0, Voter1_pun=0, Coercer_pun_1=0, Voter2_vote=0, Voter2_reported=0, Voter2_pun=0, Coercer_pun_2=0]
SHOW_EPISTEMIC: False