const
	MININT	:	-32768;
	MAXINT	:	32767;
type
	T#user#state	:	enum { idle,entering,critical,exiting };
var
	fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_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_1_1_1_1_1_1_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_1_1_1_1_1_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_1_1_1_1_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_1_1_1_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_1_1_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_1_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_1_1_1	:	BOOLEAN;
	fail_1_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_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;
	__init	:	BOOLEAN;
	__init_v#user#state	:	BOOLEAN;
	__init_v#user#semaphore	:	BOOLEAN;
	state	:	T#user#state;
	__init_v#user#state_v#user#state	:	BOOLEAN;
	__init_v#user#semaphore_v#user#semaphore	:	BOOLEAN;
	state_user	:	T#user#state;
	semaphore	:	BOOLEAN;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable state */ 
Ruleset i : T#user#state Do
Rule 
PC=0 | PC=8 | PC=17 | PC=26 | PC=35 | PC=44 | PC=53 | PC=62 | PC=71 | PC=80 | PC=89 | PC=98 | PC=107 | PC=116 | PC=125 | PC=134 | PC=143 | PC=152 | PC=161 | PC=170 | PC=179 | PC=188 | PC=197 | PC=206 | PC=215 | PC=224 | PC=233 | PC=242 | PC=251 | PC=260 | PC=269 | PC=278 | PC=287 | PC=296 | PC=305 | PC=314 | PC=323 | PC=332 | PC=341 | PC=350 | PC=359 | PC=368 | PC=377 | PC=386 | PC=395 | PC=404 | PC=413 | PC=422 | PC=431 | PC=440 | PC=449
==>
begin
  state:=i;
  if PC=449 then
    PC:=450
  end;
  if PC=440 then
    PC:=441
  end;
  if PC=431 then
    PC:=432
  end;
  if PC=422 then
    PC:=423
  end;
  if PC=413 then
    PC:=414
  end;
  if PC=404 then
    PC:=405
  end;
  if PC=395 then
    PC:=396
  end;
  if PC=386 then
    PC:=387
  end;
  if PC=377 then
    PC:=378
  end;
  if PC=368 then
    PC:=369
  end;
  if PC=359 then
    PC:=360
  end;
  if PC=350 then
    PC:=351
  end;
  if PC=341 then
    PC:=342
  end;
  if PC=332 then
    PC:=333
  end;
  if PC=323 then
    PC:=324
  end;
  if PC=314 then
    PC:=315
  end;
  if PC=305 then
    PC:=306
  end;
  if PC=296 then
    PC:=297
  end;
  if PC=287 then
    PC:=288
  end;
  if PC=278 then
    PC:=279
  end;
  if PC=269 then
    PC:=270
  end;
  if PC=260 then
    PC:=261
  end;
  if PC=251 then
    PC:=252
  end;
  if PC=242 then
    PC:=243
  end;
  if PC=233 then
    PC:=234
  end;
  if PC=224 then
    PC:=225
  end;
  if PC=215 then
    PC:=216
  end;
  if PC=206 then
    PC:=207
  end;
  if PC=197 then
    PC:=198
  end;
  if PC=188 then
    PC:=189
  end;
  if PC=179 then
    PC:=180
  end;
  if PC=170 then
    PC:=171
  end;
  if PC=161 then
    PC:=162
  end;
  if PC=152 then
    PC:=153
  end;
  if PC=143 then
    PC:=144
  end;
  if PC=134 then
    PC:=135
  end;
  if PC=125 then
    PC:=126
  end;
  if PC=116 then
    PC:=117
  end;
  if PC=107 then
    PC:=108
  end;
  if PC=98 then
    PC:=99
  end;
  if PC=89 then
    PC:=90
  end;
  if PC=80 then
    PC:=81
  end;
  if PC=71 then
    PC:=72
  end;
  if PC=62 then
    PC:=63
  end;
  if PC=53 then
    PC:=54
  end;
  if PC=44 then
    PC:=45
  end;
  if PC=35 then
    PC:=36
  end;
  if PC=26 then
    PC:=27
  end;
  if PC=17 then
    PC:=18
  end;
  if PC=8 then
    PC:=9
  end;
  if PC=0 then
    PC:=1
  end;
