Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (20 KB)

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

    
3
-- Compiler: Lustre compiler 2 (ToLustre.m)
4
-- Time: 25-Jun-2018 18:40:01
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: bacteriaPopulation_PP/bacteriaPopulationSpec/require3 pre Population = environmentCapacity/arrow
21
node arrow_675_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/require3 pre Population = environmentCapacity
37
node require3prePopulation_equal_environmentCapacity_672_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_675_001(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: bacteriaPopulation_PP/bacteriaPopulationSpec/require2 pre Population > environmentCapacity
56
node require2prePopulation_environmentCapacity_664_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/require1 pre Population < environmentCapacity
71
node require1prePopulation_environmentCapacity_656_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/initialPopulation/arrow
89
node arrow_3111_004 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/initialPopulation
105
node initialPopulation_654_001 (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_3111_004(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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee4/sofar/arrow
127
node arrow_3099_004 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee4/sofar
143
node sofar_615_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_3099_004(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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee4/hasHappened/arrow
164
node arrow_3085_004 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee4/hasHappened
180
node hasHappened_613_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_3085_004(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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee4/arrow1
200
node arrow1_612_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee4/arrow
218
node arrow_611_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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee4/Implication
235
node Implication_597_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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee4
250
node guarantee4_594_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_597_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_611_001(true_1,
265
		Implication_1,
266
		__time_step);
267
	(arrow1_1) = arrow1_612_001(true1_1,
268
		RelationalOperator_1,
269
		__time_step);
270
	(hasHappened_1) = hasHappened_613_001(RelationalOperator_1,
271
		__time_step);
272
	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;
273
	(sofar_1) = sofar_615_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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee3/sofar/arrow
289
node arrow_3051_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee3/sofar
305
node sofar_566_001 (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_3051_001(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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee3/hasHappened/arrow
326
node arrow_3037_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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee3/hasHappened
342
node hasHappened_564_001 (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_3037_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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee3/arrow1
362
node arrow1_563_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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee3/arrow
380
node arrow_562_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee3/Implication
397
node Implication_548_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee3
412
node guarantee3_545_001 (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_548_001(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_562_001(true_1,
427
		Implication_1,
428
		__time_step);
429
	(arrow1_1) = arrow1_563_001(true1_1,
430
		RelationalOperator_1,
431
		__time_step);
432
	(hasHappened_1) = hasHappened_564_001(RelationalOperator_1,
433
		__time_step);
434
	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;
435
	(sofar_1) = sofar_566_001(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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee1/arrow
448
node arrow_537_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee1
464
node guarantee1_533_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_537_001(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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee population > 0/Compare--To Zero1
484
node CompareToZero1_529_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: bacteriaPopulation_PP/bacteriaPopulationSpec/guarantee population > 0
498
node guaranteepopulation_0_527_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_529_001(population_1,
505
		__time_step);
506
	guarantee_1 = CompareToZero1_1;
507
	
508
tel
509

    
510

    
511

    
512

    
513

    
514

    
515
-- Original block name: bacteriaPopulation_PP/bacteriaPopulationSpec/ensure3/arrow
516
node arrow_515_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/ensure3
532
node ensure3_512_001 (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_515_001(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: bacteriaPopulation_PP/bacteriaPopulationSpec/ensure2/arrow
554
node arrow_501_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: bacteriaPopulation_PP/bacteriaPopulationSpec/ensure2
570
node ensure2_498_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_501_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: bacteriaPopulation_PP/bacteriaPopulationSpec/ensure1/arrow
592
node arrow_486_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/ensure1
608
node ensure1_484_001 (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_486_001(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: bacteriaPopulation_PP/bacteriaPopulationSpec/assume initialPopulation > 0/Compare--To Zero
628
node CompareToZero_469_001 (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: bacteriaPopulation_PP/bacteriaPopulationSpec/assume initialPopulation > 0
642
node assumeinitialPopulation_0_467_001 (initialPopulation_1: real;
643
__time_step:real;)
644
 returns (assume_1: bool;);
645

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

    
654

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

    
660

    
661
let
662
	assume "assumeinitialPopulation_0_467_001"  assumeinitialPopulation_0_467_001(initialPopulation_1,
663
		__time_step);
664
	mode decreasing_473_001(
665
	require require2prePopulation_environmentCapacity_1;
666
		ensure ensure2_1;
667
		);
668
	var ensure1_1: bool = ensure1_484_001(population_1,
669
		__time_step);
670
	var ensure2_1: bool = ensure2_498_001(population_1,
671
		__time_step);
672
	var ensure3_1: bool = ensure3_512_001(population_1,
673
		__time_step);
674
	var environmentCapacity_1: real = 32.000000000000000;
675
	guarantee "guaranteepopulation_0_527_001"  guaranteepopulation_0_527_001(population_1,
676
		__time_step);
677
	guarantee "guarantee1_533_001"  guarantee1_533_001(population_1,
678
		initialPopulation_1,
679
		__time_step);
680
	guarantee "guarantee3_545_001"  guarantee3_545_001(population_1,
681
		environmentCapacity_1,
682
		__time_step);
683
	guarantee "guarantee4_594_001"  guarantee4_594_001(population_1,
684
		environmentCapacity_1,
685
		__time_step);
686
	mode increasing_643_001(
687
	require require1prePopulation_environmentCapacity_1;
688
		ensure ensure1_1;
689
		);
690
	var initialPopulation_1: real = initialPopulation_654_001(population0_1,
691
		__time_step);
692
	var prepopulation_1: real =  0.000000000000000 -> pre( population_1 ) ;
693
	var require1prePopulation_environmentCapacity_1: bool = require1prePopulation_environmentCapacity_656_001(environmentCapacity_1,
694
		prepopulation_1,
695
		__time_step);
696
	var require2prePopulation_environmentCapacity_1: bool = require2prePopulation_environmentCapacity_664_001(environmentCapacity_1,
697
		prepopulation_1,
698
		__time_step);
699
	var require3prePopulation_equal_environmentCapacity_1: bool = require3prePopulation_equal_environmentCapacity_672_001(environmentCapacity_1,
700
		prepopulation_1,
701
		__time_step);
702
	mode stable_684_001(
703
	require require3prePopulation_equal_environmentCapacity_1;
704
		ensure ensure3_1;
705
		);
706
	
707
tel
708

    
709

    
710

    
711

    
712

    
713

    
714
-- Original block name: bacteriaPopulation_PP/bacteriaPopulation/arrow
715
node arrow_432_000 (initialvalue_1: real;
716
nextvalue_1: real;
717
__time_step:real;)
718
 returns (output_1: real;);
719

    
720
var Memory_1: bool;Switch_1: real;false_1: bool;
721
let
722
	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;
723
	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 
724
	false_1 = false;
725
	output_1 = Switch_1;
726
	
727
tel
728

    
729

    
730

    
731
-- Original block name: bacteriaPopulation_PP/bacteriaPopulation/Compare--To Zero1
732
node CompareToZero1_429_000 (u_1: real;
733
__time_step:real;)
734
 returns (y_1: bool;);
735

    
736
var Compare_1: bool;Constant_1: real;
737
let
738
	Compare_1 = u_1 < Constant_1;
739
	Constant_1 = 0.000000000000000;
740
	y_1 = Compare_1;
741
	
742
tel
743

    
744

    
745

    
746
-- Original block name: bacteriaPopulation_PP/bacteriaPopulation/Compare--To Zero
747
node CompareToZero_428_000 (u_1: real;
748
__time_step:real;)
749
 returns (y_1: bool;);
750

    
751
var Compare_1: bool;Constant_1: real;
752
let
753
	Compare_1 = u_1 > Constant_1;
754
	Constant_1 = 0.000000000000000;
755
	y_1 = Compare_1;
756
	
757
tel
758

    
759

    
760
-- Original block name: bacteriaPopulation_PP/bacteriaPopulation
761
node bacteriaPopulation_425_000 (population0_1: real;
762
__time_step:real;)
763
 returns (population_1: real;);
764
(*@contract
765
import bacteriaPopulationSpec_463_001( population0_1, __time_step ) returns (population_1);
766
*)
767
var Add_1: real;CompareToZero_1: bool;CompareToZero1_1: bool;Switch2_1: real;Switch3_1: real;arrow_1: real;death_1: real;deathproduct_1: real;environmentCapacity_1: real;growth_1: real;growthproduct_1: real;prepopulation_1: real;
768
let
769
	Add_1 = 0.0 + environmentCapacity_1 - prepopulation_1;
770
	(CompareToZero_1) = CompareToZero_428_000(Add_1,
771
		__time_step);
772
	(CompareToZero1_1) = CompareToZero1_429_000(Add_1,
773
		__time_step);
774
	Switch2_1 = if  CompareToZero_1  then growthproduct_1 else Switch3_1; 
775
	Switch3_1 = if  CompareToZero1_1  then deathproduct_1 else prepopulation_1; 
776
	(arrow_1) = arrow_432_000(population0_1,
777
		Switch2_1,
778
		__time_step);
779
	death_1 = 0.500000000000000;
780
	deathproduct_1 = 1.0 * death_1 * prepopulation_1;
781
	environmentCapacity_1 = 32.000000000000000;
782
	growth_1 = 2.000000000000000;
783
	growthproduct_1 = 1.0 * growth_1 * prepopulation_1;
784
	prepopulation_1 =  0.000000000000000 -> pre( arrow_1 ) ;
785
	population_1 = arrow_1;
786
	
787
tel
788

    
789

    
790
-- Original block name: bacteriaPopulation_PP
791
node bacteriaPopulation_PP (population0_1: real;)
792
 returns (population_1: real;);
793

    
794
var bacteriaPopulation_1: real;
795
	__time_step:real;
796
let
797
	__time_step = 0.0 -> pre __time_step + 1.000000000000000;
798
	(bacteriaPopulation_1) = bacteriaPopulation_425_000(population0_1,
799
		__time_step);
800
	population_1 = bacteriaPopulation_1;
801
	
802
tel