CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by CoCoSim2.

-- Compiler: Lustre compiler 2 (ToLustre.m)

-- Time: 28-Jun-2018 10:59:12

--external libraries

node int_to_bool (x: int)

returns(y:bool);

let

	 y= (x <> 0);

tel

--Simulink code

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/require3 pre Population = environmentCapacity/arrow

node arrow_2967_000 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/require3 pre Population = environmentCapacity

node require3prePopulation_equal_environmentCapacity_2964_001 (environmentCapacity_1: real;

prePopulation_1: real;

__time_step:real;)

 returns (require_1: bool;);

var arrow_1: bool;equals_1: bool;true_1: bool;

let

	(arrow_1) = arrow_2967_000(true_1,

		equals_1,

		__time_step);

	equals_1 = prePopulation_1 = environmentCapacity_1;

	true_1 = true;

	require_1 = arrow_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/require2 pre Population > environmentCapacity

node require2prePopulation_environmentCapacity_2956_000 (environmentCapacity_1: real;

prePopulation_1: real;

__time_step:real;)

 returns (require_1: bool;);

var RelationalOperator_1: bool;

let

	RelationalOperator_1 = prePopulation_1 > environmentCapacity_1;

	require_1 = RelationalOperator_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/require1 pre Population < environmentCapacity

node require1prePopulation_environmentCapacity_2948_000 (environmentCapacity_1: real;

prePopulation_1: real;

__time_step:real;)

 returns (require_1: bool;);

var RelationalOperator_1: bool;

let

	RelationalOperator_1 = prePopulation_1 < environmentCapacity_1;

	require_1 = RelationalOperator_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/initialPopulation/arrow

node arrow_2928_000 (initialvalue_1: real;

nextvalue_1: real;

__time_step:real;)

 returns (output_1: real;);

var Memory_1: bool;Switch_1: real;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/initialPopulation

node initialPopulation_2926_000 (input_1: real;

__time_step:real;)

 returns (output_1: real;);

var arrow_1: real;preoutput_1: real;

let

	(arrow_1) = arrow_2928_000(input_1,

		preoutput_1,

		__time_step);

	preoutput_1 =  1.000000000000000 -> pre( arrow_1 ) ;

	output_1 = arrow_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/sofar/arrow

node arrow_2866_001 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/sofar