end;
end;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable state_user */ 
Ruleset i : T#user#state Do
Rule 
PC=1 | PC=5 | PC=14 | PC=23 | PC=32 | PC=41 | PC=50 | PC=59 | PC=68 | PC=77 | PC=86 | PC=95 | PC=104 | PC=113 | PC=122 | PC=131 | PC=140 | PC=149 | PC=158 | PC=167 | PC=176 | PC=185 | PC=194 | PC=203 | PC=212 | PC=221 | PC=230 | PC=239 | PC=248 | PC=257 | PC=266 | PC=275 | PC=284 | PC=293 | PC=302 | PC=311 | PC=320 | PC=329 | PC=338 | PC=347 | PC=356 | PC=365 | PC=374 | PC=383 | PC=392 | PC=401 | PC=410 | PC=419 | PC=428 | PC=437 | PC=446
==>
begin
  state_user:=i;
  if PC=446 then
    PC:=447
  end;
  if PC=437 then
    PC:=438
  end;
  if PC=428 then
    PC:=429
  end;
  if PC=419 then
    PC:=420
  end;
  if PC=410 then
    PC:=411
  end;
  if PC=401 then
    PC:=402
  end;
  if PC=392 then
    PC:=393
  end;
  if PC=383 then
    PC:=384
  end;
  if PC=374 then
    PC:=375
  end;
  if PC=365 then
    PC:=366
  end;
  if PC=356 then
    PC:=357
  end;
  if PC=347 then
    PC:=348
  end;
  if PC=338 then
    PC:=339
  end;
  if PC=329 then
    PC:=330
  end;
  if PC=320 then
    PC:=321
  end;
  if PC=311 then
    PC:=312
  end;
  if PC=302 then
    PC:=303
  end;
  if PC=293 then
    PC:=294
  end;
  if PC=284 then
    PC:=285
  end;
  if PC=275 then
    PC:=276
  end;
  if PC=266 then
    PC:=267
  end;
  if PC=257 then
    PC:=258
  end;
  if PC=248 then
    PC:=249
  end;
  if PC=239 then
    PC:=240
  end;
  if PC=230 then
    PC:=231
  end;
  if PC=221 then
    PC:=222
  end;
  if PC=212 then
    PC:=213
  end;
  if PC=203 then
    PC:=204
  end;
  if PC=194 then
    PC:=195
  end;
  if PC=185 then
    PC:=186
  end;
  if PC=176 then
    PC:=177
  end;
  if PC=167 then
    PC:=168
  end;
  if PC=158 then
    PC:=159
  end;
  if PC=149 then
    PC:=150
  end;
  if PC=140 then
    PC:=141
  end;
  if PC=131 then
    PC:=132
  end;
  if PC=122 then
    PC:=123
  end;
  if PC=113 then
    PC:=114
  end;
  if PC=104 then
    PC:=105
  end;
  if PC=95 then
    PC:=96
  end;
  if PC=86 then
    PC:=87
  end;
  if PC=77 then
    PC:=78
  end;
  if PC=68 then
    PC:=69
  end;
  if PC=59 then
    PC:=60
  end;
  if PC=50 then
    PC:=51
  end;
  if PC=41 then
    PC:=42
  end;
  if PC=32 then
    PC:=33
  end;
  if PC=23 then
    PC:=24
  end;
  if PC=14 then
    PC:=15
  end;
  if PC=5 then
    PC:=6
  end;
  if PC=1 then
    PC:=2
  end;
end;
end;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable semaphore */ 
Ruleset i : BOOLEAN Do
Rule 
PC=2 | PC=4 | PC=13 | PC=22 | PC=31 | PC=40 | PC=49 | PC=58 | PC=67 | PC=76 | PC=85 | PC=94 | PC=103 | PC=112 | PC=121 | PC=130 | PC=139 | PC=148 | PC=157 | PC=166 | PC=175 | PC=184 | PC=193 | PC=202 | PC=211 | PC=220 | PC=229 | PC=238 | PC=247 | PC=256 | PC=265 | PC=274 | PC=283 | PC=292 | PC=301 | PC=310 | PC=319 | PC=328 | PC=337 | PC=346 | PC=355 | PC=364 | PC=373 | PC=382 | PC=391 | PC=400 | PC=409 | PC=418 | PC=427 | PC=436 | PC=445
==>
begin
  semaphore:=i;
  if PC=445 then
    PC:=446
  end;
  if PC=436 then
    PC:=437
  end;
  if PC=427 then
    PC:=428
  end;
  if PC=418 then
    PC:=419
  end;
  if PC=409 then
    PC:=410
  end;
  if PC=400 then
    PC:=401
  end;
  if PC=391 then
    PC:=392
  end;
  if PC=382 then
    PC:=383
  end;
  if PC=373 then
    PC:=374
  end;
  if PC=364 then
    PC:=365
  end;
  if PC=355 then
    PC:=356
  end;
  if PC=346 then
    PC:=347
  end;
  if PC=337 then
    PC:=338
  end;
  if PC=328 then
    PC:=329
  end;
  if PC=319 then
    PC:=320
  end;
  if PC=310 then
    PC:=311
  end;
  if PC=301 then
    PC:=302
  end;
  if PC=292 then
    PC:=293
  end;
  if PC=283 then
    PC:=284
  end;
  if PC=274 then
    PC:=275
  end;
  if PC=265 then
    PC:=266
  end;
  if PC=256 then
    PC:=257
  end;
  if PC=247 then
    PC:=248
  end;
  if PC=238 then
    PC:=239
  end;
  if PC=229 then
    PC:=230
  end;
  if PC=220 then
    PC:=221
  end;
  if PC=211 then
    PC:=212
  end;
  if PC=202 then
    PC:=203
  end;
  if PC=193 then
    PC:=194
  end;
  if PC=184 then
    PC:=185
  end;
  if PC=175 then
    PC:=176
  end;
  if PC=166 then
    PC:=167
  end;
  if PC=157 then
    PC:=158
  end;
  if PC=148 then
    PC:=149
  end;
  if PC=139 then
    PC:=140
  end;
  if PC=130 then
    PC:=131
  end;
  if PC=121 then
    PC:=122
  end;
  if PC=112 then
    PC:=113
  end;
  if PC=103 then
    PC:=104
  end;
  if PC=94 then
    PC:=95
  end;
  if PC=85 then
    PC:=86
  end;
  if PC=76 then
    PC:=77
  end;
  if PC=67 then
    PC:=68
  end;
  if PC=58 then
    PC:=59
  end;
  if PC=49 then
    PC:=50
  end;
  if PC=40 then
    PC:=41
  end;
  if PC=31 then
    PC:=32
  end;
  if PC=22 then
    PC:=23
  end;
  if PC=13 then
    PC:=14
  end;
  if PC=4 then
    PC:=5
  end;
  if PC=2 then
    PC:=3
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to __init_v#user#semaphore_v#user#semaphore that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : BOOLEAN Do
Rule 
PC=6 | PC=15 | PC=24 | PC=33 | PC=42 | PC=51 | PC=60 | PC=69 | PC=78 | PC=87 | PC=96 | PC=105 | PC=114 | PC=123 | PC=132 | PC=141 | PC=150 | PC=159 | PC=168 | PC=177 | PC=186 | PC=195 | PC=204 | PC=213 | PC=222 | PC=231 | PC=240 | PC=249 | PC=258 | PC=267 | PC=276 | PC=285 | PC=294 | PC=303 | PC=312 | PC=321 | PC=330 | PC=339 | PC=348 | PC=357 | PC=366 | PC=375 | PC=384 | PC=393 | PC=402 | PC=411 | PC=420 | PC=429 | PC=438 | PC=447
==>
begin
  __init_v#user#semaphore_v#user#semaphore:=i;
  if PC=447 then
    PC:=448
  end;
  if PC=438 then
    PC:=439
  end;
  if PC=429 then
    PC:=430
  end;
  if PC=420 then
    PC:=421
  end;
  if PC=411 then
    PC:=412
  end;
  if PC=402 then
    PC:=403
  end;
  if PC=393 then
    PC:=394
  end;
  if PC=384 then
    PC:=385
  end;
  if PC=375 then
    PC:=376
  end;
  if PC=366 then
    PC:=367
  end;
  if PC=357 then
    PC:=358
  end;
  if PC=348 then
    PC:=349
  end;
  if PC=339 then
    PC:=340
  end;
  if PC=330 then
    PC:=331
  end;
  if PC=321 then
    PC:=322
  end;
  if PC=312 then
    PC:=313
  end;
  if PC=303 then
    PC:=304
  end;
  if PC=294 then
    PC:=295
  end;
  if PC=285 then
    PC:=286
  end;
  if PC=276 then
    PC:=277
  end;
  if PC=267 then
    PC:=268
  end;
  if PC=258 then
    PC:=259
  end;
  if PC=249 then
    PC:=250
  end;
  if PC=240 then
    PC:=241
  end;
  if PC=231 then
    PC:=232
  end;
  if PC=222 then
    PC:=223
  end;
  if PC=213 then
    PC:=214
  end;
  if PC=204 then
    PC:=205
  end;
  if PC=195 then
    PC:=196
  end;
  if PC=186 then
    PC:=187
  end;
  if PC=177 then
    PC:=178
  end;
  if PC=168 then
    PC:=169
  end;
  if PC=159 then
    PC:=160
  end;
  if PC=150 then
    PC:=151
  end;
  if PC=141 then
    PC:=142
  end;
  if PC=132 then
    PC:=133
  end;
  if PC=123 then
    PC:=124
  end;
  if PC=114 then
    PC:=115
  end;
  if PC=105 then
    PC:=106
  end;
  if PC=96 then
    PC:=97
  end;
  if PC=87 then
    PC:=88
  end;
  if PC=78 then
    PC:=79
  end;
  if PC=69 then
    PC:=70
  end;
  if PC=60 then
    PC:=61
  end;
  if PC=51 then
    PC:=52
  end;
  if PC=42 then
    PC:=43
  end;
  if PC=33 then
    PC:=34
  end;
  if PC=24 then
    PC:=25
  end;
  if PC=15 then
    PC:=16
  end;
  if PC=6 then
    PC:=7
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to __init_v#user#state_v#user#state that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : BOOLEAN Do
Rule 
PC=7 | PC=16 | PC=25 | PC=34 | PC=43 | PC=52 | PC=61 | PC=70 | PC=79 | PC=88 | PC=97 | PC=106 | PC=115 | PC=124 | PC=133 | PC=142 | PC=151 | PC=160 | PC=169 | PC=178 | PC=187 | PC=196 | PC=205 | PC=214 | PC=223 | PC=232 | PC=241 | PC=250 | PC=259 | PC=268 | PC=277 | PC=286 | PC=295 | PC=304 | PC=313 | PC=322 | PC=331 | PC=340 | PC=349 | PC=358 | PC=367 | PC=376 | PC=385 | PC=394 | PC=403 | PC=412 | PC=421 | PC=430 | PC=439 | PC=448
==>
begin
  __init_v#user#state_v#user#state:=i;
  if PC=448 then
    PC:=449
  end;
  if PC=439 then
    PC:=440
  end;
  if PC=430 then
    PC:=431
  end;
  if PC=421 then
    PC:=422
  end;
  if PC=412 then
    PC:=413
  end;
  if PC=403 then
    PC:=404
  end;
  if PC=394 then
    PC:=395
  end;
  if PC=385 then
    PC:=386
  end;
  if PC=376 then
    PC:=377
  end;
  if PC=367 then
    PC:=368
  end;
  if PC=358 then
    PC:=359
  end;
  if PC=349 then
    PC:=350
  end;
  if PC=340 then
    PC:=341
  end;
  if PC=331 then
    PC:=332
  end;
  if PC=322 then
    PC:=323
  end;
  if PC=313 then
    PC:=314
  end;
  if PC=304 then
    PC:=305
  end;
  if PC=295 then
    PC:=296
  end;
  if PC=286 then
    PC:=287
  end;
  if PC=277 then
    PC:=278
  end;
  if PC=268 then
    PC:=269
  end;
  if PC=259 then
    PC:=260
  end;
  if PC=250 then
    PC:=251
  end;
  if PC=241 then
    PC:=242
  end;
  if PC=232 then
    PC:=233
  end;
  if PC=223 then
    PC:=224
  end;
  if PC=214 then
    PC:=215
  end;
  if PC=205 then
    PC:=206
  end;
  if PC=196 then
    PC:=197
  end;
  if PC=187 then
    PC:=188
  end;
  if PC=178 then
    PC:=179
  end;
  if PC=169 then
    PC:=170
  end;
  if PC=160 then
    PC:=161
  end;
  if PC=151 then
    PC:=152
  end;
  if PC=142 then
    PC:=143
  end;
  if PC=133 then
    PC:=134
  end;
  if PC=124 then
    PC:=125
  end;
  if PC=115 then
    PC:=116
  end;
  if PC=106 then
    PC:=107
  end;
  if PC=97 then
    PC:=98
  end;
  if PC=88 then
    PC:=89
  end;
  if PC=79 then
    PC:=80
  end;
  if PC=70 then
    PC:=71
  end;
  if PC=61 then
    PC:=62
  end;
  if PC=52 then
    PC:=53
  end;
  if PC=43 then
    PC:=44
  end;
  if PC=34 then
    PC:=35
  end;
  if PC=25 then
    PC:=26
  end;
  if PC=16 then
    PC:=17
  end;
  if PC=7 then
    PC:=8
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to __init_v#user#semaphore that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : BOOLEAN Do
Rule 
PC=9 | PC=18 | PC=27 | PC=36 | PC=45 | PC=54 | PC=63 | PC=72 | PC=81 | PC=90 | PC=99 | PC=108 | PC=117 | PC=126 | PC=135 | PC=144 | PC=153 | PC=162 | PC=171 | PC=180 | PC=189 | PC=198 | PC=207 | PC=216 | PC=225 | PC=234 | PC=243 | PC=252 | PC=261 | PC=270 | PC=279 | PC=288 | PC=297 | PC=306 | PC=315 | PC=324 | PC=333 | PC=342 | PC=351 | PC=360 | PC=369 | PC=378 | PC=387 | PC=396 | PC=405 | PC=414 | PC=423 | PC=432 | PC=441 | PC=450
==>
begin
  __init_v#user#semaphore:=i;
  if PC=450 then
    PC:=451
  end;
  if PC=441 then
    PC:=442
  end;
  if PC=432 then
    PC:=433
  end;
  if PC=423 then
    PC:=424
  end;
  if PC=414 then
    PC:=415
  end;
  if PC=405 then
    PC:=406
  end;
  if PC=396 then
    PC:=397
  end;
  if PC=387 then
    PC:=388
  end;
  if PC=378 then
    PC:=379
  end;
  if PC=369 then
    PC:=370
  end;
  if PC=360 then
    PC:=361
  end;
  if PC=351 then
    PC:=352
  end;
  if PC=342 then
    PC:=343
  end;
  if PC=333 then
    PC:=334
  end;
  if PC=324 then
    PC:=325
  end;
  if PC=315 then
    PC:=316
  end;
  if PC=306 then
    PC:=307
  end;
  if PC=297 then
    PC:=298
  end;
  if PC=288 then
    PC:=289
  end;
  if PC=279 then
    PC:=280
  end;
  if PC=270 then
    PC:=271
  end;
  if PC=261 then
    PC:=262
  end;
  if PC=252 then
    PC:=253
  end;
  if PC=243 then
    PC:=244
  end;
  if PC=234 then
    PC:=235
  end;
  if PC=225 then
    PC:=226
  end;
  if PC=216 then
    PC:=217
  end;
  if PC=207 then
    PC:=208
  end;
  if PC=198 then
    PC:=199
  end;
  if PC=189 then
    PC:=190
  end;
  if PC=180 then
    PC:=181
  end;
  if PC=171 then
    PC:=172
  end;
  if PC=162 then
    PC:=163
  end;
  if PC=153 then
    PC:=154
  end;
  if PC=144 then
    PC:=145
  end;
  if PC=135 then
    PC:=136
  end;
  if PC=126 then
    PC:=127
  end;
  if PC=117 then
    PC:=118
  end;
  if PC=108 then
    PC:=109
  end;
  if PC=99 then
    PC:=100
  end;
  if PC=90 then
    PC:=91
  end;
  if PC=81 then
    PC:=82
  end;
  if PC=72 then
    PC:=73
  end;
  if PC=63 then
    PC:=64
  end;
  if PC=54 then
    PC:=55
  end;
  if PC=45 then
    PC:=46
  end;
  if PC=36 then
    PC:=37
  end;
  if PC=27 then
    PC:=28
  end;
  if PC=18 then
    PC:=19
  end;
  if PC=9 then
    PC:=10
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to __init_v#user#state that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : BOOLEAN Do
Rule 
PC=10 | PC=19 | PC=28 | PC=37 | PC=46 | PC=55 | PC=64 | PC=73 | PC=82 | PC=91 | PC=100 | PC=109 | PC=118 | PC=127 | PC=136 | PC=145 | PC=154 | PC=163 | PC=172 | PC=181 | PC=190 | PC=199 | PC=208 | PC=217 | PC=226 | PC=235 | PC=244 | PC=253 | PC=262 | PC=271 | PC=280 | PC=289 | PC=298 | PC=307 | PC=316 | PC=325 | PC=334 | PC=343 | PC=352 | PC=361 | PC=370 | PC=379 | PC=388 | PC=397 | PC=406 | PC=415 | PC=424 | PC=433 | PC=442 | PC=451
==>
begin
  __init_v#user#state:=i;
  if PC=451 then
    PC:=452
  end;
  if PC=442 then
    PC:=443
  end;
  if PC=433 then
    PC:=434
  end;
  if PC=424 then
    PC:=425
  end;
  if PC=415 then
    PC:=416
  end;
  if PC=406 then
    PC:=407
  end;
  if PC=397 then
    PC:=398
  end;
  if PC=388 then
    PC:=389
  end;
  if PC=379 then
    PC:=380
  end;
  if PC=370 then
    PC:=371
  end;
  if PC=361 then
    PC:=362
  end;
  if PC=352 then
    PC:=353
  end;
  if PC=343 then
    PC:=344
  end;
  if PC=334 then
    PC:=335
  end;
  if PC=325 then
    PC:=326
  end;
  if PC=316 then
    PC:=317
  end;
  if PC=307 then
    PC:=308
  end;
  if PC=298 then
    PC:=299
  end;
  if PC=289 then
    PC:=290
  end;
  if PC=280 then
    PC:=281
  end;
  if PC=271 then
    PC:=272
  end;
  if PC=262 then
    PC:=263
  end;
  if PC=253 then
    PC:=254
  end;
  if PC=244 then
    PC:=245
  end;
  if PC=235 then
    PC:=236
  end;
  if PC=226 then
    PC:=227
  end;
  if PC=217 then
    PC:=218
  end;
  if PC=208 then
    PC:=209
  end;
  if PC=199 then
    PC:=200
  end;
  if PC=190 then
    PC:=191
  end;
  if PC=181 then
    PC:=182
  end;
  if PC=172 then
    PC:=173
  end;
  if PC=163 then
    PC:=164
  end;
  if PC=154 then
    PC:=155
  end;
  if PC=145 then
    PC:=146
  end;
  if PC=136 then
    PC:=137
  end;
  if PC=127 then
    PC:=128
  end;
  if PC=118 then
    PC:=119
  end;
  if PC=109 then
    PC:=110
  end;
  if PC=100 then
    PC:=101
  end;
  if PC=91 then
    PC:=92
  end;
  if PC=82 then
    PC:=83
  end;
  if PC=73 then
    PC:=74
  end;
  if PC=64 then
    PC:=65
  end;
  if PC=55 then
    PC:=56
  end;
  if PC=46 then
    PC:=47
  end;
  if PC=37 then
    PC:=38
  end;
  if PC=28 then
    PC:=29
  end;
  if PC=19 then
    PC:=20
  end;
  if PC=10 then
    PC:=11
  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=11 | PC=20 | PC=29 | PC=38 | PC=47 | PC=56 | PC=65 | PC=74 | PC=83 | PC=92 | PC=101 | PC=110 | PC=119 | PC=128 | PC=137 | PC=146 | PC=155 | PC=164 | PC=173 | PC=182 | PC=191 | PC=200 | PC=209 | PC=218 | PC=227 | PC=236 | PC=245 | PC=254 | PC=263 | PC=272 | PC=281 | PC=290 | PC=299 | PC=308 | PC=317 | PC=326 | PC=335 | PC=344 | PC=353 | PC=362 | PC=371 | PC=380 | PC=389 | PC=398 | PC=407 | PC=416 | PC=425 | PC=434 | PC=443 | PC=452
