Project

General

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