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

(*@

25

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

26

let

27

 the maximum population size in the environment

28

const environmentCapacity : real = 32.0;

29


30

 the initial size of the population

31

var initialPopulation:real = first(p);

32


33

 the initial population is greater than zero

34

assume initialPopulation > 0.0;

35


36

 the population will always be positive

37

guarantee population > 0.0;

38


39

 initially the population is equal to the initial population

40

guarantee population = initialPopulation > true;

41


42

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

43

 and the current population are smaller than the capacity, then

44

 so far the population has been growing

45

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

46

and pre population < environmentCapacity

47

and population < environmentCapacity

48

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

49


50

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

51

 and the current population are larger than the capacity, then

52

 so far the population has been declining

53

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

54

and pre population > environmentCapacity

55

and population > environmentCapacity

56

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

57


58

mode increasing (

59

 the previous population is smaller than the capacity

60

require true > pre population < environmentCapacity ;

61


62

 The current population is strictly larger than previous population

63

 if the latter is smaller than the capacity

64

ensure true > pre population < population;

65

) ;

66


67

mode decreasing (

68

 the previous population is larger than the capacity

69

require true > pre population > environmentCapacity ;

70


71

 The current population is strictly smaller than previous population

72

 if the latter is larger than the capacity

73

ensure true > pre population > population;

74

);

75


76

mode stable (

77

 the previous population is the same as the enviroment capacity

78

require true > pre population = environmentCapacity ;

79


80

 The current population is the same as the previous population

81

ensure true > population = pre population;

82

) ;

83

tel

84

*)

85


86

 This node simulates bacteria population growth over time

87

 input : population size at time 0

88

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

89

 within an environment that has a carrying capacity

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