==>
begin
  __init:=i;
  if PC=452 then
    PC:=453
  end;
  if PC=443 then
    PC:=444
  end;
  if PC=434 then
    PC:=435
  end;
  if PC=425 then
    PC:=426
  end;
  if PC=416 then
    PC:=417
  end;
  if PC=407 then
    PC:=408
  end;
  if PC=398 then
    PC:=399
  end;
  if PC=389 then
    PC:=390
  end;
  if PC=380 then
    PC:=381
  end;
  if PC=371 then
    PC:=372
  end;
  if PC=362 then
    PC:=363
  end;
  if PC=353 then
    PC:=354
  end;
  if PC=344 then
    PC:=345
  end;
  if PC=335 then
    PC:=336
  end;
  if PC=326 then
    PC:=327
  end;
  if PC=317 then
    PC:=318
  end;
  if PC=308 then
    PC:=309
  end;
  if PC=299 then
    PC:=300
  end;
  if PC=290 then
    PC:=291
  end;
  if PC=281 then
    PC:=282
  end;
  if PC=272 then
    PC:=273
  end;
  if PC=263 then
    PC:=264
  end;
  if PC=254 then
    PC:=255
  end;
  if PC=245 then
    PC:=246
  end;
  if PC=236 then
    PC:=237
  end;
  if PC=227 then
    PC:=228
  end;
  if PC=218 then
    PC:=219
  end;
  if PC=209 then
    PC:=210
  end;
  if PC=200 then
    PC:=201
  end;
  if PC=191 then
    PC:=192
  end;
  if PC=182 then
    PC:=183
  end;
  if PC=173 then
    PC:=174
  end;
  if PC=164 then
    PC:=165
  end;
  if PC=155 then
    PC:=156
  end;
  if PC=146 then
    PC:=147
  end;
  if PC=137 then
    PC:=138
  end;
  if PC=128 then
    PC:=129
  end;
  if PC=119 then
    PC:=120
  end;
  if PC=110 then
    PC:=111
  end;
  if PC=101 then
    PC:=102
  end;
  if PC=92 then
    PC:=93
  end;
  if PC=83 then
    PC:=84
  end;
  if PC=74 then
    PC:=75
  end;
  if PC=65 then
    PC:=66
  end;
  if PC=56 then
    PC:=57
  end;
  if PC=47 then
    PC:=48
  end;
  if PC=38 then
    PC:=39
  end;
  if PC=29 then
    PC:=30
  end;
  if PC=20 then
    PC:=21
  end;
  if PC=11 then
    PC:=12
  end;
