Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / tests / cocospec / bacteriaPopulationStateflow_PP.lus @ 1e3ae41f

History | View | Annotate | Download (37.9 KB)

1
-- This file has been generated by CoCoSim2.
2

    
3
-- Compiler: Lustre compiler 2 (ToLustre.m)
4
-- Time: 28-Jun-2018 10:59:12
5
--external libraries
6
node int_to_bool (x: int)
7
returns(y:bool);
8
let
9
	 y= (x <> 0);
10
tel
11

    
12
--Simulink code
13

    
14

    
15

    
16

    
17

    
18

    
19

    
20
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/require3 pre Population = environmentCapacity/arrow
21
node arrow_2967_000 (initialvalue_1: bool;
22
nextvalue_1: bool;
23
__time_step:real;)
24
 returns (output_1: bool;);
25

    
26
var Memory_1: bool;Switch_1: bool;false_1: bool;
27
let
28
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
29
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
30
	false_1 = false;
31
	output_1 = Switch_1;
32
	
33
tel
34

    
35

    
36
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/require3 pre Population = environmentCapacity
37
node require3prePopulation_equal_environmentCapacity_2964_001 (environmentCapacity_1: real;
38
prePopulation_1: real;
39
__time_step:real;)
40
 returns (require_1: bool;);
41

    
42
var arrow_1: bool;equals_1: bool;true_1: bool;
43
let
44
	(arrow_1) = arrow_2967_000(true_1,
45
		equals_1,
46
		__time_step);
47
	equals_1 = prePopulation_1 = environmentCapacity_1;
48
	true_1 = true;
49
	require_1 = arrow_1;
50
	
51
tel
52

    
53

    
54

    
55
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/require2 pre Population > environmentCapacity
56
node require2prePopulation_environmentCapacity_2956_000 (environmentCapacity_1: real;
57
prePopulation_1: real;
58
__time_step:real;)
59
 returns (require_1: bool;);
60

    
61
var RelationalOperator_1: bool;
62
let
63
	RelationalOperator_1 = prePopulation_1 > environmentCapacity_1;
64
	require_1 = RelationalOperator_1;
65
	
66
tel
67

    
68

    
69

    
70
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/require1 pre Population < environmentCapacity
71
node require1prePopulation_environmentCapacity_2948_000 (environmentCapacity_1: real;
72
prePopulation_1: real;
73
__time_step:real;)
74
 returns (require_1: bool;);
75

    
76
var RelationalOperator_1: bool;
77
let
78
	RelationalOperator_1 = prePopulation_1 < environmentCapacity_1;
79
	require_1 = RelationalOperator_1;
80
	
81
tel
82

    
83

    
84

    
85

    
86

    
87

    
88
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/initialPopulation/arrow
89
node arrow_2928_000 (initialvalue_1: real;
90
nextvalue_1: real;
91
__time_step:real;)
92
 returns (output_1: real;);
93

    
94
var Memory_1: bool;Switch_1: real;false_1: bool;
95
let
96
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
97
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
98
	false_1 = false;
99
	output_1 = Switch_1;
100
	
101
tel
102

    
103

    
104
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/initialPopulation
105
node initialPopulation_2926_000 (input_1: real;
106
__time_step:real;)
107
 returns (output_1: real;);
108

    
109
var arrow_1: real;preoutput_1: real;
110
let
111
	(arrow_1) = arrow_2928_000(input_1,
112
		preoutput_1,
113
		__time_step);
114
	preoutput_1 =  1.000000000000000 -> pre( arrow_1 ) ;
115
	output_1 = arrow_1;
116
	
117
tel
118

    
119

    
120

    
121

    
122

    
123

    
124

    
125

    
126
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/sofar/arrow
127
node arrow_2866_001 (initialvalue_1: bool;
128
nextvalue_1: bool;
129
__time_step:real;)
130
 returns (output_1: bool;);
131

    
132
var Memory_1: bool;Switch_1: bool;false_1: bool;
133
let
134
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
135
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
136
	false_1 = false;
137
	output_1 = Switch_1;
138
	
139
tel
140

    
141

    
142
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/sofar
143
node sofar_2863_001 (input_1: bool;
144
__time_step:real;)
145
 returns (output_1: bool;);
146

    
147
var and_1: bool;arrow_1: bool;preoutput_1: bool;
148
let
149
	and_1 = input_1 and preoutput_1; 
150
	(arrow_1) = arrow_2866_001(input_1,
151
		and_1,
152
		__time_step);
153
	preoutput_1 =  int_to_bool(1) -> pre( arrow_1 ) ;
154
	output_1 = arrow_1;
155
	
156
tel
157

    
158

    
159

    
160

    
161

    
162

    
163
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/hasHappened/arrow
164
node arrow_2839_000 (initialvalue_1: bool;
165
nextvalue_1: bool;
166
__time_step:real;)
167
 returns (output_1: bool;);
168

    
169
var Memory_1: bool;Switch_1: bool;false_1: bool;
170
let
171
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
172
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
173
	false_1 = false;
174
	output_1 = Switch_1;
175
	
176
tel
177

    
178

    
179
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/hasHappened
180
node hasHappened_2837_001 (input_1: bool;
181
__time_step:real;)
182
 returns (output_1: bool;);
183

    
184
var arrow_1: bool;false_1: bool;or_1: bool;preoutput_1: bool;
185
let
186
	(arrow_1) = arrow_2839_000(false_1,
187
		preoutput_1,
188
		__time_step);
189
	false_1 = false;
190
	or_1 = input_1 or arrow_1; 
191
	preoutput_1 =  int_to_bool(1) -> pre( or_1 ) ;
192
	output_1 = or_1;
193
	
194
tel
195

    
196

    
197

    
198

    
199
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/arrow1
200
node arrow1_700_000 (initialvalue_1: bool;
201
nextvalue_1: bool;
202
__time_step:real;)
203
 returns (output_1: bool;);
204

    
205
var Memory_1: bool;Switch_1: bool;false_1: bool;
206
let
207
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
208
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
209
	false_1 = false;
210
	output_1 = Switch_1;
211
	
212
tel
213

    
214

    
215

    
216

    
217
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/arrow
218
node arrow_688_001 (initialvalue_1: bool;
219
nextvalue_1: bool;
220
__time_step:real;)
221
 returns (output_1: bool;);
222

    
223
var Memory_1: bool;Switch_1: bool;false_1: bool;
224
let
225
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
226
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
227
	false_1 = false;
228
	output_1 = Switch_1;
229
	
230
tel
231

    
232

    
233

    
234
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/Implication
235
node Implication_674_001 (A1_1: bool;
236
B1_1: bool;
237
__time_step:real;)
238
 returns (A_equal__equal__B_1: bool;);