node sofar_2863_001 (input_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var and_1: bool;arrow_1: bool;preoutput_1: bool;

let

	and_1 = input_1 and preoutput_1; 

	(arrow_1) = arrow_2866_001(input_1,

		and_1,

		__time_step);

	preoutput_1 =  int_to_bool(1) -> pre( arrow_1 ) ;

	output_1 = arrow_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/hasHappened/arrow

node arrow_2839_000 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/hasHappened

node hasHappened_2837_001 (input_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var arrow_1: bool;false_1: bool;or_1: bool;preoutput_1: bool;

let

	(arrow_1) = arrow_2839_000(false_1,

		preoutput_1,

		__time_step);

	false_1 = false;

	or_1 = input_1 or arrow_1; 

	preoutput_1 =  int_to_bool(1) -> pre( or_1 ) ;

	output_1 = or_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/arrow1

node arrow1_700_000 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/arrow

node arrow_688_001 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4/Implication

node Implication_674_001 (A1_1: bool;

B1_1: bool;

__time_step:real;)

 returns (A_equal__equal__B_1: bool;);

var LogicalOperator_1: bool;LogicalOperator1_1: bool;

let

	LogicalOperator_1 = LogicalOperator1_1 or B1_1; 

	LogicalOperator1_1 = not A1_1; 

	A_equal__equal__B_1 = LogicalOperator_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee4

node guarantee4_671_001 (population_1: real;

environmentCapacity_1: real;

__time_step:real;)

 returns (guarantee_1: bool;);

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;

let

	(Implication_1) = Implication_674_001(LogicalOperator_1,

		sofar_1,

		__time_step);

	LogicalOperator_1 = hasHappened_1 and RelationalOperator1_1 and RelationalOperator2_1; 

	RelationalOperator_1 = population_1 < prepopulation_1;

	RelationalOperator1_1 = prepopulation_1 > environmentCapacity_1;

	RelationalOperator2_1 = population_1 > environmentCapacity_1;

	(arrow_1) = arrow_688_001(true_1,

		Implication_1,

		__time_step);

	(arrow1_1) = arrow1_700_000(true1_1,

		RelationalOperator_1,

		__time_step);

	(hasHappened_1) = hasHappened_2837_001(RelationalOperator_1,

		__time_step);

	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;

	(sofar_1) = sofar_2863_001(arrow1_1,

		__time_step);

	true_1 = true;

	true1_1 = true;

	guarantee_1 = arrow_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/sofar/arrow

node arrow_622_000 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/sofar

node sofar_619_000 (input_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var and_1: bool;arrow_1: bool;preoutput_1: bool;

let

	and_1 = input_1 and preoutput_1; 

	(arrow_1) = arrow_622_000(input_1,

		and_1,

		__time_step);

	preoutput_1 =  int_to_bool(1) -> pre( arrow_1 ) ;

	output_1 = arrow_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/hasHappened/arrow

node arrow_595_000 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/hasHappened

node hasHappened_593_000 (input_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var arrow_1: bool;false_1: bool;or_1: bool;preoutput_1: bool;

let

	(arrow_1) = arrow_595_000(false_1,

		preoutput_1,

		__time_step);

	false_1 = false;

	or_1 = input_1 or arrow_1; 

	preoutput_1 =  int_to_bool(1) -> pre( or_1 ) ;

	output_1 = or_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/arrow1

node arrow1_581_001 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/arrow

node arrow_569_000 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3/Implication

node Implication_555_000 (A1_1: bool;

B1_1: bool;

__time_step:real;)

 returns (A_equal__equal__B_1: bool;);

var LogicalOperator_1: bool;LogicalOperator1_1: bool;

let

	LogicalOperator_1 = LogicalOperator1_1 or B1_1; 

	LogicalOperator1_1 = not A1_1; 

	A_equal__equal__B_1 = LogicalOperator_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee3

node guarantee3_552_000 (population_1: real;

environmentCapacity_1: real;

__time_step:real;)

 returns (guarantee_1: bool;);

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;

let

	(Implication_1) = Implication_555_000(LogicalOperator_1,

		sofar_1,

		__time_step);

	LogicalOperator_1 = hasHappened_1 and RelationalOperator1_1 and RelationalOperator2_1; 

	RelationalOperator_1 = population_1 > prepopulation_1;

	RelationalOperator1_1 = prepopulation_1 < environmentCapacity_1;

	RelationalOperator2_1 = population_1 < environmentCapacity_1;

	(arrow_1) = arrow_569_000(true_1,

		Implication_1,

		__time_step);

	(arrow1_1) = arrow1_581_001(true1_1,

		RelationalOperator_1,

		__time_step);

	(hasHappened_1) = hasHappened_593_000(RelationalOperator_1,

		__time_step);

	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;

	(sofar_1) = sofar_619_000(arrow1_1,

		__time_step);

	true_1 = true;

	true1_1 = true;

	guarantee_1 = arrow_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee1/arrow

node arrow_533_000 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee1

node guarantee1_529_001 (population_1: real;

initialPopulation_1: real;

__time_step:real;)

 returns (guarantee_1: bool;);

var RelationalOperator_1: bool;arrow_1: bool;true_1: bool;

let

	RelationalOperator_1 = population_1 = initialPopulation_1;

	(arrow_1) = arrow_533_000(RelationalOperator_1,

		true_1,

		__time_step);

	true_1 = true;

	guarantee_1 = arrow_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee population > 0/Compare--To Zero1

node CompareToZero1_518_001 (u_1: real;

__time_step:real;)

 returns (y_1: bool;);

var Compare_1: bool;Constant_1: real;

let

	Compare_1 = u_1 > Constant_1;

	Constant_1 = 0.000000000000000;

	y_1 = Compare_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/guarantee population > 0

node guaranteepopulation_0_516_001 (population_1: real;

__time_step:real;)

 returns (guarantee_1: bool;);

var CompareToZero1_1: bool;

let

	(CompareToZero1_1) = CompareToZero1_518_001(population_1,

		__time_step);

	guarantee_1 = CompareToZero1_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure3/arrow

node arrow_493_000 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure3

node ensure3_490_000 (population_1: real;

__time_step:real;)

 returns (ensure_1: bool;);

var RelationalOperator1_1: bool;arrow_1: bool;prepopulation_1: real;true_1: bool;

let

	RelationalOperator1_1 = population_1 = prepopulation_1;

	(arrow_1) = arrow_493_000(true_1,

		RelationalOperator1_1,

		__time_step);

	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;

	true_1 = true;

	ensure_1 = arrow_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure2/arrow

node arrow_468_001 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure2

node ensure2_465_001 (population_1: real;

__time_step:real;)

 returns (ensure_1: bool;);

var RelationalOperator1_1: bool;arrow_1: bool;prepopulation_1: real;true_1: bool;

let

	RelationalOperator1_1 = population_1 < prepopulation_1;

	(arrow_1) = arrow_468_001(true_1,

		RelationalOperator1_1,

		__time_step);

	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;

	true_1 = true;

	ensure_1 = arrow_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure1/arrow

node arrow_442_000 (initialvalue_1: bool;

nextvalue_1: bool;

__time_step:real;)

 returns (output_1: bool;);

var Memory_1: bool;Switch_1: bool;false_1: bool;

let

	Memory_1 =  int_to_bool(1) -> pre( false_1 ) ;

	Switch_1 = if  Memory_1  then initialvalue_1 else nextvalue_1; 

	false_1 = false;

	output_1 = Switch_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/ensure1

node ensure1_440_000 (population_1: real;

__time_step:real;)

 returns (ensure_1: bool;);

var arrow_1: bool;greaterthan_1: bool;prepopulation_1: real;true_1: bool;

let

	(arrow_1) = arrow_442_000(true_1,

		greaterthan_1,

		__time_step);

	greaterthan_1 = population_1 > prepopulation_1;

	prepopulation_1 =  0.000000000000000 -> pre( population_1 ) ;

	true_1 = true;

	ensure_1 = arrow_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/assume initialPopulation > 0/Compare--To Zero

node CompareToZero_418_000 (u_1: real;

__time_step:real;)

 returns (y_1: bool;);

var Compare_1: bool;Constant_1: real;

let

	Compare_1 = u_1 > Constant_1;

	Constant_1 = 0.000000000000000;

	y_1 = Compare_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec/assume initialPopulation > 0

node assumeinitialPopulation_0_416_000 (initialPopulation_1: real;

__time_step:real;)

 returns (assume_1: bool;);

var CompareToZero_1: bool;

let

	(CompareToZero_1) = CompareToZero_418_000(initialPopulation_1,

		__time_step);

	assume_1 = CompareToZero_1;

tel

-- Original block name: bacteriaPopulationStateflow_PP/bacteriaPopulationSpec

(*@

contract bacteriaPopulationSpec_412_000 (population0_1: real;

__time_step:real;)

 returns (population_1: real;);

let

	assume "assumeinitialPopulation_0_416_000"  assumeinitialPopulation_0_416_000(initialPopulation_1,

		__time_step);

	mode decreasing_429_000(

	require require2prePopulation_environmentCapacity_1;

		ensure ensure2_1;

		);

	var ensure1_1: bool = ensure1_440_000(population_1,

		__time_step);

	var ensure2_1: bool = ensure2_465_001(population_1,

		__time_step);

	var ensure3_1: bool = ensure3_490_000(population_1,

		__time_step);

	var environmentCapacity_1: real = 32.000000000000000;

	guarantee "guaranteepopulation_0_516_001"  guaranteepopulation_0_516_001(population_1,

		__time_step);

	guarantee "guarantee1_529_001"  guarantee1_529_001(population_1,

		initialPopulation_1,

		__time_step);

	guarantee "guarantee3_552_000"  guarantee3_552_000(population_1,

		environmentCapacity_1,

		__time_step);

	guarantee "guarantee4_671_001"  guarantee4_671_001(population_1,

		environmentCapacity_1,

		__time_step);

	mode increasing_2915_001(

	require require1prePopulation_environmentCapacity_1;

		ensure ensure1_1;

		);

	var initialPopulation_1: real = initialPopulation_2926_000(population0_1,

		__time_step);

	var prepopulation_1: real =  0.000000000000000 -> pre( population_1 ) ;

	var require1prePopulation_environmentCapacity_1: bool = require1prePopulation_environmentCapacity_2948_000(environmentCapacity_1,

		prepopulation_1,

		__time_step);

	var require2prePopulation_environmentCapacity_1: bool = require2prePopulation_environmentCapacity_2956_000(environmentCapacity_1,

		prepopulation_1,

		__time_step);

	var require3prePopulation_equal_environmentCapacity_1: bool = require3prePopulation_equal_environmentCapacity_2964_001(environmentCapacity_1,

		prepopulation_1,

		__time_step);

	mode stable_2987_000(

	require require3prePopulation_equal_environmentCapacity_1;

		ensure ensure3_1;

		);

tel

*)

-- Entry action for state :bacteriaPopulation_stable65

node bacteriaPopulation_stable65_en(idbacteriaPopulation_bacteriaPopulation63_1:int;

	population_1:real;

	prePopulation_1:real;

	isInner:bool)

returns (idbacteriaPopulation_bacteriaPopulation63:int;

	population:real;

	prePopulation:real);

var 	idbacteriaPopulation_bacteriaPopulation63_2:int;

	prePopulation_2:real;

let

	-- set state as active 

	idbacteriaPopulation_bacteriaPopulation63_2 

	= 65;

	prePopulation_2 

	= if (not isInner) then  population_1 

	 else prePopulation_1;

	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 

	= (idbacteriaPopulation_bacteriaPopulation63_2, population_1, prePopulation_2);

tel

-- Exit action for state :bacteriaPopulation_stable65

node bacteriaPopulation_stable65_ex(idbacteriaPopulation_bacteriaPopulation63_1:int;

	isInner:bool)

returns (idbacteriaPopulation_bacteriaPopulation63:int);

var 	idbacteriaPopulation_bacteriaPopulation63_2:int;

let

	-- set state as inactive 

	idbacteriaPopulation_bacteriaPopulation63_2

	 = if (not isInner) then 0 else idbacteriaPopulation_bacteriaPopulation63_1;

	(idbacteriaPopulation_bacteriaPopulation63) 

	= (idbacteriaPopulation_bacteriaPopulation63_1);

tel

-- Entry action for state :bacteriaPopulation_increasing64

node bacteriaPopulation_increasing64_en(idbacteriaPopulation_bacteriaPopulation63_1:int;

	population_1:real;

	prePopulation_1:real;

	isInner:bool)

returns (idbacteriaPopulation_bacteriaPopulation63:int;

	population:real;

	prePopulation:real);

var 	idbacteriaPopulation_bacteriaPopulation63_2:int;

	population_2:real;

	prePopulation_2:real;

let

	-- set state as active 

	idbacteriaPopulation_bacteriaPopulation63_2 

	= 64;

	prePopulation_2 

	= if (not isInner) then  population_1 

	 else prePopulation_1;

	population_2 

	= if (not isInner) then  prePopulation_2 *2.0

	 else population_1;

	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 

	= (idbacteriaPopulation_bacteriaPopulation63_2, population_2, prePopulation_2);

tel

-- Exit action for state :bacteriaPopulation_increasing64

node bacteriaPopulation_increasing64_ex(idbacteriaPopulation_bacteriaPopulation63_1:int;

	isInner:bool)

returns (idbacteriaPopulation_bacteriaPopulation63:int);

var 	idbacteriaPopulation_bacteriaPopulation63_2:int;

let

	-- set state as inactive 

	idbacteriaPopulation_bacteriaPopulation63_2

	 = if (not isInner) then 0 else idbacteriaPopulation_bacteriaPopulation63_1;

	(idbacteriaPopulation_bacteriaPopulation63) 

	= (idbacteriaPopulation_bacteriaPopulation63_1);

tel

-- Entry action for state :bacteriaPopulation_decreasing67

node bacteriaPopulation_decreasing67_en(idbacteriaPopulation_bacteriaPopulation63_1:int;

	population_1:real;

	prePopulation_1:real;

	isInner:bool)

returns (idbacteriaPopulation_bacteriaPopulation63:int;

	population:real;

	prePopulation:real);

var 	idbacteriaPopulation_bacteriaPopulation63_2:int;

	population_2:real;

	prePopulation_2:real;

let

	-- set state as active 

	idbacteriaPopulation_bacteriaPopulation63_2 

	= 67;

	prePopulation_2 

	= if (not isInner) then  population_1 

	 else prePopulation_1;

	population_2 

	= if (not isInner) then  prePopulation_2 /2.0

	 else population_1;

	(idbacteriaPopulation_bacteriaPopulation63, population, prePopulation) 

	= (idbacteriaPopulation_bacteriaPopulation63_2, population_2, prePopulation_2);

tel

-- Exit action for state :bacteriaPopulation_decreasing67

node bacteriaPopulation_decreasing67_ex(idbacteriaPopulation_bacteriaPopulation63_1:int;

	isInner:bool)

returns (idbacteriaPopulation_bacteriaPopulation63:int);

var 	idbacteriaPopulation_bacteriaPopulation63_2:int;

let

	-- set state as inactive 

	idbacteriaPopulation_bacteriaPopulation63_2

	 = if (not isInner) then 0 else idbacteriaPopulation_bacteriaPopulation63_1;

	(idbacteriaPopulation_bacteriaPopulation63) 

	= (idbacteriaPopulation_bacteriaPopulation63_1);

tel

-- Entry action for state :bacteriaPopulation_start66

node bacteriaPopulation_start66_en(idbacteriaPopulation_bacteriaPopulation63_1:int;

	population0:real;

	prePopulation_1:real;

	population_1:real;

	isInner:bool)

returns (idbacteriaPopulation_bacteriaPopulation63:int;

	prePopulation:real;

	population:real);

var 	idbacteriaPopulation_bacteriaPopulation63_2:int;

	prePopulation_2:real;

	population_2:real;

let

	-- set state as active 

	idbacteriaPopulation_bacteriaPopulation63_2 

	= 66;

	prePopulation_2 

	= if (not isInner) then population0

	 else prePopulation_1;

	population_2 

	= if (not isInner) then population0

	 else population_1;

	(idbacteriaPopulation_bacteriaPopulation63, prePopulation, population) 

	= (idbacteriaPopulation_bacteriaPopulation63_2, prePopulation_2, population_2);

tel