Project

General

Profile

« Previous | Next » 

Revision c3af3032

Added by Bourbouh over 3 years ago

add more contracts examples

View differences:

tests/cocospec/ElevatorSpec.lus
1

  
2
--==================
3
-- Simple Elevator 
4
--==================
5

  
6
(*
7
Acknowledgements: This example is inspired by a similar one first made 
8
by Prover Technology AB, then adapted at Chalmers University 
9
by Carl Johan Lillieroth, K.V.S. Prasad, Mary Sheeran, Angela Wallenburg, 
10
and Jan-Willem Roorda. 
11

  
12
-------
13
Setting
14
-------
15

  
16
It models a simple elevator, moving people between two floors. 
17
In the elevator, there are three buttons: 
18
- a button 1 to go to the first floor, 
19
- a button 2 to go to the first floor, and 
20
- a stop switch to stop the elevator. 
21
On each floor, there is a button to call the elevator. 
22

  
23
The elevator has three sensors, 
24
- the first indicating if the elevator is on the first floor or not, 
25
- the second doing the same for the second floor, and 
26
- the third indicating if the elevator's door is closed or not.
27

  
28
The stop switch is located within the elevator and can be pressed to 
29
block the elevator. While the switch is on the elevator stops immediately 
30
if it was moving and ignores any other input. Turning the switch back off 
31
makes the elevator to be responsive again to other inputs.
32

  
33
The elevator is moved up and down by a motor that is on the roof of the 
34
building. The motor is controlled by two signals, 
35
- one for moving the elevator up and 
36
- one for moving it down.
37

  
38
The control system looks at the buttons that are being pressed and the sensors 
39
that say where the elevator is and if the door is open, and then decides if 
40
the motor should move the elevator up or down, or do nothing.
41

  
42
For simplicity, we do not distinguish between the case of someone on floor 1 
43
(resp., 2) pressing the call button and someone in the elevator pressing 
44
the button 1 (resp., 2). 
45

  
46
-------------------
47
Safety Requirements
48
-------------------
49

  
50
The controller is supposed to satisfy the following safety requirements:
51

  
52
R1  The elevator moves only when the door is closed and the stop switch 
53
    is not on.
54
R2  The elevator may not pass the end positions, that is, go through 
55
    the roof or the floor.
56
R3  A moving elevator halts only if the stop switch is on, or the door 
57
    is opened, or the elevator has arrived at the destination floor.
58
R4  The elevator halts before changing direction.
59
R5  The signals sent to the motor are not contradictory.
60
R6  The elevator starts moving when it should. 
61
R7  The elevator stays on a floor indefinitely as long as
62
    there is no call the other floor
63
*)
64

  
65
-------------------------
66
-- Auxiliary operators --
67
-------------------------
68

  
69
node Happened(X : bool) returns (Y : bool);
70
let
71
  Y = X or (false -> pre Y) ;
72
tel
73

  
74
node Since( X, Y : bool ) returns ( Z : bool );
75
let
76
  Z =  X or (Y and (false -> pre Z));
77
tel
78

  
79
node SinceIncl( X, Y : bool ) returns ( Z : bool );
80
let
81
  Z =  Y and (X or (false -> pre Z));
82
tel
83

  
84
node ToInt(X: bool) returns (N: int);
85
let
86
  N = if X then 1 else 0;
87
tel
88

  
89
node MutuallyExcl_4(X1, X2, X3, X4: bool) returns (Y: bool);
90
let
91
  Y = ToInt(X1) + ToInt(X2) + ToInt(X3) + ToInt(X4) < 2 ;
92
tel
93

  
94

  
95
---------------------------------
96
-- Controller high-level specs --
97
---------------------------------
98

  
99
contract ControlReq( Floor_1, Floor_2, DoorOpen, Call_1, Call_2, Stop : bool )
100
returns ( MotorUp, MotorDown : bool);
101
let
102
 
103
  -------------------------------
104
  -- Environmental assumptions --
105
  -------------------------------
106
  -- the elevator starts on the first floor
107
  assume Floor_1 -> true; 
108

  
109
  -- if the elevator was on the first (second) floor and did not move up (down)
110
  -- then it is still on that floor
111
  assume true -> pre (Floor_1 and not MotorUp and not MotorDown) => Floor_1 ; 
112
  assume true -> pre (Floor_2 and not MotorUp and not MotorDown) => Floor_2 ;
113
 (*
114
  -- if the elevator was on the first (second) floor and moved up (down)
115
  -- then it has left that floor
116
  assume true -> pre (Floor_1 and MotorUp) => not Floor_1 ;
117
  assume true -> pre (Floor_2 and MotorDown) => not Floor_2 ;
118
 *)
119
 
120
  -----------
121
  -- Modes --
122
  -----------
123
  mode blocked (
124
    require Stop or DoorOpen ;
125
    ensure not MotorUp ;
126
    ensure not MotorDown ;
127
  );
128
  