239

    
240
var LogicalOperator_1: bool;LogicalOperator1_1: bool;
241
let
242
	LogicalOperator_1 = LogicalOperator1_1 or B1_1; 
243
	LogicalOperator1_1 = not A1_1; 
244
	A_equal__equal__B_1 = LogicalOperator_1;
245
	
246
tel
247

    
248

    
249
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4
250
node guarantee4_671_001 (population_1: real;
251
environmentCapacity_1: real;
252
__time_step:real;)
253
 returns (guarantee_1: bool;);
254

    
255
var Implication_1: bool;LogicalOperator_1: bool;RelationalOperator_1: bool;RelationalOperator1_1: bool;RelationalOperator2_1: bool;arrow_1: bool;arrow1_1: bool;hasHappened_1: bool;prepopulation_1: real;sofar_1: bool;true_1: bool;true1_1: bool;
256
let
257
	(Implication_1) = Implication_674_001(LogicalOperator_1,
258
		sofar_1,
259
		__time_step);
260
	LogicalOperator_1 = hasHappened_1 and RelationalOperator1_1 and RelationalOperator2_1; 
261
	RelationalOperator_1 = population_1 < prepopulation_1;
262
	RelationalOperator1_1 = prepopulation_1 > environmentCapacity_1;
263
	RelationalOperator2_1 = population_1 > environmentCapacity_1;
264
	(arrow_1) = arrow_688_001(true_1,
265
		Implication_1,
266
		__time_step);
267
	(arrow1_1) = arrow1_700_000(true1_1,
268
		RelationalOperator_1,
269
		__time_step);
270
	(hasHappened_1) = hasHappened_2837_001(RelationalOperator_1,
271
		__time_step);
272
	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;
273
	(sofar_1) = sofar_2863_001(arrow1_1,
274
		__time_step);
275
	true_1 = true;
276
	true1_1 = true;
277
	guarantee_1 = arrow_1;
278
	
279
tel
280

    
281

    
282

    
283

    
284

    
285

    
286

    
287

    
288
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/sofar/arrow
289
node arrow_622_000 (initialvalue_1: bool;
290
nextvalue_1: bool;
291
__time_step:real;)
292
 returns (output_1: bool;);
293

    
294
var Memory_1: bool;Switch_1: bool;false_1: bool;
295
let
296
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
297
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
298
	false_1 = false;
299
	output_1 = Switch_1;
300
	
301
tel
302

    
303

    
304
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/sofar
305
node sofar_619_000 (input_1: bool;
306
__time_step:real;)
307
 returns (output_1: bool;);
308

    
309
var and_1: bool;arrow_1: bool;preoutput_1: bool;
310
let
311
	and_1 = input_1 and preoutput_1; 
312
	(arrow_1) = arrow_622_000(input_1,
313
		and_1,
314
		__time_step);
315
	preoutput_1 =  int_to_bool(1) -> pre( arrow_1 ) ;
316
	output_1 = arrow_1;
317
	
318
tel
319

    
320

    
321

    
322

    
323

    
324

    
325
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/hasHappened/arrow
326
node arrow_595_000 (initialvalue_1: bool;
327
nextvalue_1: bool;
328
__time_step:real;)
329
 returns (output_1: bool;);
330

    
331
var Memory_1: bool;Switch_1: bool;false_1: bool;
332
let
333
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
334
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
335
	false_1 = false;
336
	output_1 = Switch_1;
337
	
338
tel
339

    
340

    
341
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/hasHappened
342
node hasHappened_593_000 (input_1: bool;
343
__time_step:real;)
344
 returns (output_1: bool;);
345

    
346
var arrow_1: bool;false_1: bool;or_1: bool;preoutput_1: bool;
347
let
348
	(arrow_1) = arrow_595_000(false_1,
349
		preoutput_1,
350
		__time_step);
351
	false_1 = false;
352
	or_1 = input_1 or arrow_1; 
353
	preoutput_1 =  int_to_bool(1) -> pre( or_1 ) ;
354
	output_1 = or_1;
355
	
356
tel
357

    
358

    
359

    
360

    
361
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/arrow1
362
node arrow1_581_001 (initialvalue_1: bool;
363
nextvalue_1: bool;
364
__time_step:real;)
365
 returns (output_1: bool;);
366

    
367
var Memory_1: bool;Switch_1: bool;false_1: bool;
368
let
369
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
370
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
371
	false_1 = false;
372
	output_1 = Switch_1;
373
	
374
tel
375

    
376

    
377

    
378

    
379
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/arrow
380
node arrow_569_000 (initialvalue_1: bool;
381
nextvalue_1: bool;
382
__time_step:real;)
383
 returns (output_1: bool;);
384

    
385
var Memory_1: bool;Switch_1: bool;false_1: bool;
386
let
387
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
388
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
389
	false_1 = false;
390
	output_1 = Switch_1;
391
	
392
tel
393

    
394

    
395

    
396
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/Implication
397
node Implication_555_000 (A1_1: bool;
398
B1_1: bool;
399
__time_step:real;)
400
 returns (A_equal__equal__B_1: bool;);
401

    
402
var LogicalOperator_1: bool;LogicalOperator1_1: bool;
403
let
404
	LogicalOperator_1 = LogicalOperator1_1 or B1_1; 
405
	LogicalOperator1_1 = not A1_1; 
406
	A_equal__equal__B_1 = LogicalOperator_1;
407
	
408
tel
409

    
410

    
411
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3
412
node guarantee3_552_000 (population_1: real;
413
environmentCapacity_1: real;
414
__time_step:real;)
415
 returns (guarantee_1: bool;);
416

    
417
var Implication_1: bool;LogicalOperator_1: bool;RelationalOperator_1: bool;RelationalOperator1_1: bool;RelationalOperator2_1: bool;arrow_1: bool;arrow1_1: bool;hasHappened_1: bool;prepopulation_1: real;sofar_1: bool;true_1: bool;true1_1: bool;
418
let
419
	(Implication_1) = Implication_555_000(LogicalOperator_1,
420
		sofar_1,
421
		__time_step);
422
	LogicalOperator_1 = hasHappened_1 and RelationalOperator1_1 and RelationalOperator2_1; 
423
	RelationalOperator_1 = population_1 > prepopulation_1;
424
	RelationalOperator1_1 = prepopulation_1 < environmentCapacity_1;
425
	RelationalOperator2_1 = population_1 < environmentCapacity_1;
426
	(arrow_1) = arrow_569_000(true_1,
427
		Implication_1,
428
		__time_step);
429
	(arrow1_1) = arrow1_581_001(true1_1,
430
		RelationalOperator_1,
431
		__time_step);
432
	(hasHappened_1) = hasHappened_593_000(RelationalOperator_1,
433
		__time_step);
434
	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;
435
	(sofar_1) = sofar_619_000(arrow1_1,
436
		__time_step);
437
	true_1 = true;
438
	true1_1 = true;
439
	guarantee_1 = arrow_1;
440
	
441
tel
442

    
443

    
444

    
445

    
446

    
447
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee1/arrow
448
node arrow_533_000 (initialvalue_1: bool;
449
nextvalue_1: bool;
450
__time_step:real;)
451
 returns (output_1: bool;);
452

    
453
var Memory_1: bool;Switch_1: bool;false_1: bool;
454
let
455
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
456
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
457
	false_1 = false;
458
	output_1 = Switch_1;
459
	
460
tel
461

    
462

    
463
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee1
464
node guarantee1_529_001 (population_1: real;
465
initialPopulation_1: real;
466
__time_step:real;)
467
 returns (guarantee_1: bool;);
468

    
469
var RelationalOperator_1: bool;arrow_1: bool;true_1: bool;
470
let
471
	RelationalOperator_1 = population_1 = initialPopulation_1;
472
	(arrow_1) = arrow_533_000(RelationalOperator_1,
473
		true_1,
474
		__time_step);
475
	true_1 = true;
476
	guarantee_1 = arrow_1;
477
	
478
tel
479

    
480

    
481

    
482

    
483
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee population > 0/Compare--To Zero1
484
node CompareToZero1_518_001 (u_1: real;
485
__time_step:real;)
486
 returns (y_1: bool;);
487

    
488
var Compare_1: bool;Constant_1: real;
489
let
490
	Compare_1 = u_1 > Constant_1;
491
	Constant_1 = 0.000000000000000;
492
	y_1 = Compare_1;
493
	
494
tel
495

    
496

    
497
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee population > 0
498
node guaranteepopulation_0_516_001 (population_1: real;
499
__time_step:real;)
500
 returns (guarantee_1: bool;);
501

    
502
var CompareToZero1_1: bool;
503
let
504
	(CompareToZero1_1) = CompareToZero1_518_001(population_1,
505
		__time_step);
506
	guarantee_1 = CompareToZero1_1;
507
	
508
tel
509

    
510

    
511

    
512

    
513

    
514

    
515
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure3/arrow
516
node arrow_493_000 (initialvalue_1: bool;
517
nextvalue_1: bool;
518
__time_step:real;)
519
 returns (output_1: bool;);
520

    
521
var Memory_1: bool;Switch_1: bool;false_1: bool;
522
let
523
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
524
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
525
	false_1 = false;
526
	output_1 = Switch_1;
527
	
528
tel
529

    
530

    
531
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure3
532
node ensure3_490_000 (population_1: real;
533
__time_step:real;)
534
 returns (ensure_1: bool;);
535

    
536
var RelationalOperator1_1: bool;arrow_1: bool;prepopulation_1: real;true_1: bool;
537
let
538
	RelationalOperator1_1 = population_1 = prepopulation_1;
539
	(arrow_1) = arrow_493_000(true_1,
540
		RelationalOperator1_1,
541
		__time_step);
542
	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;
543
	true_1 = true;
544
	ensure_1 = arrow_1;
545
	
546
tel
547

    
548

    
549

    
550

    
551

    
552

    
553
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure2/arrow
554
node arrow_468_001 (initialvalue_1: bool;
555
nextvalue_1: bool;
556
__time_step:real;)
557
 returns (output_1: bool;);
558

    
559
var Memory_1: bool;Switch_1: bool;false_1: bool;
560
let
561
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
562
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
563
	false_1 = false;
564
	output_1 = Switch_1;
565
	
566
tel
567

    
568

    
569
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure2
570
node ensure2_465_001 (population_1: real;
571
__time_step:real;)
572
 returns (ensure_1: bool;);
573

    
574
var RelationalOperator1_1: bool;arrow_1: bool;prepopulation_1: real;true_1: bool;
575
let
576
	RelationalOperator1_1 = population_1 < prepopulation_1;
577
	(arrow_1) = arrow_468_001(true_1,
578
		RelationalOperator1_1,
579
		__time_step);
580
	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;
581
	true_1 = true;
582
	ensure_1 = arrow_1;
583
	
584
tel
585

    
586

    
587

    
588

    
589

    
590

    
591
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure1/arrow
592
node arrow_442_000 (initialvalue_1: bool;
593
nextvalue_1: bool;
594
__time_step:real;)
595
 returns (output_1: bool;);
596

    
597
var Memory_1: bool;Switch_1: bool;false_1: bool;
598
let
599
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
600
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
601
	false_1 = false;
602
	output_1 = Switch_1;
603
	
604
tel
605

    
606

    
607
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure1
608
node ensure1_440_000 (population_1: real;
609
__time_step:real;)
610
 returns (ensure_1: bool;);
611

    
612
var arrow_1: bool;greaterthan_1: bool;prepopulation_1: real;true_1: bool;
613
let
614
	(arrow_1) = arrow_442_000(true_1,
615
		greaterthan_1,
616
		__time_step);
617
	greaterthan_1 = population_1 > prepopulation_1;
618
	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;
619
	true_1 = true;
620
	ensure_1 = arrow_1;
621
	
622
tel
623

    
624

    
625

    
626

    
627
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/assume initialPopulation > 0/Compare--To Zero
628
node CompareToZero_418_000 (u_1: real;
629
__time_step:real;)
630
 returns (y_1: bool;);
631

    
632
var Compare_1: bool;Constant_1: real;
633
let
634
	Compare_1 = u_1 > Constant_1;
635
	Constant_1 = 0.000000000000000;
636
	y_1 = Compare_1;
637
	
638
tel
639

    
640

    
641
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/assume initialPopulation > 0
642
node assumeinitialPopulation_0_416_000 (initialPopulation_1: real;
643
__time_step:real;)
644
 returns (assume_1: bool;);
645

    
646
var CompareToZero_1: bool;
647
let
648
	(CompareToZero_1) = CompareToZero_418_000(initialPopulation_1,
649
		__time_step);
650
	assume_1 = CompareToZero_1;
651
	
652
tel
653

    
654

    
655
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec
656
contract bacteriaPopulationSpec_412_000 (population0_1: real;
657
__time_step:real;)
658
 returns (population_1: real;);
659

    
660

    
661
let
662
	assume "assumeinitialPopulation_0_416_000"  assumeinitialPopulation_0_416_000(initialPopulation_1,
663
		__time_step);
