const
	NumProcess	:	5;
	MININT	:	-32768;
	MAXINT	:	32767;
type
	message_state	:	enum { election,elected,no_message };
var
	fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1_1	:	BOOLEAN;
	fail_1_1_1_1	:	BOOLEAN;
	fail_1_1_1	:	BOOLEAN;
	fail_1_1	:	BOOLEAN;
	fail_1	:	BOOLEAN;
	fail	:	BOOLEAN;
	PC	:	MININT..MAXINT;
	message_exist	:	array [0..NumProcess-1] of message_state;
	messages	:	array [0..NumProcess-1] of MININT..MAXINT;
	processes	:	array [0..NumProcess-1] of MININT..MAXINT;
	init	:	BOOLEAN;
	leader	:	MININT..MAXINT;
	leader_PROCESS	:	MININT..MAXINT;
	leader_PROCESS_PROCESS	:	MININT..MAXINT;
	leader_PROCESS_PROCESS_PROCESS	:	MININT..MAXINT;
	leader_PROCESS_PROCESS_PROCESS_PROCESS	:	MININT..MAXINT;
	proc1	:	MININT..MAXINT;
	proc2	:	MININT..MAXINT;
	proc3	:	MININT..MAXINT;
	proc4	:	MININT..MAXINT;
	proc5	:	MININT..MAXINT;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable messages */ 
Ruleset i_1 : 0..NumProcess-1 Do
Ruleset i_1_1 : MININT..MAXINT Do
Rule 
PC=0 | PC=14 | PC=28 | PC=42 | PC=56 | PC=70 | PC=84 | PC=98 | PC=112 | PC=126 | PC=140 | PC=154 | PC=168 | PC=182 | PC=196 | PC=210 | PC=224 | PC=238 | PC=252 | PC=266 | PC=280 | PC=294
==>
begin
  messages[i_1]:=i_1_1;
  if PC=294 then
    PC:=295
  end;
  if PC=280 then
    PC:=281
  end;
  if PC=266 then
    PC:=267
  end;
  if PC=252 then
    PC:=253
  end;
  if PC=238 then
    PC:=239
  end;
  if PC=224 then
    PC:=225
  end;
  if PC=210 then
    PC:=211
  end;
  if PC=196 then
    PC:=197
  end;
  if PC=182 then
    PC:=183
  end;
  if PC=168 then
    PC:=169
  end;
  if PC=154 then
    PC:=155
  end;
  if PC=140 then
    PC:=141
  end;
  if PC=126 then
    PC:=127
  end;
  if PC=112 then
    PC:=113
  end;
  if PC=98 then
    PC:=99
  end;
  if PC=84 then
    PC:=85
  end;
  if PC=70 then
    PC:=71
  end;
  if PC=56 then
    PC:=57
  end;
  if PC=42 then
    PC:=43
  end;
  if PC=28 then
    PC:=29
  end;
  if PC=14 then
    PC:=15
  end;
  if PC=0 then
    PC:=1
  end;
end;
end;
end;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable processes */ 
Ruleset i_1 : 0..NumProcess-1 Do
Ruleset i_1_1 : MININT..MAXINT Do
Rule 
PC=1 | PC=13 | PC=27 | PC=41 | PC=55 | PC=69 | PC=83 | PC=97 | PC=111 | PC=125 | PC=139 | PC=153 | PC=167 | PC=181 | PC=195 | PC=209 | PC=223 | PC=237 | PC=251 | PC=265 | PC=279 | PC=293
==>
begin
  processes[i_1]:=i_1_1;
  if PC=293 then
    PC:=294
  end;
  if PC=279 then
    PC:=280
  end;
  if PC=265 then
    PC:=266
  end;
  if PC=251 then
    PC:=252
  end;
  if PC=237 then
    PC:=238
  end;
  if PC=223 then
    PC:=224
  end;
  if PC=209 then
    PC:=210
  end;
  if PC=195 then
    PC:=196
  end;
  if PC=181 then
    PC:=182
  end;
  if PC=167 then
    PC:=168
  end;
  if PC=153 then
    PC:=154
  end;
  if PC=139 then
    PC:=140
  end;
  if PC=125 then
    PC:=126
  end;
  if PC=111 then
    PC:=112
  end;
  if PC=97 then
    PC:=98
  end;
  if PC=83 then
    PC:=84
  end;
  if PC=69 then
    PC:=70
  end;
  if PC=55 then
    PC:=56
  end;
  if PC=41 then
    PC:=42
  end;
  if PC=27 then
    PC:=28
  end;
  if PC=13 then
    PC:=14
  end;
  if PC=1 then
    PC:=2
  end;