129
  mode servicing1 (
130
    require SinceIncl(Call_1, not ::blocked and not Floor_1  
131
                              and not (false -> pre MotorUp) 
132
                              ) ;
133
    ensure MotorDown ;
134
    ensure not MotorUp ;
135
  ) ;
136
  
137
  mode servicing2 (
138
    require SinceIncl(Call_2, not ::servicing1  
139
                              and not ::blocked and not Floor_2  
140
                              and not (false -> pre MotorDown) 
141
                              ) ;
142
    ensure MotorUp ;
143
    ensure not MotorDown ;
144
  ) ;
145

  
146
 mode waiting (
147
    require not ::blocked ;
148
    require not ::servicing1 ;
149
    require not ::servicing2 ;
150
    ensure not MotorUp ;
151
    ensure not MotorDown ;
152
  ) ;
153

  
154

  
155
  -------------------------
156
  -- Auxiliary variables --
157
  -------------------------
158
  
159
  -- Moving is true iff the elevator is moving now
160
  var Moving: bool = MotorUp or MotorDown ;
161
  
162
  -- Halts is true iff the elevator has come to a stop
163
  var Halts: bool = not Moving and (false -> pre Moving);
164

  
165
  -- The elevator can move now iff 
166
  --   the Stop button is not pressed and
167
  --   the door is not closed
168
  var CanMove: bool = not Stop and not DoorOpen;
169
  
170
  -- The elevator should start moving iff 
171
  --   it was not moving before
172
  --   it can move,
173
  --   there is a call to go to a floor, and
174
  --   the elevator is not a that floor
175
    var ShouldMove: bool = (true -> not pre Moving) 
176
                           and CanMove
177
                           and ((Call_1 and not Floor_1) or
178
                                (Call_2 and not Floor_2)) ;
179

  
180
  ----------------
181
  -- Guarantees --
182
  ----------------
183
  -- the execution modes are mutually exclusive  
184
  guarantee MutuallyExcl_4(::blocked, ::servicing1, ::servicing2, ::waiting) ;
185

  
186
  -- R1: The elevator moves only when the door is closed and
187
  --     the Stop button is not pressed
188
  guarantee Moving => not DoorOpen and not Stop;
189

  
190
  -- R2: The elevator will not pass the end positions, that is,
191
  --     go through the roof or the floor.
192
  guarantee (Floor_1 => not MotorDown) ; 
193
  guarantee (Floor_2 => not MotorUp) ;
194

  
195
  -- R3: A moving elevator halts only if
196
  --     the Stop button is pressed, or the door is open, or
197
  --     the elevator has arrived at the destination floor
198
  guarantee Halts => ( Stop 
199
                       or DoorOpen
200
                       or ((true -> pre MotorDown) and Floor_1)
201
                       or ((true -> pre MotorUp) and Floor_2)
202
                       ) ;
203

  
204
  -- R4: he elevator halts before changing direction
205
  guarantee true -> (     not (pre MotorDown and MotorUp)  
206
                      and not (pre MotorUp and MotorDown)
207
                      ) ;
208

  
209
  -- R5: The signals sent to the motor are not contradictory
210
  guarantee not (MotorUp and MotorDown) ;
211

  
212
  -- R6: The elevator starts moving when it should
213
  guarantee ShouldMove => Moving ;
214
 
215
  -- R7: The elevator stays on a floor indefinitely as long as
216
  --     there is no call the other floor
217
  guarantee Since(Floor_1, not Happened(Call_2)) => Floor_1 ;
218
  guarantee Since(Floor_2, not Happened(Call_1)) => Floor_2 ;
219
  
220
 tel
221

  
222

  
223
--------------------------------
224
-- Controller low-level specs --
225
--------------------------------
226

  
227
node Control( Floor_1, Floor_2, DoorOpen, Call_1, Call_2, Stop : bool )
228
returns ( MotorUp, MotorDown : bool) ;
229
(*@ contract import
230
  ControlReq( Floor_1, Floor_2, DoorOpen, Call_1, Call_2, Stop )
231
  returns ( MotorUp, MotorDown ) ;
232
*)
233
var CanMove : bool ;
234
let
235
  CanMove =  not Stop and not DoorOpen ;
236

  
237
(*
238
  The elevator goes down iff all the following hold:
239
  1) there is a call to the first floor or it was already going down
240
  2) it can move
241
  3) it is not on the first floor already
242
  4) it was not going up
243
*)
244
  MotorDown =  (Call_1 or (false -> pre MotorDown)) 
245
               and CanMove 
246
               and not Floor_1
247
               and not (false -> pre MotorUp) ;
248

  
249
(*
250
  The elevator goes up iff all the following hold:
251
  0) it is not going down (i.e., going down takes precedence over going up)
252
  1) there is a call to the second floor or it was already going up
253
  2) it can move
254
  3) it is not on the second floor already
255
  4) it was not going down
256
*)
257
  MotorUp =  not MotorDown 
258
             and (Call_2 or (false -> pre MotorUp))
259
             and CanMove 
260
             and not Floor_2
261
             and not (false -> pre MotorDown) ;
262

  
263
  --%MAIN;