664
	mode decreasing_429_000(
665
	require require2prePopulation_environmentCapacity_1;
666
		ensure ensure2_1;
667
		);
668
	var ensure1_1: bool = ensure1_440_000(population_1,
669
		__time_step);
670
	var ensure2_1: bool = ensure2_465_001(population_1,
671
		__time_step);
672
	var ensure3_1: bool = ensure3_490_000(population_1,
673
		__time_step);
674
	var environmentCapacity_1: real = 32.000000000000000;
675
	guarantee "guaranteepopulation_0_516_001"  guaranteepopulation_0_516_001(population_1,
676
		__time_step);
677
	guarantee "guarantee1_529_001"  guarantee1_529_001(population_1,
678
		initialPopulation_1,
679
		__time_step);
680
	guarantee "guarantee3_552_000"  guarantee3_552_000(population_1,
681
		environmentCapacity_1,
682
		__time_step);
683
	guarantee "guarantee4_671_001"  guarantee4_671_001(population_1,
684
		environmentCapacity_1,
685
		__time_step);
686
	mode increasing_2915_001(
687
	require require1prePopulation_environmentCapacity_1;
688
		ensure ensure1_1;
689
		);
690
	var initialPopulation_1: real = initialPopulation_2926_000(population0_1,
691
		__time_step);
692
	var prepopulation_1: real =  0.000000000000000 -> pre( population_1 ) ;
693
	var require1prePopulation_environmentCapacity_1: bool = require1prePopulation_environmentCapacity_2948_000(environmentCapacity_1,
694
		prepopulation_1,
695
		__time_step);
696
	var require2prePopulation_environmentCapacity_1: bool = require2prePopulation_environmentCapacity_2956_000(environmentCapacity_1,
697
		prepopulation_1,
698
		__time_step);
699
	var require3prePopulation_equal_environmentCapacity_1: bool = require3prePopulation_equal_environmentCapacity_2964_001(environmentCapacity_1,
700
		prepopulation_1,
701
		__time_step);
702
	mode stable_2987_000(
703
	require require3prePopulation_equal_environmentCapacity_1;
704
		ensure ensure3_1;
705
		);
706
	
707
tel
708

    
709

    
710

    
711

    
712

    
713

    
714

    
715

    
716

    
717

    
718

    
719

    
720

    
721

    
722

    
723

    
724
-- Entry action for state :bacteriaPopulation_stable65
725
node bacteriaPopulation_stable65_en(idbacteriaPopulation_bacteriaPopulation63_1:int;
726
	population_1:real;
727
	prePopulation_1:real;
728
	isInner:bool)
729

    
730
returns (idbacteriaPopulation_bacteriaPopulation63:int;
731
	population:real;
732
	prePopulation:real);
733

    
734

    
735
var 	idbacteriaPopulation_bacteriaPopulation63_2:int;
736
	prePopulation_2:real;
737

    
738

    
739
let
740

    
741

    
742

    
743
	-- set state as active 
744
	idbacteriaPopulation_bacteriaPopulation63_2 
745
	= 65;
746
	
747

    
748
	prePopulation_2 
749
	= if (not isInner) then  population_1 
750
	 else prePopulation_1;
751
	
752

    
753
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
754
	= (idbacteriaPopulation_bacteriaPopulation63_2, population_1, prePopulation_2);
755
	
756

    
757
tel
758

    
759

    
760

    
761

    
762

    
763
-- Exit action for state :bacteriaPopulation_stable65
764
node bacteriaPopulation_stable65_ex(idbacteriaPopulation_bacteriaPopulation63_1:int;
765
	isInner:bool)
766

    
767
returns (idbacteriaPopulation_bacteriaPopulation63:int);
768

    
769

    
770
var 	idbacteriaPopulation_bacteriaPopulation63_2:int;
771

    
772

    
773
let
774

    
775

    
776

    
777
	-- set state as inactive 
778
	idbacteriaPopulation_bacteriaPopulation63_2
779
	 = if (not isInner) then 0 else idbacteriaPopulation_bacteriaPopulation63_1;
780

    
781

    
782
	(idbacteriaPopulation_bacteriaPopulation63) 
783
	= (idbacteriaPopulation_bacteriaPopulation63_1);
784
	
785

    
786
tel
787

    
788

    
789

    
790

    
791

    
792

    
793
-- Entry action for state :bacteriaPopulation_increasing64
794
node bacteriaPopulation_increasing64_en(idbacteriaPopulation_bacteriaPopulation63_1:int;
795
	population_1:real;
796
	prePopulation_1:real;
797
	isInner:bool)
798

    
799
returns (idbacteriaPopulation_bacteriaPopulation63:int;
800
	population:real;
801
	prePopulation:real);
802

    
803

    
804
var 	idbacteriaPopulation_bacteriaPopulation63_2:int;
805
	population_2:real;
806
	prePopulation_2:real;
807

    
808

    
809
let
810

    
811

    
812

    
813
	-- set state as active 
814
	idbacteriaPopulation_bacteriaPopulation63_2 
815
	= 64;
816
	
817

    
818
	prePopulation_2 
819
	= if (not isInner) then  population_1 
820
	 else prePopulation_1;
821
	
822

    
823
	population_2 
824
	= if (not isInner) then  prePopulation_2 *2.0
825
	 else population_1;
826
	
827

    
828
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
829
	= (idbacteriaPopulation_bacteriaPopulation63_2, population_2, prePopulation_2);
830
	
831

    
832
tel
833

    
834

    
835

    
836

    
837

    
838
-- Exit action for state :bacteriaPopulation_increasing64
839
node bacteriaPopulation_increasing64_ex(idbacteriaPopulation_bacteriaPopulation63_1:int;
840
	isInner:bool)
841

    
842
returns (idbacteriaPopulation_bacteriaPopulation63:int);
843

    
844

    
845
var 	idbacteriaPopulation_bacteriaPopulation63_2:int;
846

    
847

    
848
let
849

    
850

    
851

    
852
	-- set state as inactive 
853
	idbacteriaPopulation_bacteriaPopulation63_2
854
	 = if (not isInner) then 0 else idbacteriaPopulation_bacteriaPopulation63_1;
855

    
856

    
857
	(idbacteriaPopulation_bacteriaPopulation63) 
858
	= (idbacteriaPopulation_bacteriaPopulation63_1);
859
	
860

    
861
tel
862

    
863

    
864

    
865

    
866

    
867

    
868
-- Entry action for state :bacteriaPopulation_decreasing67
869
node bacteriaPopulation_decreasing67_en(idbacteriaPopulation_bacteriaPopulation63_1:int;
870
	population_1:real;
871
	prePopulation_1:real;
872
	isInner:bool)
