### Profile

« Previous | Next »

## Revision dd2eeba6

#### Added by Bourbouh almost 3 years ago

add another contract example

View differences:

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

tests/cocospec/StopwatchSpecV2.lus
1
```-------------------------
```
2
```-- Auxiliary operators --
```
3
```-------------------------
```
4
```node Even (N: int) returns (B: bool) ;
```
5
```let
```
6
```  B = (N mod 2 = 0) ;
```
7
```tel
```
8

9
```node ToInt (X: bool) returns (N: int) ;
```
10
```let
```
11
```  N = if X then 1 else 0 ;
```
12
```tel
```
13

14
```node Count (X: bool) returns (N: int) ;
```
15
```let
```
16
```  N = ToInt(X) -> ToInt(X) + pre N ;
```
17
```tel
```
18

19
```node Sofar ( X : bool ) returns ( Y : bool ) ;
```
20
```let
```
21
``` Y = X -> (X and (pre Y)) ;
```
22
```tel
```
23

24
```node Since ( X, Y : bool ) returns ( Z : bool ) ;
```
25
```let
```
26
```  Z =  X or (Y and (false -> pre Z)) ;
```
27
```tel
```
28

29

30
```node SinceIncl ( X, Y : bool ) returns ( Z : bool ) ;
```
31
```let
```
32
```  Z =  Y and (X or (false -> pre Z)) ;
```
33
```tel
```
34

35
```node Increased (N: int) returns (B: bool) ;
```
36
```let
```
37
```  B = true -> N > pre N ;
```
38
```tel
```
39

40
```node Stable (N: int) returns (B: bool) ;
```
41
```let
```
42
```  B = true -> N = pre N ;
```
43
```tel
```
44

45
```-------------------------------
```
46
```-- Stopwatch high-level spec --
```
47
```-------------------------------
```
48

49

50
```(*contract stopwatchSpec ( toggle, reset : bool ) returns ( time : int ) ;
```
51
```let
```
52
```  -- the watch is activated initially if the toggle button is pressed
```
53
```  -- afterwards, it is activated iff
```
54
```  --   it was activated before and the toggle button is unpressed or
```
55
```  --   it was not activated before and the toggle button is pressed
```
56
```  var on: bool = toggle ->    (pre on and not toggle)
```
57
```                           or (not pre on and toggle) ;
```
58
```
```
59
```  -- we can assume that the two buttons are never pressed together
```
60
```  assume not (toggle and reset) ;
```
61
```
```
62
```  -- the elapsed time starts at 1 or 0 depending
```
63
```  -- on whether the watch is activated or not
```
64
```  guarantee (on => time = 1) -> true ;
```
65
```  guarantee (not on => time = 0) -> true ;
```
66
```  -- the elapsed time is always non-negative
```
67
```  guarantee time >= 0 ;
```
68
```
```
69
```  -- if there is no reset now and there was an even number of counts since the last reset
```
70
```  -- then the current elapsed time is the same as the previous one
```
71
```  guarantee not reset and Since(reset, Even(Count(toggle)))
```
72
```            => Stable(time) ;
```
73
```  -- if there is no reset now and there was an odd number of counts since the last reset
```
74
```  -- then the current elapsed time is greater than previous one
```
75
```  guarantee not reset and Since(reset, not Even(Count(toggle)))
```
76
```            => Increased(time) ;
```
77

78

79
```--  guarantee true -> not Even(Count(toggle)) and Count(reset) = 0 => time > pre time ;
```
80

81
```
```
82
```  -- the watch is in resetting mode if the reset button is pressed
```
83
```  -- while in that mode, the elapsed time is 0
```
84
```  mode resetting (
```
85
```    require reset ;
```
86
```    ensure time = 0 ;
```
87
```  ) ;
```
88

89
```  -- the watch is in running mode if is activated and
```
90
```  -- the reset button is unpressed.
```
91
```  -- while in that mode, the elapsed time increases by 1
```
92
```  mode running (
```
93
```    require on ;
```
94
```    require not reset ;
```
95
```    ensure true -> time = pre time + 1 ;
```
96
```  ) ;
```
97

98
```  -- the watch is in stopped mode if is not activated and
```
99
```  -- the reset button is unpressed
```
100
```  -- while in that mode, the elapsed time remains the same
```
101
```  mode stopped (
```
102
```    require not reset ;
```
103
```    require not on ;
```
104
```    ensure true -> time = pre time ;
```
105
```  ) ;
```
106
```tel
```
107
```*)
```
108

109
```------------------------------
```
110
```-- Stopwatch low-level spec --
```
111
```------------------------------
```
112

113
```node stopwatch ( toggle, reset : bool ) returns ( count : int );
```
114
```(*@contract import stopwatchSpec(toggle, reset ) returns (count) ; *)
```
115
```  var running : bool;
```
116
```let
```
117
```  running = (false -> pre running) <> toggle ;
```
118
```  count =
```
119
```    if reset then 0
```
120
```    else if running then 1 -> pre count + 1
```
121
```    else 0 -> pre count ;
```
122
```tel
```
123

124

125

126

127

tests/lusic/test2.lusi
1
```(* Generated Lustre Interface file from test2.lusi *)
```
2
```(* by Lustre-C compiler version 323, 2014/6/23, 18:25:31 *)
```
3
```(* Feel free to mask some of the definitions by removing them from this file. *)
```
4

5
```type toto = enum {Up, Down };
```
6

7
```const titi = [1,2];
```
8

1
```(* Generated Lustre Interface file from test2.lus *)
```
2
```(* by Lustre-C compiler version 1.5-     837-master, 2018/9/28, 06:01:24 *)
```
3
```(* Feel free to mask some of the definitions by removing them from this file. *)
```
4

5
```type toto = enum {Up, Down };
```
6

7
```const titi = [1,2];
```
8

9

Also available in: Unified diff