264
tel
265

  
266

  
267

  
268
-- To simulate the elevator system make this the main file first
269

  
270
-- The simulator assumes (for brevity) that it takes 5 execution steps 
271
-- to go from one floor to the other, each corresponding to an intermediate
272
-- "level". Level 0 corresponds to the first floor, level 4 to the second 
273
node Simulator( Call_1, Call_2, Stop, DoorOpen : bool )
274
returns ( Floor_1, Floor_2 : bool ) ;
275
var MotorUp, MotorDown: bool ;
276
    L: int ;
277
let
278
  L = 0 -> if pre MotorUp then pre L + 1
279
           else if pre MotorDown then pre L - 1
280
           else pre L ;
281
  Floor_1 =  L = 0 ;
282
  Floor_2 =  L = 4 ;
283
  
284
  (MotorUp, MotorDown) = Control(Floor_1, Floor_2, DoorOpen, Call_1, Call_2, Stop) ;
285
  -- %MAIN;
286
 tel
287

  
288

  
289

  
290

  
tests/cocospec/StopwatchSpec.lus
46 46
-- Stopwatch high-level spec --
47 47
-------------------------------
48 48

  
49
(*@
49

  
50 50
contract stopwatchSpec ( toggle, reset : bool ) returns ( time : int ) ;
51 51
let
52 52
  -- the watch is activated initially if the toggle button is pressed
......
104 104
    ensure true -> time = pre time ; 
105 105
  ) ;
106 106
tel
107
*)
107

  
108 108

  
109 109
------------------------------
110 110
-- Stopwatch low-level spec --
tests/cocospec/StopwatchSpec2.lus
52 52
-- Stopwatch low-level spec --
53 53
------------------------------
54 54

  
55
node stopwatch ( toggle, reset : bool ) returns ( count : int );
56
(*@
55
node stopwatch ( toggle, reset : bool ) returns ( time : int );
56
(*@contract
57 57
  -- the watch is activated initially if the toggle button is pressed
58 58
  -- afterwards, it is activated iff 
59 59
  --   it was activated before and the toggle button is unpressed or
......
73 73
  
74 74
  -- if there is no reset now and there was an even number of counts since the last reset
75 75
  -- then the current elapsed time is the same as the previous one
76
  guarantee not reset and Since(reset, Even(Count(toggle))) 
76
  var even_count:bool = Even(Count(toggle));
77
  guarantee not reset and Since(reset, even_count) 
77 78
            => Stable(time) ;
78 79
  -- if there is no reset now and there was an odd number of counts since the last reset
79 80
  -- then the current elapsed time is greater than previous one
80
  guarantee not reset and Since(reset, not Even(Count(toggle))) 
81
            => Increased(time) ;
81
  guarantee (not reset) and Since(reset, not even_count)  => Increased(time) ;
82 82

  
83 83

  
84 84
--  guarantee true -> not Even(Count(toggle)) and Count(reset) = 0 => time > pre time ;
......
115 115
  var running : bool;
116 116
let
117 117
  running = (false -> pre running) <> toggle ;
118
  count =
118
  time =
119 119
    if reset then 0
120
    else if running then 1 -> pre count + 1
121
    else 0 -> pre count ;
120
    else if running then 1 -> pre time + 1
121
    else 0 -> pre time ;
122 122
tel
123 123

  
124 124

  
tests/cocospec/bacteria.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/refinement.lus
1
node count (in: bool) returns (cpt: int) ;
2
let
3
  cpt = (if in then 1 else 0) + (0 -> pre cpt) ;
4
tel
5

  
6
node sub (in: bool) returns (cpt: int) ;
7
(*@contract
8
  assume true -> in = not pre in ;
9
  mode begin (
10
    require count(true) <= 10 ;
11
    ensure  cpt >= 0 ;
12
  ) ;
13
  mode and_then (
14
    require not ::begin ;
15
    ensure  true ;
16
  ) ;
17
*)
18
let
19
  cpt = count(in) ;
20
tel
21

  
22
node top (in: bool) returns (cpt: int) ;
23
(*@contract
24
  assume true -> in = not pre in ;
25
  guarantee "sub" cpt >= 0 ;
26
  guarantee "sub" (count(true) > 15) => false ;
27
*)
28
let
29
  cpt = sub(in) ;
30
tel
tests/cocospec/simple-ok.lus
1
node sub (in: int) returns (out: int);
2
--@mode contract_sub ;
3
--@require in > 0 ;
4
--@ensure out >= 0 ;
5
let
6
  out = 0 -> in + pre out ;
7
  -- Does not hold
8
  --%PROPERTY out >= 0 ;
9
tel
10

  
11
node top (in: int; clk: bool) returns (out: int);
12
--@mode contract_top ;
13
--@require in >= 0 ;
14
--@ensure true -> out >= 0 ;
15
var mem: int ;
16
let
17
  mem = 1 -> in + pre mem ;
18
  out = sub(mem) ;
19
  --%PROPERTY true -> out > pre out ;
20
tel

Also available in: Unified diff