873

    
874
returns (idbacteriaPopulation_bacteriaPopulation63:int;
875
	population:real;
876
	prePopulation:real);
877

    
878

    
879
var 	idbacteriaPopulation_bacteriaPopulation63_2:int;
880
	population_2:real;
881
	prePopulation_2:real;
882

    
883

    
884
let
885

    
886

    
887

    
888
	-- set state as active 
889
	idbacteriaPopulation_bacteriaPopulation63_2 
890
	= 67;
891
	
892

    
893
	prePopulation_2 
894
	= if (not isInner) then  population_1 
895
	 else prePopulation_1;
896
	
897

    
898
	population_2 
899
	= if (not isInner) then  prePopulation_2 /2.0
900
	 else population_1;
901
	
902

    
903
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
904
	= (idbacteriaPopulation_bacteriaPopulation63_2, population_2, prePopulation_2);
905
	
906

    
907
tel
908

    
909

    
910

    
911

    
912

    
913
-- Exit action for state :bacteriaPopulation_decreasing67
914
node bacteriaPopulation_decreasing67_ex(idbacteriaPopulation_bacteriaPopulation63_1:int;
915
	isInner:bool)
916

    
917
returns (idbacteriaPopulation_bacteriaPopulation63:int);
918

    
919

    
920
var 	idbacteriaPopulation_bacteriaPopulation63_2:int;
921

    
922

    
923
let
924

    
925

    
926

    
927
	-- set state as inactive 
928
	idbacteriaPopulation_bacteriaPopulation63_2
929
	 = if (not isInner) then 0 else idbacteriaPopulation_bacteriaPopulation63_1;
930

    
931

    
932
	(idbacteriaPopulation_bacteriaPopulation63) 
933
	= (idbacteriaPopulation_bacteriaPopulation63_1);
934
	
935

    
936
tel
937

    
938

    
939

    
940

    
941

    
942

    
943
-- Entry action for state :bacteriaPopulation_start66
944
node bacteriaPopulation_start66_en(idbacteriaPopulation_bacteriaPopulation63_1:int;
945
	population0:real;
946
	prePopulation_1:real;
947
	population_1:real;
948
	isInner:bool)
949

    
950
returns (idbacteriaPopulation_bacteriaPopulation63:int;
951
	prePopulation:real;
952
	population:real);
953

    
954

    
955
var 	idbacteriaPopulation_bacteriaPopulation63_2:int;
956
	prePopulation_2:real;
957
	population_2:real;
958

    
959

    
960
let
961

    
962

    
963

    
964
	-- set state as active 
965
	idbacteriaPopulation_bacteriaPopulation63_2 
966
	= 66;
967
	
968

    
969
	prePopulation_2 
970
	= if (not isInner) then population0
971
	 else prePopulation_1;
972
	
973

    
974
	population_2 
975
	= if (not isInner) then population0
976
	 else population_1;
977
	
978

    
979
	(idbacteriaPopulation_bacteriaPopulation63, prePopulation, population) 
980
	= (idbacteriaPopulation_bacteriaPopulation63_2, prePopulation_2, population_2);
981
	
982

    
983
tel
984

    
985

    
986

    
987

    
988

    
989
-- Exit action for state :bacteriaPopulation_start66
990
node bacteriaPopulation_start66_ex(idbacteriaPopulation_bacteriaPopulation63_1:int;
991
	isInner:bool)
992

    
993
returns (idbacteriaPopulation_bacteriaPopulation63:int);
994

    
995

    
996
var 	idbacteriaPopulation_bacteriaPopulation63_2:int;
997

    
998

    
999
let
1000

    
1001

    
1002

    
1003
	-- set state as inactive 
1004
	idbacteriaPopulation_bacteriaPopulation63_2
1005
	 = if (not isInner) then 0 else idbacteriaPopulation_bacteriaPopulation63_1;
1006

    
1007

    
1008
	(idbacteriaPopulation_bacteriaPopulation63) 
1009
	= (idbacteriaPopulation_bacteriaPopulation63_1);
1010
	
1011

    
1012
tel
1013

    
1014

    
1015
--***************************************************State :bacteriaPopulation_bacteriaPopulation63 Automaton***************************************************
1016

    
1017
node bacteriaPopulation_bacteriaPopulation63_node(idbacteriaPopulation_bacteriaPopulation63_1:int;
1018
	population_1:real;
1019
	population0:real;
1020
	prePopulation_1:real)
1021

    
1022
returns (idbacteriaPopulation_bacteriaPopulation63:int;
1023
	population:real;
1024
	prePopulation:real);
1025

    
1026

    
1027
let
1028

    
1029
	 automaton bacteriapopulation_bacteriapopulation63
1030

    
1031
	state POINTbacteriaPopulation_bacteriaPopulation63:
1032
	unless (idbacteriaPopulation_bacteriaPopulation63_1=0) restart POINT__TO__BACTERIAPOPULATION_START66_1
1033

    
1034

    
1035

    
1036
	unless (idbacteriaPopulation_bacteriaPopulation63_1=64) restart BACTERIAPOPULATION_INCREASING64__TO__BACTERIAPOPULATION_BACTERIAPOPULATION63JUNCTION79_1
1037

    
1038

    
1039

    
1040
	unless (idbacteriaPopulation_bacteriaPopulation63_1=66) restart BACTERIAPOPULATION_START66__TO__BACTERIAPOPULATION_BACTERIAPOPULATION63JUNCTION79_1
1041

    
1042

    
1043

    
1044
	unless (idbacteriaPopulation_bacteriaPopulation63_1=67) restart BACTERIAPOPULATION_DECREASING67__TO__BACTERIAPOPULATION_BACTERIAPOPULATION63JUNCTION79_1
1045

    
1046

    
1047

    
1048
	unless (idbacteriaPopulation_bacteriaPopulation63_1=64) restart BACTERIAPOPULATION_INCREASING64_IDL
1049

    
1050
	unless (idbacteriaPopulation_bacteriaPopulation63_1=65) restart BACTERIAPOPULATION_STABLE65_IDL
1051

    
1052
	unless (idbacteriaPopulation_bacteriaPopulation63_1=66) restart BACTERIAPOPULATION_START66_IDL
1053

    
1054
	unless (idbacteriaPopulation_bacteriaPopulation63_1=67) restart BACTERIAPOPULATION_DECREASING67_IDL
1055

    
1056
	let
