Project

General

Profile

Revision 1e3ae41f

View differences:

tests/cocospec/DaysEnum_PP.KIND2.lus
1
-- This file has been generated by CoCoSim2.
2

  
3
-- Compiler: Lustre compiler 2 (ToLustre.m)
4
-- Time: 18-Jan-2019 19:01:54
5
type days = enum {Sunday, Monday, Tuesday, Wednesday, Thursday, Friday, Saturday};
6
(*
7
Original block name: DaysEnum_PP/contract/guarantee/EnumeratedConstant
8
*)
9
node  EnumeratedConstant_84_000(__time_step : real;
10
	__nb_step : int;)
11
returns(Out_1 : days;);
12
let
13
	Out_1 = ( Saturday );
14
tel
15

  
16
(*
17
Original block name: DaysEnum_PP/contract/guarantee/EnumeratedConstant1
18
*)
19
node  EnumeratedConstant1_85_000(__time_step : real;
20
	__nb_step : int;)
21
returns(Out_1 : days;);
22
let
23
	Out_1 = ( Sunday );
24
tel
25

  
26
(*
27
Original block name: DaysEnum_PP/contract/guarantee
28
*)
29
node  guarantee_81_000(day_1 : days;
30
	isWeekend_1 : bool;
31
	__time_step : real;
32
	__nb_step : int;)
33
returns(guarantee_1 : bool;);
34
let
35
	guarantee_1 = ( ( (not ( ( (( EnumeratedConstant_84_000(__time_step, __nb_step) ) <> day_1) ) and ( (day_1 <> ( EnumeratedConstant1_85_000(__time_step, __nb_step) )) ) )) ) or ( (not isWeekend_1) ) );
36
tel
37

  
38
(*
39
Original block name: DaysEnum_PP/subsystem/EnumeratedConstant
40
*)
41
node  EnumeratedConstant_113_000(__time_step : real;
42
	__nb_step : int;)
43
returns(Out_1 : days;);
44
let
45
	Out_1 = ( Saturday );
46
tel
47

  
48
(*
49
Original block name: DaysEnum_PP/subsystem/EnumeratedConstant1
50
*)
51
node  EnumeratedConstant1_114_000(__time_step : real;
52
	__nb_step : int;)
53
returns(Out_1 : days;);
54
let
55
	Out_1 = ( Sunday );
56
tel
57

  
58
(*
59
Original block name: DaysEnum_PP/contract
60
*)
61
contract contract_78_000(day_1 : days;
62
	__time_step : real;
63
	__nb_step : int;)
64
returns(isWeekend_1 : bool;);
65
let
66
	guarantee "guarantee_81_000" guarantee_81_000(day_1, isWeekend_1, __time_step, __nb_step);
67
tel
68

  
69
(*
70
Original block name: DaysEnum_PP/subsystem
71
*)
72
node  subsystem_111_000(day_1 : days;
73
	__time_step : real;
74
	__nb_step : int;)
75
returns(isWeekend_1 : bool;);
76
(*@contract
77
	import contract_78_000(day_1, __time_step, __nb_step) returns (isWeekend_1);
78
*)
79
let
80
	isWeekend_1 = ( ( (( EnumeratedConstant_113_000(__time_step, __nb_step) ) = day_1) ) or ( (day_1 = ( EnumeratedConstant1_114_000(__time_step, __nb_step) )) ) );
81
tel
82

  
83
(*
84
Original block name: DaysEnum_PP
85
*)
86
node  DaysEnum_PP(day_1 : days;)
87
returns(isWeekend_1 : bool;);
88
var __time_step : real;
89
	__nb_step : int;
90
let
91
	isWeekend_1 = ( subsystem_111_000(day_1, __time_step, __nb_step) );
92
	__time_step = (0.0 -> ((pre __time_step) + 1.0));
93
	__nb_step = (0 -> ((pre __nb_step) + 1));
94
tel
95

  
tests/cocospec/bacteriaPopulationStateflow_PP.lus
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

  
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff