MODULE main DEFINE NumProcess := 5; TRANS (_trans=1 & ((((next(messages[4])=messages[0]))&((next(leader_PROCESS_PROCESS_PROCESS_PROCESS)=messages[0])))))|(_trans=2 & ((((next(messages[3])=messages[4]))&((next(leader_PROCESS_PROCESS_PROCESS_PROCESS)=messages[4])))))|(_trans=3 & ((((next(messages[2])=messages[3]))&((next(leader_PROCESS_PROCESS_PROCESS_PROCESS)=messages[3])))))|(_trans=4 & ((((next(messages[1])=messages[2]))&((next(leader_PROCESS_PROCESS_PROCESS_PROCESS)=messages[2])))))|(_trans=5 & ((((next(messages[0])=messages[1]))&((next(leader_PROCESS_PROCESS_PROCESS_PROCESS)=messages[1])))))|(_trans=6)|(_trans=7)|(_trans=8)|(_trans=9)|(_trans=10)|(_trans=11 & ((((next(leader_PROCESS_PROCESS_PROCESS_PROCESS)=processes[0]))&((next(messages[4])=processes[0])))))|(_trans=12 & ((((next(leader_PROCESS_PROCESS_PROCESS_PROCESS)=processes[4]))&((next(messages[3])=processes[4])))))|(_trans=13 & ((((next(leader_PROCESS_PROCESS_PROCESS_PROCESS)=processes[3]))&((next(messages[2])=processes[3])))))|(_trans=14 & ((((next(leader_PROCESS_PROCESS_PROCESS_PROCESS)=processes[2]))&((next(messages[1])=processes[2])))))|(_trans=15 & ((((next(leader_PROCESS_PROCESS_PROCESS_PROCESS)=processes[1]))&((next(messages[0])=processes[1])))))|(_trans=16 & ((next(messages[4])=processes[0])))|(_trans=17 & ((next(messages[3])=processes[4])))|(_trans=18 & ((next(messages[2])=processes[3])))|(_trans=19 & ((next(messages[1])=processes[2])))|(_trans=20 & ((next(messages[0])=processes[1])))|(_trans=21 & ((next(messages[4])=messages[0])))|(_trans=22 & ((next(messages[3])=messages[4])))|(_trans=23 & ((next(messages[2])=messages[3])))|(_trans=24 & ((next(messages[1])=messages[2])))|(_trans=25 & ((next(messages[0])=messages[1])))|(_trans=26 & ((((next(messages[4])=messages[0]))&((next(leader_PROCESS_PROCESS_PROCESS)=messages[0])))))|(_trans=27 & ((((next(messages[3])=messages[4]))&((next(leader_PROCESS_PROCESS_PROCESS)=messages[4])))))|(_trans=28 & ((((next(messages[2])=messages[3]))&((next(leader_PROCESS_PROCESS_PROCESS)=messages[3])))))|(_trans=29 & ((((next(messages[1])=messages[2]))&((next(leader_PROCESS_PROCESS_PROCESS)=messages[2])))))|(_trans=30 & ((((next(messages[0])=messages[1]))&((next(leader_PROCESS_PROCESS_PROCESS)=messages[1])))))|(_trans=31)|(_trans=32)|(_trans=33)|(_trans=34)|(_trans=35)|(_trans=36 & ((((next(leader_PROCESS_PROCESS_PROCESS)=processes[0]))&((next(messages[4])=processes[0])))))|(_trans=37 & ((((next(leader_PROCESS_PROCESS_PROCESS)=processes[4]))&((next(messages[3])=processes[4])))))|(_trans=38 & ((((next(leader_PROCESS_PROCESS_PROCESS)=processes[3]))&((next(messages[2])=processes[3])))))|(_trans=39 & ((((next(leader_PROCESS_PROCESS_PROCESS)=processes[2]))&((next(messages[1])=processes[2])))))|(_trans=40 & ((((next(leader_PROCESS_PROCESS_PROCESS)=processes[1]))&((next(messages[0])=processes[1])))))|(_trans=41 & ((next(messages[4])=processes[0])))|(_trans=42 & ((next(messages[3])=processes[4])))|(_trans=43 & ((next(messages[2])=processes[3])))|(_trans=44 & ((next(messages[1])=processes[2])))|(_trans=45 & ((next(messages[0])=processes[1])))|(_trans=46 & ((next(messages[4])=messages[0])))|(_trans=47 & ((next(messages[3])=messages[4])))|(_trans=48 & ((next(messages[2])=messages[3])))|(_trans=49 & ((next(messages[1])=messages[2])))|(_trans=50 & ((next(messages[0])=messages[1])))|(_trans=51 & ((((next(messages[4])=messages[0]))&((next(leader_PROCESS_PROCESS)=messages[0])))))|(_trans=52 & ((((next(messages[3])=messages[4]))&((next(leader_PROCESS_PROCESS)=messages[4])))))|(_trans=53 & ((((next(messages[2])=messages[3]))&((next(leader_PROCESS_PROCESS)=messages[3])))))|(_trans=54 & ((((next(messages[1])=messages[2]))&((next(leader_PROCESS_PROCESS)=messages[2])))))|(_trans=55 & ((((next(messages[0])=messages[1]))&((next(leader_PROCESS_PROCESS)=messages[1])))))|(_trans=56)|(_trans=57)|(_trans=58)|(_trans=59)|(_trans=60)|(_trans=61 & ((((next(leader_PROCESS_PROCESS)=processes[0]))&((next(messages[4])=processes[0])))))|(_trans=62 & ((((next(leader_PROCESS_PROCESS)=processes[4]))&((next(messages[3])=processes[4])))))|(_trans=63 & ((((next(leader_PROCESS_PROCESS)=processes[3]))&((next(messages[2])=processes[3])))))|(_trans=64 & ((((next(leader_PROCESS_PROCESS)=processes[2]))&((next(messages[1])=processes[2])))))|(_trans=65 & ((((next(leader_PROCESS_PROCESS)=processes[1]))&((next(messages[0])=processes[1])))))|(_trans=66 & ((next(messages[4])=processes[0])))|(_trans=67 & ((next(messages[3])=processes[4])))|(_trans=68 & ((next(messages[2])=processes[3])))|(_trans=69 & ((next(messages[1])=processes[2])))|(_trans=70 & ((next(messages[0])=processes[1])))|(_trans=71 & ((next(messages[4])=messages[0])))|(_trans=72 & ((next(messages[3])=messages[4])))|(_trans=73 & ((next(messages[2])=messages[3])))|(_trans=74 & ((next(messages[1])=messages[2])))|(_trans=75 & ((next(messages[0])=messages[1])))|(_trans=76 & ((((next(messages[4])=messages[0]))&((next(leader_PROCESS)=messages[0])))))|(_trans=77 & ((((next(messages[3])=messages[4]))&((next(leader_PROCESS)=messages[4])))))|(_trans=78 & ((((next(messages[2])=messages[3]))&((next(leader_PROCESS)=messages[3])))))|(_trans=79 & ((((next(messages[1])=messages[2]))&((next(leader_PROCESS)=messages[2])))))|(_trans=80 & ((((next(messages[0])=messages[1]))&((next(leader_PROCESS)=messages[1])))))|(_trans=81)|(_trans=82)|(_trans=83)|(_trans=84)|(_trans=85)|(_trans=86 & ((((next(leader_PROCESS)=processes[0]))&((next(messages[4])=processes[0])))))|(_trans=87 & ((((next(leader_PROCESS)=processes[4]))&((next(messages[3])=processes[4])))))|(_trans=88 & ((((next(leader_PROCESS)=processes[3]))&((next(messages[2])=processes[3])))))|(_trans=89 & ((((next(leader_PROCESS)=processes[2]))&((next(messages[1])=processes[2])))))|(_trans=90 & ((((next(leader_PROCESS)=processes[1]))&((next(messages[0])=processes[1])))))|(_trans=91 & ((next(messages[4])=processes[0])))|(_trans=92 & ((next(messages[3])=processes[4])))|(_trans=93 & ((next(messages[2])=processes[3])))|(_trans=94 & ((next(messages[1])=processes[2])))|(_trans=95 & ((next(messages[0])=processes[1])))|(_trans=96 & ((next(messages[4])=messages[0])))|(_trans=97 & ((next(messages[3])=messages[4])))|(_trans=98 & ((next(messages[2])=messages[3])))|(_trans=99 & ((next(messages[1])=messages[2])))|(_trans=100 & ((next(messages[0])=messages[1])))|(_trans=101 & ((((next(messages[4])=messages[0]))&((next(leader)=messages[0])))))|(_trans=102 & ((((next(messages[3])=messages[4]))&((next(leader)=messages[4])))))|(_trans=103 & ((((next(messages[2])=messages[3]))&((next(leader)=messages[3])))))|(_trans=104 & ((((next(messages[1])=messages[2]))&((next(leader)=messages[2])))))|(_trans=105 & ((((next(messages[0])=messages[1]))&((next(leader)=messages[1])))))|(_trans=106)|(_trans=107)|(_trans=108)|(_trans=109)|(_trans=110)|(_trans=111 & ((((next(leader)=processes[0]))&((next(messages[4])=processes[0])))))|(_trans=112 & ((((next(leader)=processes[4]))&((next(messages[3])=processes[4])))))|(_trans=113 & ((((next(leader)=processes[3]))&((next(messages[2])=processes[3])))))|(_trans=114 & ((((next(leader)=processes[2]))&((next(messages[1])=processes[2])))))|(_trans=115 & ((((next(leader)=processes[1]))&((next(messages[0])=processes[1])))))|(_trans=116 & ((next(messages[4])=processes[0])))|(_trans=117 & ((next(messages[3])=processes[4])))|(_trans=118 & ((next(messages[2])=processes[3])))|(_trans=119 & ((next(messages[1])=processes[2])))|(_trans=120 & ((next(messages[0])=processes[1])))|(_trans=121 & ((next(messages[4])=messages[0])))|(_trans=122 & ((next(messages[3])=messages[4])))|(_trans=123 & ((next(messages[2])=messages[3])))|(_trans=124 & ((next(messages[1])=messages[2])))|(_trans=125 & ((next(messages[0])=messages[1])))|(_trans=126 & ((next(messages[4])=processes[0]))) INVAR !_fail VAR _trans : 1..126; _terminate : boolean; _fail : boolean; proc5 : -100..100; proc4 : -100..100; proc3 : -100..100; proc2 : -100..100; proc1 : -100..100; leader_PROCESS_PROCESS_PROCESS_PROCESS : -100..100; leader_PROCESS_PROCESS_PROCESS : -100..100; leader_PROCESS_PROCESS : -100..100; leader_PROCESS : -100..100; leader : -100..100; init : boolean; processes : array 0..4 of -100..100; messages : array 0..4 of -100..100; message_exist : array 0..4 of { no_message,elected,election }; ASSIGN _terminate := case !(((((message_exist[0]=elected))&((processes[0]!=messages[0]))))|(((((message_exist[4]=elected))&((processes[4]!=messages[4]))))|(((((message_exist[3]=elected))&((processes[3]!=messages[3]))))|(((((message_exist[2]=elected))&((processes[2]!=messages[2]))))|(((((message_exist[1]=elected))&((processes[1]!=messages[1]))))|(((((message_exist[0]=elected))&((processes[0]=messages[0]))))|(((((message_exist[4]=elected))&((processes[4]=messages[4]))))|(((((message_exist[3]=elected))&((processes[3]=messages[3]))))|(((((message_exist[2]=elected))&((processes[2]=messages[2]))))|(((((message_exist[1]=elected))&((processes[1]=messages[1]))))|(((((message_exist[0]=election))&((processes[0]=messages[0]))))|(((((message_exist[4]=election))&((processes[4]=messages[4]))))|(((((message_exist[3]=election))&((processes[3]=messages[3]))))|(((((message_exist[2]=election))&((processes[2]=messages[2]))))|(((((message_exist[1]=election))&((processes[1]=messages[1]))))|(((((message_exist[0]=election))&((processes[0]>messages[0]))))|(((((message_exist[4]=election))&((processes[4]>messages[4]))))|(((((message_exist[3]=election))&((processes[3]>messages[3]))))|(((((message_exist[2]=election))&((processes[2]>messages[2]))))|(((((message_exist[1]=election))&((processes[1]>messages[1]))))|(((((message_exist[0]=election))&((messages[0]>processes[0]))))|(((((message_exist[4]=election))&((messages[4]>processes[4]))))|(((((message_exist[3]=election))&((messages[3]>processes[3]))))|(((((message_exist[2]=election))&((messages[2]>processes[2]))))|(((((message_exist[1]=election))&((messages[1]>processes[1]))))|(((((message_exist[0]=elected))&((processes[0]!=messages[0]))))|(((((message_exist[4]=elected))&((processes[4]!=messages[4]))))|(((((message_exist[3]=elected))&((processes[3]!=messages[3]))))|(((((message_exist[2]=elected))&((processes[2]!=messages[2]))))|(((((message_exist[1]=elected))&((processes[1]!=messages[1]))))|(((((message_exist[0]=elected))&((processes[0]=messages[0]))))|(((((message_exist[4]=elected))&((processes[4]=messages[4]))))|(((((message_exist[3]=elected))&((processes[3]=messages[3]))))|(((((message_exist[2]=elected))&((processes[2]=messages[2]))))|(((((message_exist[1]=elected))&((processes[1]=messages[1]))))|(((((message_exist[0]=election))&((processes[0]=messages[0]))))|(((((message_exist[4]=election))&((processes[4]=messages[4]))))|(((((message_exist[3]=election))&((processes[3]=messages[3]))))|(((((message_exist[2]=election))&((processes[2]=messages[2]))))|(((((message_exist[1]=election))&((processes[1]=messages[1]))))|(((((message_exist[0]=election))&((processes[0]>messages[0]))))|(((((message_exist[4]=election))&((processes[4]>messages[4]))))|(((((message_exist[3]=election))&((processes[3]>messages[3]))))|(((((message_exist[2]=election))&((processes[2]>messages[2]))))|(((((message_exist[1]=election))&((processes[1]>messages[1]))))|(((((message_exist[0]=election))&((messages[0]>processes[0]))))|(((((message_exist[4]=election))&((messages[4]>processes[4]))))|(((((message_exist[3]=election))&((messages[3]>processes[3]))))|(((((message_exist[2]=election))&((messages[2]>processes[2]))))|(((((message_exist[1]=election))&((messages[1]>processes[1]))))|(((((message_exist[0]=elected))&((processes[0]!=messages[0]))))|(((((message_exist[4]=elected))&((processes[4]!=messages[4]))))|(((((message_exist[3]=elected))&((processes[3]!=messages[3]))))|(((((message_exist[2]=elected))&((processes[2]!=messages[2]))))|(((((message_exist[1]=elected))&((processes[1]!=messages[1]))))|(((((message_exist[0]=elected))&((processes[0]=messages[0]))))|(((((message_exist[4]=elected))&((processes[4]=messages[4]))))|(((((message_exist[3]=elected))&((processes[3]=messages[3]))))|(((((message_exist[2]=elected))&((processes[2]=messages[2]))))|(((((message_exist[1]=elected))&((processes[1]=messages[1]))))|(((((message_exist[0]=election))&((processes[0]=messages[0]))))|(((((message_exist[4]=election))&((processes[4]=messages[4]))))|(((((message_exist[3]=election))&((processes[3]=messages[3]))))|(((((message_exist[2]=election))&((processes[2]=messages[2]))))|(((((message_exist[1]=election))&((processes[1]=messages[1]))))|(((((message_exist[0]=election))&((processes[0]>messages[0]))))|(((((message_exist[4]=election))&((processes[4]>messages[4]))))|(((((message_exist[3]=election))&((processes[3]>messages[3]))))|(((((message_exist[2]=election))&((processes[2]>messages[2]))))|(((((message_exist[1]=election))&((processes[1]>messages[1]))))|(((((message_exist[0]=election))&((messages[0]>processes[0]))))|(((((message_exist[4]=election))&((messages[4]>processes[4]))))|(((((message_exist[3]=election))&((messages[3]>processes[3]))))|(((((message_exist[2]=election))&((messages[2]>processes[2]))))|(((((message_exist[1]=election))&((messages[1]>processes[1]))))|(((((message_exist[0]=elected))&((processes[0]!=messages[0]))))|(((((message_exist[4]=elected))&((processes[4]!=messages[4]))))|(((((message_exist[3]=elected))&((processes[3]!=messages[3]))))|(((((message_exist[2]=elected))&((processes[2]!=messages[2]))))|(((((message_exist[1]=elected))&((processes[1]!=messages[1]))))|(((((message_exist[0]=elected))&((processes[0]=messages[0]))))|(((((message_exist[4]=elected))&((processes[4]=messages[4]))))|(((((message_exist[3]=elected))&((processes[3]=messages[3]))))|(((((message_exist[2]=elected))&((processes[2]=messages[2]))))|(((((message_exist[1]=elected))&((processes[1]=messages[1]))))|(((((message_exist[0]=election))&((processes[0]=messages[0]))))|(((((message_exist[4]=election))&((processes[4]=messages[4]))))|(((((message_exist[3]=election))&((processes[3]=messages[3]))))|(((((message_exist[2]=election))&((processes[2]=messages[2]))))|(((((message_exist[1]=election))&((processes[1]=messages[1]))))|(((((message_exist[0]=election))&((processes[0]>messages[0]))))|(((((message_exist[4]=election))&((processes[4]>messages[4]))))|(((((message_exist[3]=election))&((processes[3]>messages[3]))))|(((((message_exist[2]=election))&((processes[2]>messages[2]))))|(((((message_exist[1]=election))&((processes[1]>messages[1]))))|(((((message_exist[0]=election))&((messages[0]>processes[0]))))|(((((message_exist[4]=election))&((messages[4]>processes[4]))))|(((((message_exist[3]=election))&((messages[3]>processes[3]))))|(((((message_exist[2]=election))&((messages[2]>processes[2]))))|(((((message_exist[1]=election))&((messages[1]>processes[1]))))|(((((message_exist[0]=elected))&((processes[0]!=messages[0]))))|(((((message_exist[4]=elected))&((processes[4]!=messages[4]))))|(((((message_exist[3]=elected))&((processes[3]!=messages[3]))))|(((((message_exist[2]=elected))&((processes[2]!=messages[2]))))|(((((message_exist[1]=elected))&((processes[1]!=messages[1]))))|(((((message_exist[0]=elected))&((processes[0]=messages[0]))))|(((((message_exist[4]=elected))&((processes[4]=messages[4]))))|(((((message_exist[3]=elected))&((processes[3]=messages[3]))))|(((((message_exist[2]=elected))&((processes[2]=messages[2]))))|(((((message_exist[1]=elected))&((processes[1]=messages[1]))))|(((((message_exist[0]=election))&((processes[0]=messages[0]))))|(((((message_exist[4]=election))&((processes[4]=messages[4]))))|(((((message_exist[3]=election))&((processes[3]=messages[3]))))|(((((message_exist[2]=election))&((processes[2]=messages[2]))))|(((((message_exist[1]=election))&((processes[1]=messages[1]))))|(((((message_exist[0]=election))&((processes[0]>messages[0]))))|(((((message_exist[4]=election))&((processes[4]>messages[4]))))|(((((message_exist[3]=election))&((processes[3]>messages[3]))))|(((((message_exist[2]=election))&((processes[2]>messages[2]))))|(((((message_exist[1]=election))&((processes[1]>messages[1]))))|(((((message_exist[0]=election))&((messages[0]>processes[0]))))|(((((message_exist[4]=election))&((messages[4]>processes[4]))))|(((((message_exist[3]=election))&((messages[3]>processes[3]))))|(((((message_exist[2]=election))&((messages[2]>processes[2]))))|(((((message_exist[1]=election))&((messages[1]>processes[1]))))|(init=1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) : 1; 1 : 0; esac; _fail := case _terminate : 0; (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((_trans=126)&!(init=1))|((_trans=125)&!((((message_exist[1]=election))&((messages[1]>processes[1]))))))|((_trans=124)&!((((message_exist[2]=election))&((messages[2]>processes[2]))))))|((_trans=123)&!((((message_exist[3]=election))&((messages[3]>processes[3]))))))|((_trans=122)&!((((message_exist[4]=election))&((messages[4]>processes[4]))))))|((_trans=121)&!((((message_exist[0]=election))&((messages[0]>processes[0]))))))|((_trans=120)&!((((message_exist[1]=election))&((processes[1]>messages[1]))))))|((_trans=119)&!((((message_exist[2]=election))&((processes[2]>messages[2]))))))|((_trans=118)&!((((message_exist[3]=election))&((processes[3]>messages[3]))))))|((_trans=117)&!((((message_exist[4]=election))&((processes[4]>messages[4]))))))|((_trans=116)&!((((message_exist[0]=election))&((processes[0]>messages[0]))))))|((_trans=115)&!((((message_exist[1]=election))&((processes[1]=messages[1]))))))|((_trans=114)&!((((message_exist[2]=election))&((processes[2]=messages[2]))))))|((_trans=113)&!((((message_exist[3]=election))&((processes[3]=messages[3]))))))|((_trans=112)&!((((message_exist[4]=election))&((processes[4]=messages[4]))))))|((_trans=111)&!((((message_exist[0]=election))&((processes[0]=messages[0]))))))|((_trans=110)&!((((message_exist[1]=elected))&((processes[1]=messages[1]))))))|((_trans=109)&!((((message_exist[2]=elected))&((processes[2]=messages[2]))))))|((_trans=108)&!((((message_exist[3]=elected))&((processes[3]=messages[3]))))))|((_trans=107)&!((((message_exist[4]=elected))&((processes[4]=messages[4]))))))|((_trans=106)&!((((message_exist[0]=elected))&((processes[0]=messages[0]))))))|((_trans=105)&!((((message_exist[1]=elected))&((processes[1]!=messages[1]))))))|((_trans=104)&!((((message_exist[2]=elected))&((processes[2]!=messages[2]))))))|((_trans=103)&!((((message_exist[3]=elected))&((processes[3]!=messages[3]))))))|((_trans=102)&!((((message_exist[4]=elected))&((processes[4]!=messages[4]))))))|((_trans=101)&!((((message_exist[0]=elected))&((processes[0]!=messages[0]))))))|((_trans=100)&!((((message_exist[1]=election))&((messages[1]>processes[1]))))))|((_trans=99)&!((((message_exist[2]=election))&((messages[2]>processes[2]))))))|((_trans=98)&!((((message_exist[3]=election))&((messages[3]>processes[3]))))))|((_trans=97)&!((((message_exist[4]=election))&((messages[4]>processes[4]))))))|((_trans=96)&!((((message_exist[0]=election))&((messages[0]>processes[0]))))))|((_trans=95)&!((((message_exist[1]=election))&((processes[1]>messages[1]))))))|((_trans=94)&!((((message_exist[2]=election))&((processes[2]>messages[2]))))))|((_trans=93)&!((((message_exist[3]=election))&((processes[3]>messages[3]))))))|((_trans=92)&!((((message_exist[4]=election))&((processes[4]>messages[4]))))))|((_trans=91)&!((((message_exist[0]=election))&((processes[0]>messages[0]))))))|((_trans=90)&!((((message_exist[1]=election))&((processes[1]=messages[1]))))))|((_trans=89)&!((((message_exist[2]=election))&((processes[2]=messages[2]))))))|((_trans=88)&!((((message_exist[3]=election))&((processes[3]=messages[3]))))))|((_trans=87)&!((((message_exist[4]=election))&((processes[4]=messages[4]))))))|((_trans=86)&!((((message_exist[0]=election))&((processes[0]=messages[0]))))))|((_trans=85)&!((((message_exist[1]=elected))&((processes[1]=messages[1]))))))|((_trans=84)&!((((message_exist[2]=elected))&((processes[2]=messages[2]))))))|((_trans=83)&!((((message_exist[3]=elected))&((processes[3]=messages[3]))))))|((_trans=82)&!((((message_exist[4]=elected))&((processes[4]=messages[4]))))))|((_trans=81)&!((((message_exist[0]=elected))&((processes[0]=messages[0]))))))|((_trans=80)&!((((message_exist[1]=elected))&((processes[1]!=messages[1]))))))|((_trans=79)&!((((message_exist[2]=elected))&((processes[2]!=messages[2]))))))|((_trans=78)&!((((message_exist[3]=elected))&((processes[3]!=messages[3]))))))|((_trans=77)&!((((message_exist[4]=elected))&((processes[4]!=messages[4]))))))|((_trans=76)&!((((message_exist[0]=elected))&((processes[0]!=messages[0]))))))|((_trans=75)&!((((message_exist[1]=election))&((messages[1]>processes[1]))))))|((_trans=74)&!((((message_exist[2]=election))&((messages[2]>processes[2]))))))|((_trans=73)&!((((message_exist[3]=election))&((messages[3]>processes[3]))))))|((_trans=72)&!((((message_exist[4]=election))&((messages[4]>processes[4]))))))|((_trans=71)&!((((message_exist[0]=election))&((messages[0]>processes[0]))))))|((_trans=70)&!((((message_exist[1]=election))&((processes[1]>messages[1]))))))|((_trans=69)&!((((message_exist[2]=election))&((processes[2]>messages[2]))))))|((_trans=68)&!((((message_exist[3]=election))&((processes[3]>messages[3]))))))|((_trans=67)&!((((message_exist[4]=election))&((processes[4]>messages[4]))))))|((_trans=66)&!((((message_exist[0]=election))&((processes[0]>messages[0]))))))|((_trans=65)&!((((message_exist[1]=election))&((processes[1]=messages[1]))))))|((_trans=64)&!((((message_exist[2]=election))&((processes[2]=messages[2]))))))|((_trans=63)&!((((message_exist[3]=election))&((processes[3]=messages[3]))))))|((_trans=62)&!((((message_exist[4]=election))&((processes[4]=messages[4]))))))|((_trans=61)&!((((message_exist[0]=election))&((processes[0]=messages[0]))))))|((_trans=60)&!((((message_exist[1]=elected))&((processes[1]=messages[1]))))))|((_trans=59)&!((((message_exist[2]=elected))&((processes[2]=messages[2]))))))|((_trans=58)&!((((message_exist[3]=elected))&((processes[3]=messages[3]))))))|((_trans=57)&!((((message_exist[4]=elected))&((processes[4]=messages[4]))))))|((_trans=56)&!((((message_exist[0]=elected))&((processes[0]=messages[0]))))))|((_trans=55)&!((((message_exist[1]=elected))&((processes[1]!=messages[1]))))))|((_trans=54)&!((((message_exist[2]=elected))&((processes[2]!=messages[2]))))))|((_trans=53)&!((((message_exist[3]=elected))&((processes[3]!=messages[3]))))))|((_trans=52)&!((((message_exist[4]=elected))&((processes[4]!=messages[4]))))))|((_trans=51)&!((((message_exist[0]=elected))&((processes[0]!=messages[0]))))))|((_trans=50)&!((((message_exist[1]=election))&((messages[1]>processes[1]))))))|((_trans=49)&!((((message_exist[2]=election))&((messages[2]>processes[2]))))))|((_trans=48)&!((((message_exist[3]=election))&((messages[3]>processes[3]))))))|((_trans=47)&!((((message_exist[4]=election))&((messages[4]>processes[4]))))))|((_trans=46)&!((((message_exist[0]=election))&((messages[0]>processes[0]))))))|((_trans=45)&!((((message_exist[1]=election))&((processes[1]>messages[1]))))))|((_trans=44)&!((((message_exist[2]=election))&((processes[2]>messages[2]))))))|((_trans=43)&!((((message_exist[3]=election))&((processes[3]>messages[3]))))))|((_trans=42)&!((((message_exist[4]=election))&((processes[4]>messages[4]))))))|((_trans=41)&!((((message_exist[0]=election))&((processes[0]>messages[0]))))))|((_trans=40)&!((((message_exist[1]=election))&((processes[1]=messages[1]))))))|((_trans=39)&!((((message_exist[2]=election))&((processes[2]=messages[2]))))))|((_trans=38)&!((((message_exist[3]=election))&((processes[3]=messages[3]))))))|((_trans=37)&!((((message_exist[4]=election))&((processes[4]=messages[4]))))))|((_trans=36)&!((((message_exist[0]=election))&((processes[0]=messages[0]))))))|((_trans=35)&!((((message_exist[1]=elected))&((processes[1]=messages[1]))))))|((_trans=34)&!((((message_exist[2]=elected))&((processes[2]=messages[2]))))))|((_trans=33)&!((((message_exist[3]=elected))&((processes[3]=messages[3]))))))|((_trans=32)&!((((message_exist[4]=elected))&((processes[4]=messages[4]))))))|((_trans=31)&!((((message_exist[0]=elected))&((processes[0]=messages[0]))))))|((_trans=30)&!((((message_exist[1]=elected))&((processes[1]!=messages[1]))))))|((_trans=29)&!((((message_exist[2]=elected))&((processes[2]!=messages[2]))))))|((_trans=28)&!((((message_exist[3]=elected))&((processes[3]!=messages[3]))))))|((_trans=27)&!((((message_exist[4]=elected))&((processes[4]!=messages[4]))))))|((_trans=26)&!((((message_exist[0]=elected))&((processes[0]!=messages[0]))))))|((_trans=25)&!((((message_exist[1]=election))&((messages[1]>processes[1]))))))|((_trans=24)&!((((message_exist[2]=election))&((messages[2]>processes[2]))))))|((_trans=23)&!((((message_exist[3]=election))&((messages[3]>processes[3]))))))|((_trans=22)&!((((message_exist[4]=election))&((messages[4]>processes[4]))))))|((_trans=21)&!((((message_exist[0]=election))&((messages[0]>processes[0]))))))|((_trans=20)&!((((message_exist[1]=election))&((processes[1]>messages[1]))))))|((_trans=19)&!((((message_exist[2]=election))&((processes[2]>messages[2]))))))|((_trans=18)&!((((message_exist[3]=election))&((processes[3]>messages[3]))))))|((_trans=17)&!((((message_exist[4]=election))&((processes[4]>messages[4]))))))|((_trans=16)&!((((message_exist[0]=election))&((processes[0]>messages[0]))))))|((_trans=15)&!((((message_exist[1]=election))&((processes[1]=messages[1]))))))|((_trans=14)&!((((message_exist[2]=election))&((processes[2]=messages[2]))))))|((_trans=13)&!((((message_exist[3]=election))&((processes[3]=messages[3]))))))|((_trans=12)&!((((message_exist[4]=election))&((processes[4]=messages[4]))))))|((_trans=11)&!((((message_exist[0]=election))&((processes[0]=messages[0]))))))|((_trans=10)&!((((message_exist[1]=elected))&((processes[1]=messages[1]))))))|((_trans=9)&!((((message_exist[2]=elected))&((processes[2]=messages[2]))))))|((_trans=8)&!((((message_exist[3]=elected))&((processes[3]=messages[3]))))))|((_trans=7)&!((((message_exist[4]=elected))&((processes[4]=messages[4]))))))|((_trans=6)&!((((message_exist[0]=elected))&((processes[0]=messages[0]))))))|((_trans=5)&!((((message_exist[1]=elected))&((processes[1]!=messages[1]))))))|((_trans=4)&!((((message_exist[2]=elected))&((processes[2]!=messages[2]))))))|((_trans=3)&!((((message_exist[3]=elected))&((processes[3]!=messages[3]))))))|((_trans=2)&!((((message_exist[4]=elected))&((processes[4]!=messages[4]))))))|((_trans=1)&!((((message_exist[0]=elected))&((processes[0]!=messages[0])))))) : 1; 1 : 0; esac; init(proc5) := 4; next(proc5) := proc5; init(proc4) := 3; next(proc4) := proc4; init(proc3) := 2; next(proc3) := proc3; init(proc2) := 1; next(proc2) := proc2; init(proc1) := 0; next(proc1) := proc1; init(leader_PROCESS_PROCESS_PROCESS_PROCESS) := -1; next(leader_PROCESS_PROCESS_PROCESS_PROCESS) := case (next(_trans)=15) : -100..100; (next(_trans)=14) : -100..100; (next(_trans)=13) : -100..100; (next(_trans)=12) : -100..100; (next(_trans)=11) : -100..100; (next(_trans)=5) : -100..100; (next(_trans)=4) : -100..100; (next(_trans)=3) : -100..100; (next(_trans)=2) : -100..100; (next(_trans)=1) : -100..100; 1 : leader_PROCESS_PROCESS_PROCESS_PROCESS; esac; init(leader_PROCESS_PROCESS_PROCESS) := -1; next(leader_PROCESS_PROCESS_PROCESS) := case (next(_trans)=40) : -100..100; (next(_trans)=39) : -100..100; (next(_trans)=38) : -100..100; (next(_trans)=37) : -100..100; (next(_trans)=36) : -100..100; (next(_trans)=30) : -100..100; (next(_trans)=29) : -100..100; (next(_trans)=28) : -100..100; (next(_trans)=27) : -100..100; (next(_trans)=26) : -100..100; 1 : leader_PROCESS_PROCESS_PROCESS; esac; init(leader_PROCESS_PROCESS) := -1; next(leader_PROCESS_PROCESS) := case (next(_trans)=65) : -100..100; (next(_trans)=64) : -100..100; (next(_trans)=63) : -100..100; (next(_trans)=62) : -100..100; (next(_trans)=61) : -100..100; (next(_trans)=55) : -100..100; (next(_trans)=54) : -100..100; (next(_trans)=53) : -100..100; (next(_trans)=52) : -100..100; (next(_trans)=51) : -100..100; 1 : leader_PROCESS_PROCESS; esac; init(leader_PROCESS) := -1; next(leader_PROCESS) := case (next(_trans)=90) : -100..100; (next(_trans)=89) : -100..100; (next(_trans)=88) : -100..100; (next(_trans)=87) : -100..100; (next(_trans)=86) : -100..100; (next(_trans)=80) : -100..100; (next(_trans)=79) : -100..100; (next(_trans)=78) : -100..100; (next(_trans)=77) : -100..100; (next(_trans)=76) : -100..100; 1 : leader_PROCESS; esac; init(leader) := -1; next(leader) := case (next(_trans)=115) : -100..100; (next(_trans)=114) : -100..100; (next(_trans)=113) : -100..100; (next(_trans)=112) : -100..100; (next(_trans)=111) : -100..100; (next(_trans)=105) : -100..100; (next(_trans)=104) : -100..100; (next(_trans)=103) : -100..100; (next(_trans)=102) : -100..100; (next(_trans)=101) : -100..100; 1 : leader; esac; init(init) := 1; next(init) := case (next(_trans)=126) : 0; 1 : init; esac; next(processes[4]) := processes[4]; next(processes[3]) := processes[3]; next(processes[2]) := processes[2]; next(processes[1]) := processes[1]; next(processes[0]) := processes[0]; next(messages[4]) := case (next(_trans)=106) : leader; (next(_trans)=81) : leader_PROCESS; (next(_trans)=56) : leader_PROCESS_PROCESS; (next(_trans)=31) : leader_PROCESS_PROCESS_PROCESS; (next(_trans)=6) : leader_PROCESS_PROCESS_PROCESS_PROCESS; (next(_trans)=126) : -100..100; (next(_trans)=121) : -100..100; (next(_trans)=116) : -100..100; (next(_trans)=111) : -100..100; (next(_trans)=101) : -100..100; (next(_trans)=96) : -100..100; (next(_trans)=91) : -100..100; (next(_trans)=86) : -100..100; (next(_trans)=76) : -100..100; (next(_trans)=71) : -100..100; (next(_trans)=66) : -100..100; (next(_trans)=61) : -100..100; (next(_trans)=51) : -100..100; (next(_trans)=46) : -100..100; (next(_trans)=41) : -100..100; (next(_trans)=36) : -100..100; (next(_trans)=26) : -100..100; (next(_trans)=21) : -100..100; (next(_trans)=16) : -100..100; (next(_trans)=11) : -100..100; (next(_trans)=1) : -100..100; 1 : messages[4]; esac; next(messages[3]) := case (next(_trans)=107) : leader; (next(_trans)=82) : leader_PROCESS; (next(_trans)=57) : leader_PROCESS_PROCESS; (next(_trans)=32) : leader_PROCESS_PROCESS_PROCESS; (next(_trans)=7) : leader_PROCESS_PROCESS_PROCESS_PROCESS; (next(_trans)=122) : -100..100; (next(_trans)=117) : -100..100; (next(_trans)=112) : -100..100; (next(_trans)=102) : -100..100; (next(_trans)=97) : -100..100; (next(_trans)=92) : -100..100; (next(_trans)=87) : -100..100; (next(_trans)=77) : -100..100; (next(_trans)=72) : -100..100; (next(_trans)=67) : -100..100; (next(_trans)=62) : -100..100; (next(_trans)=52) : -100..100; (next(_trans)=47) : -100..100; (next(_trans)=42) : -100..100; (next(_trans)=37) : -100..100; (next(_trans)=27) : -100..100; (next(_trans)=22) : -100..100; (next(_trans)=17) : -100..100; (next(_trans)=12) : -100..100; (next(_trans)=2) : -100..100; 1 : messages[3]; esac; next(messages[2]) := case (next(_trans)=108) : leader; (next(_trans)=83) : leader_PROCESS; (next(_trans)=58) : leader_PROCESS_PROCESS; (next(_trans)=33) : leader_PROCESS_PROCESS_PROCESS; (next(_trans)=8) : leader_PROCESS_PROCESS_PROCESS_PROCESS; (next(_trans)=123) : -100..100; (next(_trans)=118) : -100..100; (next(_trans)=113) : -100..100; (next(_trans)=103) : -100..100; (next(_trans)=98) : -100..100; (next(_trans)=93) : -100..100; (next(_trans)=88) : -100..100; (next(_trans)=78) : -100..100; (next(_trans)=73) : -100..100; (next(_trans)=68) : -100..100; (next(_trans)=63) : -100..100; (next(_trans)=53) : -100..100; (next(_trans)=48) : -100..100; (next(_trans)=43) : -100..100; (next(_trans)=38) : -100..100; (next(_trans)=28) : -100..100; (next(_trans)=23) : -100..100; (next(_trans)=18) : -100..100; (next(_trans)=13) : -100..100; (next(_trans)=3) : -100..100; 1 : messages[2]; esac; next(messages[1]) := case (next(_trans)=109) : leader; (next(_trans)=84) : leader_PROCESS; (next(_trans)=59) : leader_PROCESS_PROCESS; (next(_trans)=34) : leader_PROCESS_PROCESS_PROCESS; (next(_trans)=9) : leader_PROCESS_PROCESS_PROCESS_PROCESS; (next(_trans)=124) : -100..100; (next(_trans)=119) : -100..100; (next(_trans)=114) : -100..100; (next(_trans)=104) : -100..100; (next(_trans)=99) : -100..100; (next(_trans)=94) : -100..100; (next(_trans)=89) : -100..100; (next(_trans)=79) : -100..100; (next(_trans)=74) : -100..100; (next(_trans)=69) : -100..100; (next(_trans)=64) : -100..100; (next(_trans)=54) : -100..100; (next(_trans)=49) : -100..100; (next(_trans)=44) : -100..100; (next(_trans)=39) : -100..100; (next(_trans)=29) : -100..100; (next(_trans)=24) : -100..100; (next(_trans)=19) : -100..100; (next(_trans)=14) : -100..100; (next(_trans)=4) : -100..100; 1 : messages[1]; esac; next(messages[0]) := case (next(_trans)=110) : leader; (next(_trans)=85) : leader_PROCESS; (next(_trans)=60) : leader_PROCESS_PROCESS; (next(_trans)=35) : leader_PROCESS_PROCESS_PROCESS; (next(_trans)=10) : leader_PROCESS_PROCESS_PROCESS_PROCESS; (next(_trans)=125) : -100..100; (next(_trans)=120) : -100..100; (next(_trans)=115) : -100..100; (next(_trans)=105) : -100..100; (next(_trans)=100) : -100..100; (next(_trans)=95) : -100..100; (next(_trans)=90) : -100..100; (next(_trans)=80) : -100..100; (next(_trans)=75) : -100..100; (next(_trans)=70) : -100..100; (next(_trans)=65) : -100..100; (next(_trans)=55) : -100..100; (next(_trans)=50) : -100..100; (next(_trans)=45) : -100..100; (next(_trans)=40) : -100..100; (next(_trans)=30) : -100..100; (next(_trans)=25) : -100..100; (next(_trans)=20) : -100..100; (next(_trans)=15) : -100..100; (next(_trans)=5) : -100..100; 1 : messages[0]; esac; init(message_exist[4]) := no_message; next(message_exist[4]) := case (next(_trans)=126) : election; (next(_trans)=122) : no_message; (next(_trans)=121) : election; (next(_trans)=117) : no_message; (next(_trans)=116) : election; (next(_trans)=112) : no_message; (next(_trans)=111) : elected; (next(_trans)=107) : no_message; (next(_trans)=106) : elected; (next(_trans)=102) : no_message; (next(_trans)=101) : elected; (next(_trans)=97) : no_message; (next(_trans)=96) : election; (next(_trans)=92) : no_message; (next(_trans)=91) : election; (next(_trans)=87) : no_message; (next(_trans)=86) : elected; (next(_trans)=82) : no_message; (next(_trans)=81) : elected; (next(_trans)=77) : no_message; (next(_trans)=76) : elected; (next(_trans)=72) : no_message; (next(_trans)=71) : election; (next(_trans)=67) : no_message; (next(_trans)=66) : election; (next(_trans)=62) : no_message; (next(_trans)=61) : elected; (next(_trans)=57) : no_message; (next(_trans)=56) : elected; (next(_trans)=52) : no_message; (next(_trans)=51) : elected; (next(_trans)=47) : no_message; (next(_trans)=46) : election; (next(_trans)=42) : no_message; (next(_trans)=41) : election; (next(_trans)=37) : no_message; (next(_trans)=36) : elected; (next(_trans)=32) : no_message; (next(_trans)=31) : elected; (next(_trans)=27) : no_message; (next(_trans)=26) : elected; (next(_trans)=22) : no_message; (next(_trans)=21) : election; (next(_trans)=17) : no_message; (next(_trans)=16) : election; (next(_trans)=12) : no_message; (next(_trans)=11) : elected; (next(_trans)=7) : no_message; (next(_trans)=6) : elected; (next(_trans)=2) : no_message; (next(_trans)=1) : elected; 1 : message_exist[4]; esac; init(message_exist[3]) := no_message; next(message_exist[3]) := case (next(_trans)=123) : no_message; (next(_trans)=122) : election; (next(_trans)=118) : no_message; (next(_trans)=117) : election; (next(_trans)=113) : no_message; (next(_trans)=112) : elected; (next(_trans)=108) : no_message; (next(_trans)=107) : elected; (next(_trans)=103) : no_message; (next(_trans)=102) : elected; (next(_trans)=98) : no_message; (next(_trans)=97) : election; (next(_trans)=93) : no_message; (next(_trans)=92) : election; (next(_trans)=88) : no_message; (next(_trans)=87) : elected; (next(_trans)=83) : no_message; (next(_trans)=82) : elected; (next(_trans)=78) : no_message; (next(_trans)=77) : elected; (next(_trans)=73) : no_message; (next(_trans)=72) : election; (next(_trans)=68) : no_message; (next(_trans)=67) : election; (next(_trans)=63) : no_message; (next(_trans)=62) : elected; (next(_trans)=58) : no_message; (next(_trans)=57) : elected; (next(_trans)=53) : no_message; (next(_trans)=52) : elected; (next(_trans)=48) : no_message; (next(_trans)=47) : election; (next(_trans)=43) : no_message; (next(_trans)=42) : election; (next(_trans)=38) : no_message; (next(_trans)=37) : elected; (next(_trans)=33) : no_message; (next(_trans)=32) : elected; (next(_trans)=28) : no_message; (next(_trans)=27) : elected; (next(_trans)=23) : no_message; (next(_trans)=22) : election; (next(_trans)=18) : no_message; (next(_trans)=17) : election; (next(_trans)=13) : no_message; (next(_trans)=12) : elected; (next(_trans)=8) : no_message; (next(_trans)=7) : elected; (next(_trans)=3) : no_message; (next(_trans)=2) : elected; 1 : message_exist[3]; esac; init(message_exist[2]) := no_message; next(message_exist[2]) := case (next(_trans)=124) : no_message; (next(_trans)=123) : election; (next(_trans)=119) : no_message; (next(_trans)=118) : election; (next(_trans)=114) : no_message; (next(_trans)=113) : elected; (next(_trans)=109) : no_message; (next(_trans)=108) : elected; (next(_trans)=104) : no_message; (next(_trans)=103) : elected; (next(_trans)=99) : no_message; (next(_trans)=98) : election; (next(_trans)=94) : no_message; (next(_trans)=93) : election; (next(_trans)=89) : no_message; (next(_trans)=88) : elected; (next(_trans)=84) : no_message; (next(_trans)=83) : elected; (next(_trans)=79) : no_message; (next(_trans)=78) : elected; (next(_trans)=74) : no_message; (next(_trans)=73) : election; (next(_trans)=69) : no_message; (next(_trans)=68) : election; (next(_trans)=64) : no_message; (next(_trans)=63) : elected; (next(_trans)=59) : no_message; (next(_trans)=58) : elected; (next(_trans)=54) : no_message; (next(_trans)=53) : elected; (next(_trans)=49) : no_message; (next(_trans)=48) : election; (next(_trans)=44) : no_message; (next(_trans)=43) : election; (next(_trans)=39) : no_message; (next(_trans)=38) : elected; (next(_trans)=34) : no_message; (next(_trans)=33) : elected; (next(_trans)=29) : no_message; (next(_trans)=28) : elected; (next(_trans)=24) : no_message; (next(_trans)=23) : election; (next(_trans)=19) : no_message; (next(_trans)=18) : election; (next(_trans)=14) : no_message; (next(_trans)=13) : elected; (next(_trans)=9) : no_message; (next(_trans)=8) : elected; (next(_trans)=4) : no_message; (next(_trans)=3) : elected; 1 : message_exist[2]; esac; init(message_exist[1]) := no_message; next(message_exist[1]) := case (next(_trans)=125) : no_message; (next(_trans)=124) : election; (next(_trans)=120) : no_message; (next(_trans)=119) : election; (next(_trans)=115) : no_message; (next(_trans)=114) : elected; (next(_trans)=110) : no_message; (next(_trans)=109) : elected; (next(_trans)=105) : no_message; (next(_trans)=104) : elected; (next(_trans)=100) : no_message; (next(_trans)=99) : election; (next(_trans)=95) : no_message; (next(_trans)=94) : election; (next(_trans)=90) : no_message; (next(_trans)=89) : elected; (next(_trans)=85) : no_message; (next(_trans)=84) : elected; (next(_trans)=80) : no_message; (next(_trans)=79) : elected; (next(_trans)=75) : no_message; (next(_trans)=74) : election; (next(_trans)=70) : no_message; (next(_trans)=69) : election; (next(_trans)=65) : no_message; (next(_trans)=64) : elected; (next(_trans)=60) : no_message; (next(_trans)=59) : elected; (next(_trans)=55) : no_message; (next(_trans)=54) : elected; (next(_trans)=50) : no_message; (next(_trans)=49) : election; (next(_trans)=45) : no_message; (next(_trans)=44) : election; (next(_trans)=40) : no_message; (next(_trans)=39) : elected; (next(_trans)=35) : no_message; (next(_trans)=34) : elected; (next(_trans)=30) : no_message; (next(_trans)=29) : elected; (next(_trans)=25) : no_message; (next(_trans)=24) : election; (next(_trans)=20) : no_message; (next(_trans)=19) : election; (next(_trans)=15) : no_message; (next(_trans)=14) : elected; (next(_trans)=10) : no_message; (next(_trans)=9) : elected; (next(_trans)=5) : no_message; (next(_trans)=4) : elected; 1 : message_exist[1]; esac; init(message_exist[0]) := no_message; next(message_exist[0]) := case (next(_trans)=125) : election; (next(_trans)=121) : no_message; (next(_trans)=120) : election; (next(_trans)=116) : no_message; (next(_trans)=115) : elected; (next(_trans)=111) : no_message; (next(_trans)=110) : elected; (next(_trans)=106) : no_message; (next(_trans)=105) : elected; (next(_trans)=101) : no_message; (next(_trans)=100) : election; (next(_trans)=96) : no_message; (next(_trans)=95) : election; (next(_trans)=91) : no_message; (next(_trans)=90) : elected; (next(_trans)=86) : no_message; (next(_trans)=85) : elected; (next(_trans)=81) : no_message; (next(_trans)=80) : elected; (next(_trans)=76) : no_message; (next(_trans)=75) : election; (next(_trans)=71) : no_message; (next(_trans)=70) : election; (next(_trans)=66) : no_message; (next(_trans)=65) : elected; (next(_trans)=61) : no_message; (next(_trans)=60) : elected; (next(_trans)=56) : no_message; (next(_trans)=55) : elected; (next(_trans)=51) : no_message; (next(_trans)=50) : election; (next(_trans)=46) : no_message; (next(_trans)=45) : election; (next(_trans)=41) : no_message; (next(_trans)=40) : elected; (next(_trans)=36) : no_message; (next(_trans)=35) : elected; (next(_trans)=31) : no_message; (next(_trans)=30) : elected; (next(_trans)=26) : no_message; (next(_trans)=25) : election; (next(_trans)=21) : no_message; (next(_trans)=20) : election; (next(_trans)=16) : no_message; (next(_trans)=15) : elected; (next(_trans)=11) : no_message; (next(_trans)=10) : elected; (next(_trans)=6) : no_message; (next(_trans)=5) : elected; (next(_trans)=1) : no_message; 1 : message_exist[0]; esac;