Project

General

Profile

Download (3.63 KB) Statistics
| Branch: | Tag: | Revision:
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
-- This node simulates bacteria population growth over time
85
-- input : population size at time 0
86
-- output: population size at time t assuming exponential growth/decline
87
--         within an environment that has a carrying capacity
88

    
89
node bacteriaPopulation(population0: real) returns(population: real);
90
(*@contract import bacteriaPopulationSpec(population0) returns (population) ; *)
91
    const  environmentCapacity : real = 32.0;
92
let
93
   population =  population0 ->  
94
                if (pre population  < environmentCapacity) then pre population * 2.0
95
                else if (pre population  > environmentCapacity) then pre population * 0.5
96
                else pre population;
97
tel
98

    
99

    
100

    
(1-1/16)