end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to proc5 that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=3 | PC=16 | PC=30 | PC=44 | PC=58 | PC=72 | PC=86 | PC=100 | PC=114 | PC=128 | PC=142 | PC=156 | PC=170 | PC=184 | PC=198 | PC=212 | PC=226 | PC=240 | PC=254 | PC=268 | PC=282
==>
begin
  proc5:=i;
  if PC=282 then
    PC:=283
  end;
  if PC=268 then
    PC:=269
  end;
  if PC=254 then
    PC:=255
  end;
  if PC=240 then
    PC:=241
  end;
  if PC=226 then
    PC:=227
  end;
  if PC=212 then
    PC:=213
  end;
  if PC=198 then
    PC:=199
  end;
  if PC=184 then
    PC:=185
  end;
  if PC=170 then
    PC:=171
  end;
  if PC=156 then
    PC:=157
  end;
  if PC=142 then
    PC:=143
  end;
  if PC=128 then
    PC:=129
  end;
  if PC=114 then
    PC:=115
  end;
  if PC=100 then
    PC:=101
  end;
  if PC=86 then
    PC:=87
  end;
  if PC=72 then
    PC:=73
  end;
  if PC=58 then
    PC:=59
  end;
  if PC=44 then
    PC:=45
  end;
  if PC=30 then
    PC:=31
  end;
  if PC=16 then
    PC:=17
  end;
  if PC=3 then
    PC:=4
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to proc4 that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=4 | PC=17 | PC=31 | PC=45 | PC=59 | PC=73 | PC=87 | PC=101 | PC=115 | PC=129 | PC=143 | PC=157 | PC=171 | PC=185 | PC=199 | PC=213 | PC=227 | PC=241 | PC=255 | PC=269 | PC=283
==>
begin
  proc4:=i;
  if PC=283 then
    PC:=284
  end;
  if PC=269 then
    PC:=270
  end;
  if PC=255 then
    PC:=256
  end;
  if PC=241 then
    PC:=242
  end;
  if PC=227 then
    PC:=228
  end;
  if PC=213 then
    PC:=214
  end;
  if PC=199 then
    PC:=200
  end;
  if PC=185 then
    PC:=186
  end;
  if PC=171 then
    PC:=172
  end;
  if PC=157 then
    PC:=158
  end;
  if PC=143 then
    PC:=144
  end;
  if PC=129 then
    PC:=130
  end;
  if PC=115 then
    PC:=116
  end;
  if PC=101 then
    PC:=102
  end;
  if PC=87 then
    PC:=88
  end;
  if PC=73 then
    PC:=74
  end;
  if PC=59 then
    PC:=60
  end;
  if PC=45 then
    PC:=46
  end;
  if PC=31 then
    PC:=32
  end;
  if PC=17 then
    PC:=18
  end;
  if PC=4 then
    PC:=5
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to proc3 that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=5 | PC=18 | PC=32 | PC=46 | PC=60 | PC=74 | PC=88 | PC=102 | PC=116 | PC=130 | PC=144 | PC=158 | PC=172 | PC=186 | PC=200 | PC=214 | PC=228 | PC=242 | PC=256 | PC=270 | PC=284
==>
begin
  proc3:=i;
  if PC=284 then
    PC:=285
  end;
  if PC=270 then
    PC:=271
  end;
  if PC=256 then
    PC:=257
  end;
  if PC=242 then
    PC:=243
  end;
  if PC=228 then
    PC:=229
  end;
  if PC=214 then
    PC:=215
  end;
  if PC=200 then
    PC:=201
  end;
  if PC=186 then
    PC:=187
  end;
  if PC=172 then
    PC:=173
  end;
  if PC=158 then
    PC:=159
  end;
  if PC=144 then
    PC:=145
  end;
  if PC=130 then
    PC:=131
  end;
  if PC=116 then
    PC:=117
  end;
  if PC=102 then
    PC:=103
  end;
  if PC=88 then
    PC:=89
  end;
  if PC=74 then
    PC:=75
  end;
  if PC=60 then
    PC:=61
  end;
  if PC=46 then
    PC:=47
  end;
  if PC=32 then
    PC:=33
  end;
  if PC=18 then
    PC:=19
  end;
  if PC=5 then
    PC:=6
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to proc2 that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=6 | PC=19 | PC=33 | PC=47 | PC=61 | PC=75 | PC=89 | PC=103 | PC=117 | PC=131 | PC=145 | PC=159 | PC=173 | PC=187 | PC=201 | PC=215 | PC=229 | PC=243 | PC=257 | PC=271 | PC=285
==>
begin
  proc2:=i;
  if PC=285 then
    PC:=286
  end;
  if PC=271 then
    PC:=272
  end;
  if PC=257 then
    PC:=258
  end;
  if PC=243 then
    PC:=244
  end;
  if PC=229 then
    PC:=230
  end;
  if PC=215 then
    PC:=216
  end;
  if PC=201 then
    PC:=202
  end;
  if PC=187 then
    PC:=188
  end;
  if PC=173 then
    PC:=174
  end;
  if PC=159 then
    PC:=160
  end;
  if PC=145 then
    PC:=146
  end;
  if PC=131 then
    PC:=132
  end;
  if PC=117 then
    PC:=118
  end;
  if PC=103 then
    PC:=104
  end;
  if PC=89 then
    PC:=90
  end;
  if PC=75 then
    PC:=76
  end;
  if PC=61 then
    PC:=62
  end;
  if PC=47 then
    PC:=48
  end;
  if PC=33 then
    PC:=34
  end;
  if PC=19 then
    PC:=20
  end;
  if PC=6 then
    PC:=7
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to proc1 that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=7 | PC=20 | PC=34 | PC=48 | PC=62 | PC=76 | PC=90 | PC=104 | PC=118 | PC=132 | PC=146 | PC=160 | PC=174 | PC=188 | PC=202 | PC=216 | PC=230 | PC=244 | PC=258 | PC=272 | PC=286
==>
begin
  proc1:=i;
  if PC=286 then
    PC:=287
  end;
  if PC=272 then
    PC:=273
  end;
  if PC=258 then
    PC:=259
  end;
  if PC=244 then
    PC:=245
  end;
  if PC=230 then
    PC:=231
  end;
  if PC=216 then
    PC:=217
  end;
  if PC=202 then
    PC:=203
  end;
  if PC=188 then
    PC:=189
  end;
  if PC=174 then
    PC:=175
  end;
  if PC=160 then
    PC:=161
  end;
  if PC=146 then
    PC:=147
  end;
  if PC=132 then
    PC:=133
  end;
  if PC=118 then
    PC:=119
  end;
  if PC=104 then
    PC:=105
  end;
  if PC=90 then
    PC:=91
  end;
  if PC=76 then
    PC:=77
  end;
  if PC=62 then
    PC:=63
  end;
  if PC=48 then
    PC:=49
  end;
  if PC=34 then
    PC:=35
  end;
  if PC=20 then
    PC:=21
  end;
  if PC=7 then
    PC:=8
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to leader_PROCESS_PROCESS_PROCESS_PROCESS that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=8 | PC=21 | PC=35 | PC=49 | PC=63 | PC=77 | PC=91 | PC=105 | PC=119 | PC=133 | PC=147 | PC=161 | PC=175 | PC=189 | PC=203 | PC=217 | PC=231 | PC=245 | PC=259 | PC=273 | PC=287
==>
begin
  leader_PROCESS_PROCESS_PROCESS_PROCESS:=i;
  if PC=287 then
    PC:=288
  end;
  if PC=273 then
    PC:=274
  end;
  if PC=259 then
    PC:=260
  end;
  if PC=245 then
    PC:=246
  end;
  if PC=231 then
    PC:=232
  end;
  if PC=217 then
    PC:=218
  end;
  if PC=203 then
    PC:=204
  end;
  if PC=189 then
    PC:=190
  end;
  if PC=175 then
    PC:=176
  end;
  if PC=161 then
    PC:=162
  end;
  if PC=147 then
    PC:=148
  end;
  if PC=133 then
    PC:=134
  end;
  if PC=119 then
    PC:=120
  end;
  if PC=105 then
    PC:=106
  end;
  if PC=91 then
    PC:=92
  end;
  if PC=77 then
    PC:=78
  end;
  if PC=63 then
    PC:=64
  end;
  if PC=49 then
    PC:=50
  end;
  if PC=35 then
    PC:=36
  end;
  if PC=21 then
    PC:=22
  end;
  if PC=8 then
    PC:=9
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to leader_PROCESS_PROCESS_PROCESS that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=9 | PC=22 | PC=36 | PC=50 | PC=64 | PC=78 | PC=92 | PC=106 | PC=120 | PC=134 | PC=148 | PC=162 | PC=176 | PC=190 | PC=204 | PC=218 | PC=232 | PC=246 | PC=260 | PC=274 | PC=288
==>
begin
  leader_PROCESS_PROCESS_PROCESS:=i;
  if PC=288 then
    PC:=289
  end;
  if PC=274 then
    PC:=275
  end;
  if PC=260 then
    PC:=261
  end;
  if PC=246 then
    PC:=247
  end;
  if PC=232 then
    PC:=233
  end;
  if PC=218 then
    PC:=219
  end;
  if PC=204 then
    PC:=205
  end;
  if PC=190 then
    PC:=191
  end;
  if PC=176 then
    PC:=177
  end;
  if PC=162 then
    PC:=163
  end;
  if PC=148 then
    PC:=149
  end;
  if PC=134 then
    PC:=135
  end;
  if PC=120 then
    PC:=121
  end;
  if PC=106 then
    PC:=107
  end;
  if PC=92 then
    PC:=93
  end;
  if PC=78 then
    PC:=79
  end;
  if PC=64 then
    PC:=65
  end;
  if PC=50 then
    PC:=51
  end;
  if PC=36 then
    PC:=37
  end;
  if PC=22 then
    PC:=23
  end;
  if PC=9 then
    PC:=10
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to leader_PROCESS_PROCESS that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=10 | PC=23 | PC=37 | PC=51 | PC=65 | PC=79 | PC=93 | PC=107 | PC=121 | PC=135 | PC=149 | PC=163 | PC=177 | PC=191 | PC=205 | PC=219 | PC=233 | PC=247 | PC=261 | PC=275 | PC=289
==>
begin
  leader_PROCESS_PROCESS:=i;
  if PC=289 then
    PC:=290
  end;
  if PC=275 then
    PC:=276
  end;
  if PC=261 then
    PC:=262
  end;
  if PC=247 then
    PC:=248
  end;
  if PC=233 then
    PC:=234
  end;
  if PC=219 then
    PC:=220
  end;
  if PC=205 then
    PC:=206
  end;
  if PC=191 then
    PC:=192
  end;
  if PC=177 then
    PC:=178
  end;
  if PC=163 then
    PC:=164
  end;
  if PC=149 then
    PC:=150
  end;
  if PC=135 then
    PC:=136
  end;
  if PC=121 then
    PC:=122
  end;
  if PC=107 then
    PC:=108
  end;
  if PC=93 then
    PC:=94
  end;
  if PC=79 then
    PC:=80
  end;
  if PC=65 then
    PC:=66
  end;
  if PC=51 then
    PC:=52
  end;
  if PC=37 then
    PC:=38
  end;
  if PC=23 then
    PC:=24
  end;
  if PC=10 then
    PC:=11
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to leader_PROCESS that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=11 | PC=24 | PC=38 | PC=52 | PC=66 | PC=80 | PC=94 | PC=108 | PC=122 | PC=136 | PC=150 | PC=164 | PC=178 | PC=192 | PC=206 | PC=220 | PC=234 | PC=248 | PC=262 | PC=276 | PC=290
==>
begin
  leader_PROCESS:=i;
  if PC=290 then
    PC:=291
  end;
  if PC=276 then
    PC:=277
  end;
  if PC=262 then
    PC:=263
  end;
  if PC=248 then
    PC:=249
  end;
  if PC=234 then
    PC:=235
  end;
  if PC=220 then
    PC:=221
  end;
  if PC=206 then
    PC:=207
  end;
  if PC=192 then
    PC:=193
  end;
  if PC=178 then
    PC:=179
  end;
  if PC=164 then
    PC:=165
  end;
  if PC=150 then
    PC:=151
  end;
  if PC=136 then
    PC:=137
  end;
  if PC=122 then
    PC:=123
  end;
  if PC=108 then
    PC:=109
  end;
  if PC=94 then
    PC:=95
  end;
  if PC=80 then
    PC:=81
  end;
  if PC=66 then
    PC:=67
  end;
  if PC=52 then
    PC:=53
  end;
  if PC=38 then
    PC:=39
  end;
  if PC=24 then
    PC:=25
  end;
  if PC=11 then
    PC:=12
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to leader that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=12 | PC=25 | PC=39 | PC=53 | PC=67 | PC=81 | PC=95 | PC=109 | PC=123 | PC=137 | PC=151 | PC=165 | PC=179 | PC=193 | PC=207 | PC=221 | PC=235 | PC=249 | PC=263 | PC=277 | PC=291
==>
begin
  leader:=i;
  if PC=291 then
    PC:=292
  end;
  if PC=277 then
    PC:=278
  end;
  if PC=263 then
    PC:=264
  end;
  if PC=249 then
    PC:=250
  end;
  if PC=235 then
    PC:=236
  end;
  if PC=221 then
    PC:=222
  end;
  if PC=207 then
    PC:=208
  end;
  if PC=193 then
    PC:=194
  end;
  if PC=179 then
    PC:=180
  end;
  if PC=165 then
    PC:=166
  end;
  if PC=151 then
    PC:=152
  end;
  if PC=137 then
    PC:=138
  end;
  if PC=123 then
    PC:=124
  end;
  if PC=109 then
    PC:=110
  end;
  if PC=95 then
    PC:=96
  end;
  if PC=81 then
    PC:=82
  end;
  if PC=67 then
    PC:=68
  end;
  if PC=53 then
    PC:=54
  end;
  if PC=39 then
    PC:=40
  end;
  if PC=25 then
    PC:=26
  end;
  if PC=12 then
    PC:=13
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to init that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : BOOLEAN Do
Rule 
PC=26 | PC=40 | PC=54 | PC=68 | PC=82 | PC=96 | PC=110 | PC=124 | PC=138 | PC=152 | PC=166 | PC=180 | PC=194 | PC=208 | PC=222 | PC=236 | PC=250 | PC=264 | PC=278 | PC=292
==>
begin
  init:=i;
  if PC=292 then
    PC:=293
  end;
  if PC=278 then
    PC:=279
  end;
  if PC=264 then
    PC:=265
  end;
  if PC=250 then
    PC:=251
  end;
  if PC=236 then
    PC:=237
  end;
  if PC=222 then
    PC:=223
  end;
  if PC=208 then
    PC:=209
  end;
  if PC=194 then
    PC:=195
  end;
  if PC=180 then
    PC:=181
  end;
  if PC=166 then
    PC:=167
  end;
  if PC=152 then
    PC:=153
  end;
  if PC=138 then
    PC:=139
  end;
  if PC=124 then
    PC:=125
  end;
  if PC=110 then
    PC:=111
  end;
  if PC=96 then
    PC:=97
  end;
  if PC=82 then
    PC:=83
  end;
  if PC=68 then
    PC:=69
  end;
  if PC=54 then
    PC:=55
  end;
  if PC=40 then
    PC:=41
  end;
  if PC=26 then
    PC:=27
  end;