end;
end;

/* Rule created during translating relation */ 
Rule 
PC=453 & !((state=idle) & !__init_v#user#state_v#user#state & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1_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=453 & ((state=idle) & !__init_v#user#state_v#user#state & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=444 & !((state=idle) & !__init_v#user#state_v#user#state & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_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=444 & ((state=idle) & !__init_v#user#state_v#user#state & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=435 & !((state=idle) & !__init_v#user#state_v#user#state & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_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=435 & ((state=idle) & !__init_v#user#state_v#user#state & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=426 & !((state=idle) & !__init_v#user#state_v#user#state & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_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=426 & ((state=idle) & !__init_v#user#state_v#user#state & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=417 & !(state=idle | state=entering & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_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=417 & (state=idle | state=entering & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=408 & !(state=idle | state=entering & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_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=408 & (state=idle | state=entering & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=399 & !(state=idle | state=entering & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_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=399 & (state=idle | state=entering & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=390 & !(state=idle | state=entering & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_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=390 & (state=idle | state=entering & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=381 & !(state=critical & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_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=381 & (state=critical & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=372 & !(state=critical & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_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=372 & (state=critical & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=363 & !(state=critical & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_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=363 & (state=critical & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=354 & !(state=critical & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_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=354 & (state=critical & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=345 & !(state=critical | state=exiting & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_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=345 & (state=critical | state=exiting & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=336 & !(state=critical | state=exiting & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_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=336 & (state=critical | state=exiting & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=327 & !(state=critical | state=exiting & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=327 & (state=critical | state=exiting & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=318 & !(state=critical | state=exiting & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=318 & (state=critical | state=exiting & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=309 & !(state=idle & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=309 & (state=idle & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=300 & !(state=idle & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=300 & (state=idle & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=291 & !(state=idle & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=291 & (state=idle & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=282 & !(state=idle & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=282 & (state=idle & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=273 & !(state=state & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=273 & (state=state & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=264 & !(state=state & semaphore=1) & !fail_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=264 & (state=state & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=255 & !(state=state & semaphore=0) & !fail_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=255 & (state=state & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=246 & !(state=state & semaphore=semaphore) & !fail_1_1_1_1_1_1_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_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=246 & (state=state & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=237 & !((state=idle) & !__init_v#user#state & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !fail_1_1_1_1_1_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_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=237 & ((state=idle) & !__init_v#user#state & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=228 & !((state=idle) & !__init_v#user#state & semaphore=1) & !fail_1_1_1_1_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_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=228 & ((state=idle) & !__init_v#user#state & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=219 & !((state=idle) & !__init_v#user#state & semaphore=0) & !fail_1_1_1_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_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=219 & ((state=idle) & !__init_v#user#state & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=210 & !((state=idle) & !__init_v#user#state & semaphore=semaphore) & !fail_1_1_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_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=210 & ((state=idle) & !__init_v#user#state & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=201 & !(state=idle | state=entering & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !fail_1_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_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=201 & (state=idle | state=entering & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=192 & !(state=idle | state=entering & semaphore=1) & !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=192 & (state=idle | state=entering & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=183 & !(state=idle | state=entering & semaphore=0) & !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=183 & (state=idle | state=entering & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=174 & !(state=idle | state=entering & semaphore=semaphore) & !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=174 & (state=idle | state=entering & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=165 & !(state=critical & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !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=165 & (state=critical & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=156 & !(state=critical & semaphore=1) & !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=156 & (state=critical & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=147 & !(state=critical & semaphore=0) & !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=147 & (state=critical & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=138 & !(state=critical & semaphore=semaphore) & !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=138 & (state=critical & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=129 & !(state=critical | state=exiting & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !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=129 & (state=critical | state=exiting & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=120 & !(state=critical | state=exiting & semaphore=1) & !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=120 & (state=critical | state=exiting & semaphore=1) & !fail_1_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=111 & !(state=critical | state=exiting & semaphore=0) & !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=111 & (state=critical | state=exiting & semaphore=0) & !fail_1_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=102 & !(state=critical | state=exiting & semaphore=semaphore) & !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=102 & (state=critical | state=exiting & semaphore=semaphore) & !fail_1_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=93 & !(state=idle & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !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=93 & (state=idle & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !fail_1_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=84 & !(state=idle & semaphore=1) & !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=84 & (state=idle & semaphore=1) & !fail_1_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=75 & !(state=idle & semaphore=0) & !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=75 & (state=idle & semaphore=0) & !fail_1_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=66 & !(state=idle & semaphore=semaphore) & !fail_1_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=66 & (state=idle & semaphore=semaphore) & !fail_1_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=57 & !(state=state & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !fail_1_1_1_1_1
==>
begin
  fail_1_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=57 & (state=state & (semaphore=FALSE | semaphore=TRUE) & !__init_v#user#semaphore) & !fail_1_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=48 & !(state=state & semaphore=1) & !fail_1_1_1_1
==>
begin
  fail_1_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=48 & (state=state & semaphore=1) & !fail_1_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=39 & !(state=state & semaphore=0) & !fail_1_1_1
==>
begin
  fail_1_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=39 & (state=state & semaphore=0) & !fail_1_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=30 & !(state=state & semaphore=semaphore) & !fail_1_1
==>
begin
  fail_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=30 & (state=state & semaphore=semaphore) & !fail_1_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=21 & !((semaphore=0) & !__init) & !fail_1
==>
begin
  fail_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=21 & ((semaphore=0) & !__init) & !fail_1
==>
begin
  PC:=3;
end;

/* Rule created during translating relation */ 
Rule 
PC=12 & !(semaphore=FALSE | semaphore=TRUE) & !fail
==>
begin
  fail:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=12 & (semaphore=FALSE | semaphore=TRUE) & !fail
==>
begin
  PC:=3;
end;

Rule "T_semaphore_1"
PC=3 & !__init
==>
begin
end;

Rule "T_semaphore_0"
PC=3 & __init
==>
begin
end;

Rule "T_state_5_T_semaphore_3"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & !(state=exiting) & !__init_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_5_T_semaphore_2"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & !(state=exiting) & !__init_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_5_T_semaphore_1"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & !(state=exiting) & !__init_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_5_T_semaphore_0"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & !(state=exiting) & __init_v#user#semaphore
==>
begin
end;

Rule "T_state_4_T_semaphore_3"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & (state=exiting) & !__init_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_4_T_semaphore_2"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & (state=exiting) & !__init_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_4_T_semaphore_1"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & (state=exiting) & !__init_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_4_T_semaphore_0"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & (state=exiting) & __init_v#user#semaphore
==>
begin
end;

Rule "T_state_3_T_semaphore_3"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & (state=critical) & !__init_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_3_T_semaphore_2"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & (state=critical) & !__init_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_3_T_semaphore_1"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & (state=critical) & !__init_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_3_T_semaphore_0"
PC=3 & !__init_v#user#state & !(state=idle) & !(state=entering & !semaphore) & (state=critical) & __init_v#user#semaphore
==>
begin
end;

Rule "T_state_2_T_semaphore_3"
PC=3 & !__init_v#user#state & !(state=idle) & (state=entering & !semaphore) & !__init_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_2_T_semaphore_2"
PC=3 & !__init_v#user#state & !(state=idle) & (state=entering & !semaphore) & !__init_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_2_T_semaphore_1"
PC=3 & !__init_v#user#state & !(state=idle) & (state=entering & !semaphore) & !__init_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_2_T_semaphore_0"
PC=3 & !__init_v#user#state & !(state=idle) & (state=entering & !semaphore) & __init_v#user#semaphore
==>
begin
end;

Rule "T_state_1_T_semaphore_3"
PC=3 & !__init_v#user#state & (state=idle) & !__init_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_1_T_semaphore_2"
PC=3 & !__init_v#user#state & (state=idle) & !__init_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_1_T_semaphore_1"
PC=3 & !__init_v#user#state & (state=idle) & !__init_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_1_T_semaphore_0"
PC=3 & !__init_v#user#state & (state=idle) & __init_v#user#semaphore
==>
begin
end;

Rule "T_state_0_T_semaphore_3"
PC=3 & __init_v#user#state & !__init_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_0_T_semaphore_2"
PC=3 & __init_v#user#state & !__init_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_0_T_semaphore_1"
PC=3 & __init_v#user#state & !__init_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_0_T_semaphore_0"
PC=3 & __init_v#user#state & __init_v#user#semaphore
==>
begin
end;

Rule "T_state_5_T_semaphore_3_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & !(state=exiting) & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_5_T_semaphore_2_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & !(state=exiting) & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_5_T_semaphore_1_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & !(state=exiting) & !__init_v#user#semaphore_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_5_T_semaphore_0_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & !(state=exiting) & __init_v#user#semaphore_v#user#semaphore
==>
begin
end;

Rule "T_state_4_T_semaphore_3_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & (state=exiting) & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_4_T_semaphore_2_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & (state=exiting) & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_4_T_semaphore_1_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & (state=exiting) & !__init_v#user#semaphore_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_4_T_semaphore_0_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & !(state=critical) & (state=exiting) & __init_v#user#semaphore_v#user#semaphore
==>
begin
end;

Rule "T_state_3_T_semaphore_3_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & (state=critical) & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_3_T_semaphore_2_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & (state=critical) & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_3_T_semaphore_1_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & (state=critical) & !__init_v#user#semaphore_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_3_T_semaphore_0_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & !(state=entering & !semaphore) & (state=critical) & __init_v#user#semaphore_v#user#semaphore
==>
begin
end;

Rule "T_state_2_T_semaphore_3_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & (state=entering & !semaphore) & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_2_T_semaphore_2_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & (state=entering & !semaphore) & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_2_T_semaphore_1_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & (state=entering & !semaphore) & !__init_v#user#semaphore_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_2_T_semaphore_0_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & !(state=idle) & (state=entering & !semaphore) & __init_v#user#semaphore_v#user#semaphore
==>
begin
end;

Rule "T_state_1_T_semaphore_3_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & (state=idle) & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_1_T_semaphore_2_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & (state=idle) & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_1_T_semaphore_1_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & (state=idle) & !__init_v#user#semaphore_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_1_T_semaphore_0_v#user#state_v#user#semaphore"
PC=3 & !__init_v#user#state_v#user#state & (state=idle) & __init_v#user#semaphore_v#user#semaphore
==>
begin
end;

Rule "T_state_0_T_semaphore_3_v#user#state_v#user#semaphore"
PC=3 & __init_v#user#state_v#user#state & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & !(state=exiting)
==>
begin
end;

Rule "T_state_0_T_semaphore_2_v#user#state_v#user#semaphore"
PC=3 & __init_v#user#state_v#user#state & !__init_v#user#semaphore_v#user#semaphore & !(state=entering) & (state=exiting)
==>
begin
end;

Rule "T_state_0_T_semaphore_1_v#user#state_v#user#semaphore"
PC=3 & __init_v#user#state_v#user#state & !__init_v#user#semaphore_v#user#semaphore & (state=entering)
==>
begin
end;

Rule "T_state_0_T_semaphore_0_v#user#state_v#user#semaphore"
PC=3 & __init_v#user#state_v#user#state & __init_v#user#semaphore_v#user#semaphore
==>
begin
end;

startstate
begin
  semaphore:=TRUE;
  state_user:=idle;
  __init_v#user#semaphore_v#user#semaphore:=TRUE;
  __init_v#user#state_v#user#state:=TRUE;
  state:=idle;
  __init_v#user#semaphore:=TRUE;
  __init_v#user#state:=TRUE;
  __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;
  fail_1_1_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_1_1:=FALSE;
  fail_1_1_1_1_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_1_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_1_1_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_1_1_1_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_1_1_1_1_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_1_1_1_1_1_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_1_1_1_1_1_1_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_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1_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_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1_1:=FALSE;
end;