1057

    
1058
		(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
1059
	= (idbacteriaPopulation_bacteriaPopulation63_1, population_1, prePopulation_1);
1060
	
1061

    
1062
	tel
1063

    
1064

    
1065

    
1066
	state POINT__TO__BACTERIAPOPULATION_START66_1:
1067

    
1068
	 var 	idbacteriaPopulation_bacteriaPopulation63_2:int;
1069
	population_2:real;
1070
	prePopulation_2:real;
1071
	let
1072

    
1073
		-- transition trace :
1074
	--POINT__To__bacteriaPopulation_start66_1
1075
		(idbacteriaPopulation_bacteriaPopulation63_2, prePopulation_2, population_2) 
1076
	= bacteriaPopulation_start66_en(idbacteriaPopulation_bacteriaPopulation63_1, population0, prePopulation_1, population_1, false);
1077
		
1078

    
1079
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
1080
	=  (idbacteriaPopulation_bacteriaPopulation63_2, population_2, prePopulation_2);
1081

    
1082

    
1083
	tel
1084

    
1085
	until true restart POINTbacteriaPopulation_bacteriaPopulation63
1086

    
1087

    
1088

    
1089
	state BACTERIAPOPULATION_INCREASING64__TO__BACTERIAPOPULATION_BACTERIAPOPULATION63JUNCTION79_1:
1090

    
1091
	 var 	idbacteriaPopulation_bacteriaPopulation63_2, idbacteriaPopulation_bacteriaPopulation63_3, idbacteriaPopulation_bacteriaPopulation63_4, idbacteriaPopulation_bacteriaPopulation63_5, idbacteriaPopulation_bacteriaPopulation63_6, idbacteriaPopulation_bacteriaPopulation63_7:int;
1092
	population_2, population_3, population_4:real;
1093
	prePopulation_2, prePopulation_3, prePopulation_4:real;
1094
	let
1095

    
1096
		
1097

    
1098
-- transition trace :
1099
	--bacteriaPopulation_increasing64__To__Junction79_1, Junction79__To__bacteriaPopulation_increasing64_1
1100
		(idbacteriaPopulation_bacteriaPopulation63_2) 
1101
	= 
1102
		 if ((  population_1 <32.0 )) then 
1103
		bacteriaPopulation_increasing64_ex(idbacteriaPopulation_bacteriaPopulation63_1, false)
1104
		 else (idbacteriaPopulation_bacteriaPopulation63_1);
1105
		
1106

    
1107
		(idbacteriaPopulation_bacteriaPopulation63_3, population_2, prePopulation_2) 
1108
	= 
1109
		 if ((  population_1 <32.0 )) then 
1110
		bacteriaPopulation_increasing64_en(idbacteriaPopulation_bacteriaPopulation63_2, population_1, prePopulation_1, false)
1111
		 else (idbacteriaPopulation_bacteriaPopulation63_2, population_1, prePopulation_1);
1112
		
1113

    
1114

    
1115
-- transition trace :
1116
	--bacteriaPopulation_increasing64__To__Junction79_1, Junction79__To__bacteriaPopulation_decreasing67_2
1117
		(idbacteriaPopulation_bacteriaPopulation63_4) 
1118
	= 
1119
		 if ((  population_1 >32.0 )) then 
1120
		bacteriaPopulation_increasing64_ex(idbacteriaPopulation_bacteriaPopulation63_1, false)
1121
		 else (idbacteriaPopulation_bacteriaPopulation63_1);
1122
		
1123

    
1124
		(idbacteriaPopulation_bacteriaPopulation63_5, population_3, prePopulation_3) 
1125
	= 
1126
		 if ((  population_1 >32.0 )) then 
1127
		bacteriaPopulation_decreasing67_en(idbacteriaPopulation_bacteriaPopulation63_4, population_1, prePopulation_1, false)
1128
		 else (idbacteriaPopulation_bacteriaPopulation63_4, population_1, prePopulation_1);
1129
		
1130

    
1131

    
1132
-- transition trace :
1133
	--bacteriaPopulation_increasing64__To__Junction79_1, Junction79__To__bacteriaPopulation_stable65_3
1134
		(idbacteriaPopulation_bacteriaPopulation63_6) 
1135
	= 
1136
		 if ((  population_1 =32.0 )) then 
1137
		bacteriaPopulation_increasing64_ex(idbacteriaPopulation_bacteriaPopulation63_1, false)
1138
		 else (idbacteriaPopulation_bacteriaPopulation63_1);
1139
		
1140

    
1141
		(idbacteriaPopulation_bacteriaPopulation63_7, population_4, prePopulation_4) 
1142
	= 
1143
		 if ((  population_1 =32.0 )) then 
1144
		bacteriaPopulation_stable65_en(idbacteriaPopulation_bacteriaPopulation63_6, population_1, prePopulation_1, false)
1145
		 else (idbacteriaPopulation_bacteriaPopulation63_6, population_1, prePopulation_1);
1146
		
1147

    
1148
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
1149
	= 
1150
		 if ((  population_1 <32.0 )) then 
1151
		(idbacteriaPopulation_bacteriaPopulation63_3, population_2, prePopulation_2)
1152
		 else
1153
		 if ((  population_1 >32.0 )) then 
1154
		(idbacteriaPopulation_bacteriaPopulation63_5, population_3, prePopulation_3)
1155
		 else
1156
		 if ((  population_1 =32.0 )) then 
1157
		(idbacteriaPopulation_bacteriaPopulation63_7, population_4, prePopulation_4)
1158
		 else (idbacteriaPopulation_bacteriaPopulation63_1, population_1, prePopulation_1);
1159

    
1160

    
1161
	tel
1162

    
1163
	until true restart POINTbacteriaPopulation_bacteriaPopulation63
1164

    
1165

    
1166

    
1167
	state BACTERIAPOPULATION_START66__TO__BACTERIAPOPULATION_BACTERIAPOPULATION63JUNCTION79_1:
1168

    
1169
	 var 	idbacteriaPopulation_bacteriaPopulation63_2, idbacteriaPopulation_bacteriaPopulation63_3, idbacteriaPopulation_bacteriaPopulation63_4, idbacteriaPopulation_bacteriaPopulation63_5, idbacteriaPopulation_bacteriaPopulation63_6, idbacteriaPopulation_bacteriaPopulation63_7:int;
1170
	population_2, population_3, population_4:real;
1171
	prePopulation_2, prePopulation_3, prePopulation_4:real;
1172
	let
1173

    
1174
		
1175

    
1176
-- transition trace :
1177
	--bacteriaPopulation_start66__To__Junction79_1, Junction79__To__bacteriaPopulation_increasing64_1
1178
		(idbacteriaPopulation_bacteriaPopulation63_2) 
1179
	= 
1180
		 if ((  population_1 <32.0 )) then 
1181
		bacteriaPopulation_start66_ex(idbacteriaPopulation_bacteriaPopulation63_1, false)
1182
		 else (idbacteriaPopulation_bacteriaPopulation63_1);
1183
		
1184

    
1185
		(idbacteriaPopulation_bacteriaPopulation63_3, population_2, prePopulation_2) 
1186
	= 
1187
		 if ((  population_1 <32.0 )) then 
1188
		bacteriaPopulation_increasing64_en(idbacteriaPopulation_bacteriaPopulation63_2, population_1, prePopulation_1, false)
1189
		 else (idbacteriaPopulation_bacteriaPopulation63_2, population_1, prePopulation_1);
1190
		
1191

    
1192

    
1193
-- transition trace :
1194
	--bacteriaPopulation_start66__To__Junction79_1, Junction79__To__bacteriaPopulation_decreasing67_2
1195
		(idbacteriaPopulation_bacteriaPopulation63_4) 
1196
	= 
1197
		 if ((  population_1 >32.0 )) then 
1198
		bacteriaPopulation_start66_ex(idbacteriaPopulation_bacteriaPopulation63_1, false)
1199
		 else (idbacteriaPopulation_bacteriaPopulation63_1);
1200
		
1201

    
1202
		(idbacteriaPopulation_bacteriaPopulation63_5, population_3, prePopulation_3) 
1203
	= 
1204
		 if ((  population_1 >32.0 )) then 
1205
		bacteriaPopulation_decreasing67_en(idbacteriaPopulation_bacteriaPopulation63_4, population_1, prePopulation_1, false)
1206
		 else (idbacteriaPopulation_bacteriaPopulation63_4, population_1, prePopulation_1);
1207
		
1208

    
1209

    
1210
-- transition trace :
1211
	--bacteriaPopulation_start66__To__Junction79_1, Junction79__To__bacteriaPopulation_stable65_3
1212
		(idbacteriaPopulation_bacteriaPopulation63_6) 
1213
	= 
1214
		 if ((  population_1 =32.0 )) then 
1215
		bacteriaPopulation_start66_ex(idbacteriaPopulation_bacteriaPopulation63_1, false)
1216
		 else (idbacteriaPopulation_bacteriaPopulation63_1);
1217
		
1218

    
1219
		(idbacteriaPopulation_bacteriaPopulation63_7, population_4, prePopulation_4) 
1220
	= 
1221
		 if ((  population_1 =32.0 )) then 
1222
		bacteriaPopulation_stable65_en(idbacteriaPopulation_bacteriaPopulation63_6, population_1, prePopulation_1, false)
1223
		 else (idbacteriaPopulation_bacteriaPopulation63_6, population_1, prePopulation_1);
1224
		
1225

    
1226
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
1227
	= 
1228
		 if ((  population_1 <32.0 )) then 
1229
		(idbacteriaPopulation_bacteriaPopulation63_3, population_2, prePopulation_2)
1230
		 else
1231
		 if ((  population_1 >32.0 )) then 
1232
		(idbacteriaPopulation_bacteriaPopulation63_5, population_3, prePopulation_3)
1233
		 else
1234
		 if ((  population_1 =32.0 )) then 
1235
		(idbacteriaPopulation_bacteriaPopulation63_7, population_4, prePopulation_4)
1236
		 else (idbacteriaPopulation_bacteriaPopulation63_1, population_1, prePopulation_1);
1237

    
1238

    
1239
	tel
1240

    
1241
	until true restart POINTbacteriaPopulation_bacteriaPopulation63
1242

    
1243

    
1244

    
1245
	state BACTERIAPOPULATION_DECREASING67__TO__BACTERIAPOPULATION_BACTERIAPOPULATION63JUNCTION79_1:
1246

    
1247
	 var 	idbacteriaPopulation_bacteriaPopulation63_2, idbacteriaPopulation_bacteriaPopulation63_3, idbacteriaPopulation_bacteriaPopulation63_4, idbacteriaPopulation_bacteriaPopulation63_5, idbacteriaPopulation_bacteriaPopulation63_6, idbacteriaPopulation_bacteriaPopulation63_7:int;
1248
	population_2, population_3, population_4:real;
1249
	prePopulation_2, prePopulation_3, prePopulation_4:real;
1250
	let
1251

    
1252
		
1253

    
1254
-- transition trace :
1255
	--bacteriaPopulation_decreasing67__To__Junction79_1, Junction79__To__bacteriaPopulation_increasing64_1
1256
		(idbacteriaPopulation_bacteriaPopulation63_2) 
1257
	= 
1258
		 if ((  population_1 <32.0 )) then 
1259
		bacteriaPopulation_decreasing67_ex(idbacteriaPopulation_bacteriaPopulation63_1, false)
1260
		 else (idbacteriaPopulation_bacteriaPopulation63_1);
1261
		
1262

    
1263
		(idbacteriaPopulation_bacteriaPopulation63_3, population_2, prePopulation_2) 
1264
	= 
1265
		 if ((  population_1 <32.0 )) then 
1266
		bacteriaPopulation_increasing64_en(idbacteriaPopulation_bacteriaPopulation63_2, population_1, prePopulation_1, false)
1267
		 else (idbacteriaPopulation_bacteriaPopulation63_2, population_1, prePopulation_1);
1268
		
1269

    
1270

    
1271
-- transition trace :
1272
	--bacteriaPopulation_decreasing67__To__Junction79_1, Junction79__To__bacteriaPopulation_decreasing67_2
1273
		(idbacteriaPopulation_bacteriaPopulation63_4) 
1274
	= 
1275
		 if ((  population_1 >32.0 )) then 
1276
		bacteriaPopulation_decreasing67_ex(idbacteriaPopulation_bacteriaPopulation63_1, false)
1277
		 else (idbacteriaPopulation_bacteriaPopulation63_1);
1278
		
1279

    
1280
		(idbacteriaPopulation_bacteriaPopulation63_5, population_3, prePopulation_3) 
1281
	= 
1282
		 if ((  population_1 >32.0 )) then 
1283
		bacteriaPopulation_decreasing67_en(idbacteriaPopulation_bacteriaPopulation63_4, population_1, prePopulation_1, false)
1284
		 else (idbacteriaPopulation_bacteriaPopulation63_4, population_1, prePopulation_1);
1285
		
1286

    
1287

    
1288
-- transition trace :
1289
	--bacteriaPopulation_decreasing67__To__Junction79_1, Junction79__To__bacteriaPopulation_stable65_3
1290
		(idbacteriaPopulation_bacteriaPopulation63_6) 
1291
	= 
1292
		 if ((  population_1 =32.0 )) then 
1293
		bacteriaPopulation_decreasing67_ex(idbacteriaPopulation_bacteriaPopulation63_1, false)
1294
		 else (idbacteriaPopulation_bacteriaPopulation63_1);
1295
		
1296

    
1297
		(idbacteriaPopulation_bacteriaPopulation63_7, population_4, prePopulation_4) 
1298
	= 
1299
		 if ((  population_1 =32.0 )) then 
1300
		bacteriaPopulation_stable65_en(idbacteriaPopulation_bacteriaPopulation63_6, population_1, prePopulation_1, false)
1301
		 else (idbacteriaPopulation_bacteriaPopulation63_6, population_1, prePopulation_1);
1302
		
1303

    
1304
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
1305
	= 
1306
		 if ((  population_1 <32.0 )) then 
1307
		(idbacteriaPopulation_bacteriaPopulation63_3, population_2, prePopulation_2)
1308
		 else
1309
		 if ((  population_1 >32.0 )) then 
1310
		(idbacteriaPopulation_bacteriaPopulation63_5, population_3, prePopulation_3)
1311
		 else
1312
		 if ((  population_1 =32.0 )) then 
1313
		(idbacteriaPopulation_bacteriaPopulation63_7, population_4, prePopulation_4)
1314
		 else (idbacteriaPopulation_bacteriaPopulation63_1, population_1, prePopulation_1);
1315

    
1316

    
1317
	tel
1318

    
1319
	until true restart POINTbacteriaPopulation_bacteriaPopulation63
1320

    
1321

    
1322

    
1323
	state BACTERIAPOPULATION_INCREASING64_IDL:
1324

    
1325
	 	let
1326

    
1327
		
1328

    
1329
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
1330
	= (idbacteriaPopulation_bacteriaPopulation63_1, population_1, prePopulation_1);
1331
	
1332

    
1333
	tel
1334

    
1335
	until true restart POINTbacteriaPopulation_bacteriaPopulation63
1336

    
1337

    
1338

    
1339
	state BACTERIAPOPULATION_STABLE65_IDL:
1340

    
1341
	 	let
1342

    
1343
		
1344

    
1345
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
1346
	= (idbacteriaPopulation_bacteriaPopulation63_1, population_1, prePopulation_1);
1347
	
1348

    
1349
	tel
1350

    
1351
	until true restart POINTbacteriaPopulation_bacteriaPopulation63
1352

    
1353

    
1354

    
1355
	state BACTERIAPOPULATION_START66_IDL:
1356

    
1357
	 	let
1358

    
1359
		
1360

    
1361
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
1362
	= (idbacteriaPopulation_bacteriaPopulation63_1, population_1, prePopulation_1);
1363
	
1364

    
1365
	tel
1366

    
1367
	until true restart POINTbacteriaPopulation_bacteriaPopulation63
1368

    
1369

    
1370

    
1371
	state BACTERIAPOPULATION_DECREASING67_IDL:
1372

    
1373
	 	let
1374

    
1375
		
1376

    
1377
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 
1378
	= (idbacteriaPopulation_bacteriaPopulation63_1, population_1, prePopulation_1);
1379
	
1380

    
1381
	tel
1382

    
1383
	until true restart POINTbacteriaPopulation_bacteriaPopulation63
1384

    
1385

    
1386

    
1387
tel
1388

    
1389

    
1390
--***************************************************State :bacteriaPopulation_bacteriaPopulation63 Automaton***************************************************
1391

    
1392
node bacteriaPopulationStateflow_PP_bacteriaPopulation_bacteriaPopulation_bacteriaPopulation(population0:real)
1393

    
1394
returns (population:real);
1395

    
1396

    
1397
var population_1: real;
1398

    
1399
	prePopulation, prePopulation_1: real;
1400

    
1401
	dummyEvent, dummyEvent_1: bool;
1402

    
1403
	idbacteriaPopulation_bacteriaPopulation63, idbacteriaPopulation_bacteriaPopulation63_1: int;
1404

    
1405
	let
1406

    
1407
	population_1 = 0.0 -> pre population;
1408

    
1409
	prePopulation_1 = 0.0 -> pre prePopulation;
1410

    
1411
	dummyEvent_1 = false -> pre dummyEvent;
1412

    
1413
	idbacteriaPopulation_bacteriaPopulation63_1 = 0 -> pre idbacteriaPopulation_bacteriaPopulation63;
1414

    
1415
	
1416

    
1417

    
1418

    
1419
	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation)