end;
end;

/* Rule created during translating relation */ 
Rule 
PC=295 & !(((messages [ (proc5 - 1) % NumProcess ] =messages [ proc5 ] ) & (leader_PROCESS_PROCESS_PROCESS_PROCESS=messages [ proc5 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=295 & (((messages [ (proc5 - 1) % NumProcess ] =messages [ proc5 ] ) & (leader_PROCESS_PROCESS_PROCESS_PROCESS=messages [ proc5 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=281 & !(((leader_PROCESS_PROCESS_PROCESS_PROCESS=processes [ proc5 ] ) & (messages [ (proc5 - 1) % NumProcess ] =processes [ proc5 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=281 & (((leader_PROCESS_PROCESS_PROCESS_PROCESS=processes [ proc5 ] ) & (messages [ (proc5 - 1) % NumProcess ] =processes [ proc5 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=267 & !((messages [ (proc5 - 1) % NumProcess ] =processes [ proc5 ] )) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=267 & ((messages [ (proc5 - 1) % NumProcess ] =processes [ proc5 ] )) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=253 & !((messages [ (proc5 - 1) % NumProcess ] =messages [ proc5 ] )) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=253 & ((messages [ (proc5 - 1) % NumProcess ] =messages [ proc5 ] )) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=239 & !(((messages [ (proc4 - 1) % NumProcess ] =messages [ proc4 ] ) & (leader_PROCESS_PROCESS_PROCESS=messages [ proc4 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=239 & (((messages [ (proc4 - 1) % NumProcess ] =messages [ proc4 ] ) & (leader_PROCESS_PROCESS_PROCESS=messages [ proc4 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=225 & !(((leader_PROCESS_PROCESS_PROCESS=processes [ proc4 ] ) & (messages [ (proc4 - 1) % NumProcess ] =processes [ proc4 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=225 & (((leader_PROCESS_PROCESS_PROCESS=processes [ proc4 ] ) & (messages [ (proc4 - 1) % NumProcess ] =processes [ proc4 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=211 & !((messages [ (proc4 - 1) % NumProcess ] =processes [ proc4 ] )) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=211 & ((messages [ (proc4 - 1) % NumProcess ] =processes [ proc4 ] )) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=197 & !((messages [ (proc4 - 1) % NumProcess ] =messages [ proc4 ] )) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=197 & ((messages [ (proc4 - 1) % NumProcess ] =messages [ proc4 ] )) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=183 & !(((messages [ (proc3 - 1) % NumProcess ] =messages [ proc3 ] ) & (leader_PROCESS_PROCESS=messages [ proc3 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=183 & (((messages [ (proc3 - 1) % NumProcess ] =messages [ proc3 ] ) & (leader_PROCESS_PROCESS=messages [ proc3 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=169 & !(((leader_PROCESS_PROCESS=processes [ proc3 ] ) & (messages [ (proc3 - 1) % NumProcess ] =processes [ proc3 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=169 & (((leader_PROCESS_PROCESS=processes [ proc3 ] ) & (messages [ (proc3 - 1) % NumProcess ] =processes [ proc3 ] ))) & !fail_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=155 & !((messages [ (proc3 - 1) % NumProcess ] =processes [ proc3 ] )) & !fail_1_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=155 & ((messages [ (proc3 - 1) % NumProcess ] =processes [ proc3 ] )) & !fail_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=141 & !((messages [ (proc3 - 1) % NumProcess ] =messages [ proc3 ] )) & !fail_1_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=141 & ((messages [ (proc3 - 1) % NumProcess ] =messages [ proc3 ] )) & !fail_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=127 & !(((messages [ (proc2 - 1) % NumProcess ] =messages [ proc2 ] ) & (leader_PROCESS=messages [ proc2 ] ))) & !fail_1_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=127 & (((messages [ (proc2 - 1) % NumProcess ] =messages [ proc2 ] ) & (leader_PROCESS=messages [ proc2 ] ))) & !fail_1_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=113 & !(((leader_PROCESS=processes [ proc2 ] ) & (messages [ (proc2 - 1) % NumProcess ] =processes [ proc2 ] ))) & !fail_1_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=113 & (((leader_PROCESS=processes [ proc2 ] ) & (messages [ (proc2 - 1) % NumProcess ] =processes [ proc2 ] ))) & !fail_1_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=99 & !((messages [ (proc2 - 1) % NumProcess ] =processes [ proc2 ] )) & !fail_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=99 & ((messages [ (proc2 - 1) % NumProcess ] =processes [ proc2 ] )) & !fail_1_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=85 & !((messages [ (proc2 - 1) % NumProcess ] =messages [ proc2 ] )) & !fail_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=85 & ((messages [ (proc2 - 1) % NumProcess ] =messages [ proc2 ] )) & !fail_1_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=71 & !(((messages [ (proc1 - 1) % NumProcess ] =messages [ proc1 ] ) & (leader=messages [ proc1 ] ))) & !fail_1_1_1_1
==>
begin
  fail_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=71 & (((messages [ (proc1 - 1) % NumProcess ] =messages [ proc1 ] ) & (leader=messages [ proc1 ] ))) & !fail_1_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=57 & !(((leader=processes [ proc1 ] ) & (messages [ (proc1 - 1) % NumProcess ] =processes [ proc1 ] ))) & !fail_1_1_1
==>
begin
  fail_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=57 & (((leader=processes [ proc1 ] ) & (messages [ (proc1 - 1) % NumProcess ] =processes [ proc1 ] ))) & !fail_1_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=43 & !((messages [ (proc1 - 1) % NumProcess ] =processes [ proc1 ] )) & !fail_1_1
==>
begin
  fail_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=43 & ((messages [ (proc1 - 1) % NumProcess ] =processes [ proc1 ] )) & !fail_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=29 & !((messages [ (proc1 - 1) % NumProcess ] =messages [ proc1 ] )) & !fail_1
==>
begin
  fail_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=29 & ((messages [ (proc1 - 1) % NumProcess ] =messages [ proc1 ] )) & !fail_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=15 & !((messages [ NumProcess - 1 ] =processes [ 0 ] )) & !fail
==>
begin
  fail:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=15 & ((messages [ NumProcess - 1 ] =processes [ 0 ] )) & !fail
==>
begin
  PC:=2;
end;

Rule "INIT"
PC=2 & init=TRUE
==>
begin
  PC:=3;
  message_exist [ NumProcess - 1 ] :=election;
  init:=FALSE;
end;

Rule "RECEIVED_ELECTION_AND_I_AM_GREATER"
PC=2 & ((message_exist [ proc1 ] =election) & (messages [ proc1 ] >processes [ proc1 ] ))
==>
begin
  PC:=16;
  message_exist [ proc1 ] :=no_message;
  message_exist [ (proc1 - 1) % NumProcess ] :=election;
end;

Rule "RECEIVED_ELECTION_AND_I_AM_LESS"
PC=2 & ((message_exist [ proc1 ] =election) & (processes [ proc1 ] >messages [ proc1 ] ))
==>
begin
  PC:=30;
  message_exist [ proc1 ] :=no_message;
  message_exist [ (proc1 - 1) % NumProcess ] :=election;
end;

Rule "I_AM_THE_LEADER"
PC=2 & ((message_exist [ proc1 ] =election) & (processes [ proc1 ] =messages [ proc1 ] ))
==>
begin
  PC:=44;
  message_exist [ proc1 ] :=no_message;
  message_exist [ (proc1 - 1) % NumProcess ] :=elected;
end;

Rule "RECEIVED_ELECTED_AND_I_AM_THE_LEADER"
PC=2 & ((message_exist [ proc1 ] =elected) & (processes [ proc1 ] =messages [ proc1 ] ))
==>
begin
  message_exist [ proc1 ] :=no_message;
  message_exist [ (proc1 - 1) % NumProcess ] :=elected;
  messages [ (proc1 - 1) % NumProcess ] :=leader;
end;

Rule "RECEIVED_ELECTED_I_AM_NOT_THE_LEADER"
PC=2 & ((message_exist [ proc1 ] =elected) & (processes [ proc1 ] !=messages [ proc1 ] ))
==>
begin
  PC:=58;
  message_exist [ proc1 ] :=no_message;
  message_exist [ (proc1 - 1) % NumProcesses ] :=elected;
end;

Rule "RECEIVED_ELECTION_AND_I_AM_GREATER_PROCESS"
PC=2 & ((message_exist [ proc2 ] =election) & (messages [ proc2 ] >processes [ proc2 ] ))
==>
begin
  PC:=72;
  message_exist [ proc2 ] :=no_message;
  message_exist [ (proc2 - 1) % NumProcess ] :=election;
end;

Rule "RECEIVED_ELECTION_AND_I_AM_LESS_PROCESS"
PC=2 & ((message_exist [ proc2 ] =election) & (processes [ proc2 ] >messages [ proc2 ] ))
==>
begin
  PC:=86;
  message_exist [ proc2 ] :=no_message;
  message_exist [ (proc2 - 1) % NumProcess ] :=election;
end;

Rule "I_AM_THE_LEADER_PROCESS"
PC=2 & ((message_exist [ proc2 ] =election) & (processes [ proc2 ] =messages [ proc2 ] ))
==>
begin
  PC:=100;
  message_exist [ proc2 ] :=no_message;
  message_exist [ (proc2 - 1) % NumProcess ] :=elected;
end;

Rule "RECEIVED_ELECTED_AND_I_AM_THE_LEADER_PROCESS"
PC=2 & ((message_exist [ proc2 ] =elected) & (processes [ proc2 ] =messages [ proc2 ] ))
==>
begin
  message_exist [ proc2 ] :=no_message;
  message_exist [ (proc2 - 1) % NumProcess ] :=elected;
  messages [ (proc2 - 1) % NumProcess ] :=leader_PROCESS;
end;

Rule "RECEIVED_ELECTED_I_AM_NOT_THE_LEADER_PROCESS"
PC=2 & ((message_exist [ proc2 ] =elected) & (processes [ proc2 ] !=messages [ proc2 ] ))
==>
begin
  PC:=114;
  message_exist [ proc2 ] :=no_message;
  message_exist [ (proc2 - 1) % NumProcesses ] :=elected;
end;

Rule "RECEIVED_ELECTION_AND_I_AM_GREATER_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc3 ] =election) & (messages [ proc3 ] >processes [ proc3 ] ))
==>
begin
  PC:=128;
  message_exist [ proc3 ] :=no_message;
  message_exist [ (proc3 - 1) % NumProcess ] :=election;
end;

Rule "RECEIVED_ELECTION_AND_I_AM_LESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc3 ] =election) & (processes [ proc3 ] >messages [ proc3 ] ))
==>
begin
  PC:=142;
  message_exist [ proc3 ] :=no_message;
  message_exist [ (proc3 - 1) % NumProcess ] :=election;
end;

Rule "I_AM_THE_LEADER_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc3 ] =election) & (processes [ proc3 ] =messages [ proc3 ] ))
==>
begin
  PC:=156;
  message_exist [ proc3 ] :=no_message;
  message_exist [ (proc3 - 1) % NumProcess ] :=elected;
end;

Rule "RECEIVED_ELECTED_AND_I_AM_THE_LEADER_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc3 ] =elected) & (processes [ proc3 ] =messages [ proc3 ] ))
==>
begin
  message_exist [ proc3 ] :=no_message;
  message_exist [ (proc3 - 1) % NumProcess ] :=elected;
  messages [ (proc3 - 1) % NumProcess ] :=leader_PROCESS_PROCESS;
end;

Rule "RECEIVED_ELECTED_I_AM_NOT_THE_LEADER_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc3 ] =elected) & (processes [ proc3 ] !=messages [ proc3 ] ))
==>
begin
  PC:=170;
  message_exist [ proc3 ] :=no_message;
  message_exist [ (proc3 - 1) % NumProcesses ] :=elected;
end;

Rule "RECEIVED_ELECTION_AND_I_AM_GREATER_PROCESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc4 ] =election) & (messages [ proc4 ] >processes [ proc4 ] ))
==>
begin
  PC:=184;
  message_exist [ proc4 ] :=no_message;
  message_exist [ (proc4 - 1) % NumProcess ] :=election;
end;

Rule "RECEIVED_ELECTION_AND_I_AM_LESS_PROCESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc4 ] =election) & (processes [ proc4 ] >messages [ proc4 ] ))
==>
begin
  PC:=198;
  message_exist [ proc4 ] :=no_message;
  message_exist [ (proc4 - 1) % NumProcess ] :=election;
end;

Rule "I_AM_THE_LEADER_PROCESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc4 ] =election) & (processes [ proc4 ] =messages [ proc4 ] ))
==>
begin
  PC:=212;
  message_exist [ proc4 ] :=no_message;
  message_exist [ (proc4 - 1) % NumProcess ] :=elected;
end;

Rule "RECEIVED_ELECTED_AND_I_AM_THE_LEADER_PROCESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc4 ] =elected) & (processes [ proc4 ] =messages [ proc4 ] ))
==>
begin
  message_exist [ proc4 ] :=no_message;
  message_exist [ (proc4 - 1) % NumProcess ] :=elected;
  messages [ (proc4 - 1) % NumProcess ] :=leader_PROCESS_PROCESS_PROCESS;
end;

Rule "RECEIVED_ELECTED_I_AM_NOT_THE_LEADER_PROCESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc4 ] =elected) & (processes [ proc4 ] !=messages [ proc4 ] ))
==>
begin
  PC:=226;
  message_exist [ proc4 ] :=no_message;
  message_exist [ (proc4 - 1) % NumProcesses ] :=elected;
end;

Rule "RECEIVED_ELECTION_AND_I_AM_GREATER_PROCESS_PROCESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc5 ] =election) & (messages [ proc5 ] >processes [ proc5 ] ))
==>
begin
  PC:=240;
  message_exist [ proc5 ] :=no_message;
  message_exist [ (proc5 - 1) % NumProcess ] :=election;
end;

Rule "RECEIVED_ELECTION_AND_I_AM_LESS_PROCESS_PROCESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc5 ] =election) & (processes [ proc5 ] >messages [ proc5 ] ))
==>
begin
  PC:=254;
  message_exist [ proc5 ] :=no_message;
  message_exist [ (proc5 - 1) % NumProcess ] :=election;
end;

Rule "I_AM_THE_LEADER_PROCESS_PROCESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc5 ] =election) & (processes [ proc5 ] =messages [ proc5 ] ))
==>
begin
  PC:=268;
  message_exist [ proc5 ] :=no_message;
  message_exist [ (proc5 - 1) % NumProcess ] :=elected;
end;

Rule "RECEIVED_ELECTED_AND_I_AM_THE_LEADER_PROCESS_PROCESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc5 ] =elected) & (processes [ proc5 ] =messages [ proc5 ] ))
==>
begin
  message_exist [ proc5 ] :=no_message;
  message_exist [ (proc5 - 1) % NumProcess ] :=elected;
  messages [ (proc5 - 1) % NumProcess ] :=leader_PROCESS_PROCESS_PROCESS_PROCESS;
end;

Rule "RECEIVED_ELECTED_I_AM_NOT_THE_LEADER_PROCESS_PROCESS_PROCESS_PROCESS"
PC=2 & ((message_exist [ proc5 ] =elected) & (processes [ proc5 ] !=messages [ proc5 ] ))
==>
begin
  PC:=282;
  message_exist [ proc5 ] :=no_message;
  message_exist [ (proc5 - 1) % NumProcesses ] :=elected;
end;

startstate
begin
  proc5:=4;
  proc4:=3;
  proc3:=2;
  proc2:=1;
  proc1:=0;
  leader_PROCESS_PROCESS_PROCESS_PROCESS:=-1;
  leader_PROCESS_PROCESS_PROCESS:=-1;
  leader_PROCESS_PROCESS:=-1;
  leader_PROCESS:=-1;
  leader:=-1;
  init:=TRUE;
  PC:=0;
  fail:=FALSE;
  fail_1:=FALSE;
  fail_1_1:=FALSE;
  fail_1_1_1:=FALSE;
  fail_1_1_1_1:=FALSE;
  fail_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
  fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
  for i_1:= 0 to NumProcess-1 Do
	  processes[i_1]:=0
	endfor;
  for i_1:= 0 to NumProcess-1 Do
	  messages[i_1]:=0
	endfor;
  for i_1:= 0 to NumProcess-1 Do
	  message_exist[i_1]:=no_message
	endfor;
end;