1


2

 First(X) is the constant stream consisting of the first value of X

3

node first( X : real ) returns ( Y : real );

4

let

5

Y = X > pre Y;

6

tel

7


8

 HasHappened(X) is true iff X has been true at some point

9

node hasHappened(X : bool) returns (Y : bool);

10

let

11

Y = X or (false > pre Y);

12

tel

13


14

 Sofar(X) is true at any point iff X has been true from

15

 the beginning until that point

16

node sofar( X : bool ) returns ( Y : bool );

17

let

18

Y = X > (X and (pre Y));

19

tel

20


21



22

 bacteria Population specs

23



24

(*@ contract bacteriaPopulationSpec(p: real) returns(population: real);

25

let

26

 the maximum population size in the environment

27

const environmentCapacity : real = 32.0;

28


29

 the initial size of the population

30

var initialPopulation:real = first(p);

31


32

 the initial population is greater than zero

33

assume initialPopulation > 0.0;

34


35

 the population will always be positive

36

guarantee population > 0.0;

37


38

 initially the population is equal to the initial population

39

guarantee population = initialPopulation > true;

40


41

 if the population increases at some time, and both the previous population

42

 and the current population are smaller than the capacity, then

43

 so far the population has been growing

44

guarantee true > hasHappened(true > pre population < population)

45

and pre population < environmentCapacity

46

and population < environmentCapacity

47

=> sofar(true > pre population < population);

48


49

 if the population descreases at some time, and both the previous population

50

 and the current population are larger than the capacity, then

51

 so far the population has been declining

52

guarantee true > hasHappened(true > pre population > population)

53

and pre population > environmentCapacity

54

and population > environmentCapacity

55

=> sofar(true > pre population > population);

56


57

mode increasing (

58

 the previous population is smaller than the capacity

59

require true > pre population < environmentCapacity ;

60


61

 The current population is strictly larger than previous population

62

 if the latter is smaller than the capacity

63

ensure true > pre population < population;

64

) ;

65


66

mode decreasing (

67

 the previous population is larger than the capacity

68

require true > pre population > environmentCapacity ;

69


70

 The current population is strictly smaller than previous population

71

 if the latter is larger than the capacity

72

ensure true > pre population > population;

73

);

74


75

mode stable (

76

 the previous population is the same as the enviroment capacity

77

require true > pre population = environmentCapacity ;

78


79

 The current population is the same as the previous population

80

ensure true > population = pre population;

81

) ;

82

tel

83

*)

84


85

 This node simulates bacteria population growth over time

86

 input : population size at time 0

87

 output: population size at time t assuming exponential growth/decline

88

 within an environment that has a carrying capacity

89

 const environmentCapacity : real = 32.0;

90

const environmentCapacity = 32.0;

91

node bacteriaPopulation(population0: real) returns(population: real);

92

(*@contract import bacteriaPopulationSpec(population0) returns (population) ; *)

93

 const environmentCapacity : real = 32.0;

94

let

95

population = population0 >

96

if (pre population < environmentCapacity) then pre population * 2.0

97

else if (pre population > environmentCapacity) then pre population * 0.5

98

else pre population;

99

tel

100


101


102