1420
	 = bacteriaPopulation_bacteriaPopulation63_node(idbacteriaPopulation_bacteriaPopulation63_1, population_1, population0, prePopulation_1);
1421

    
1422

    
1423
--unused outputs
1424
	dummyEvent = false;
1425

    
1426
	
1427

    
1428
tel
1429

    
1430

    
1431

    
1432

    
1433

    
1434
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulation/bacteriaPopulation
1435
node bacteriaPopulation_397_000 (In1_1: real;
1436
__time_step:real;)
1437
 returns (Out1_1: real;);
1438

    
1439
var bacteriaPopulation_1: real;
1440
let
1441
	(bacteriaPopulation_1) = bacteriaPopulationStateflow_PP_bacteriaPopulation_bacteriaPopulation_bacteriaPopulation(In1_1);
1442
	Out1_1 = bacteriaPopulation_1;
1443
	
1444
tel
1445

    
1446

    
1447
-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulation
1448
node bacteriaPopulation_3513_001 (In1_1: real;
1449
__time_step:real;)
1450
 returns (Out1_1: real;);
1451
(*@contract
1452
import bacteriaPopulationSpec_412_000( In1_1, __time_step ) returns (Out1_1);
1453
*)
1454
var bacteriaPopulation_1: real;
1455
let
1456
	(bacteriaPopulation_1) = bacteriaPopulation_397_000(In1_1,
1457
		__time_step);
1458
	Out1_1 = bacteriaPopulation_1;
1459
	
1460
tel
1461

    
1462

    
1463
-- Original block name: bacteriaPopulationStateflow_PP
1464
node bacteriaPopulationStateflow_PP (population0_1: real;)
1465
 returns (population_1: real;);
1466

    
1467
var bacteriaPopulation_1: real;
1468
	__time_step:real;
1469
let
1470
	__time_step = 0.0 -> pre __time_step + 1.000000000000000;
1471
	(bacteriaPopulation_1) = bacteriaPopulation_3513_001(population0_1,
1472
		__time_step);
1473
	population_1 = bacteriaPopulation_1;
1474
	
1475
tel