CristalCaveGem » LustreC » Lustrec-Tests

--==================

-- Simple Elevator 

--==================

(*

Acknowledgements: This example is inspired by a similar one first made 

by Prover Technology AB, then adapted at Chalmers University 

by Carl Johan Lillieroth, K.V.S. Prasad, Mary Sheeran, Angela Wallenburg, 

and Jan-Willem Roorda. 

-------

Setting

-------

It models a simple elevator, moving people between two floors. 

In the elevator, there are three buttons: 

- a button 1 to go to the first floor, 

- a button 2 to go to the first floor, and 

- a stop switch to stop the elevator. 

On each floor, there is a button to call the elevator. 

The elevator has three sensors, 

- the first indicating if the elevator is on the first floor or not, 

- the second doing the same for the second floor, and 

- the third indicating if the elevator's door is closed or not.

The stop switch is located within the elevator and can be pressed to 

block the elevator. While the switch is on the elevator stops immediately 

if it was moving and ignores any other input. Turning the switch back off 

makes the elevator to be responsive again to other inputs.

The elevator is moved up and down by a motor that is on the roof of the 

building. The motor is controlled by two signals, 

- one for moving the elevator up and 

- one for moving it down.

The control system looks at the buttons that are being pressed and the sensors 

that say where the elevator is and if the door is open, and then decides if 

the motor should move the elevator up or down, or do nothing.

For simplicity, we do not distinguish between the case of someone on floor 1 

(resp., 2) pressing the call button and someone in the elevator pressing 

the button 1 (resp., 2). 

-------------------

Safety Requirements

-------------------

The controller is supposed to satisfy the following safety requirements:

R1  The elevator moves only when the door is closed and the stop switch 

    is not on.

R2  The elevator may not pass the end positions, that is, go through 

    the roof or the floor.

R3  A moving elevator halts only if the stop switch is on, or the door 

    is opened, or the elevator has arrived at the destination floor.

R4  The elevator halts before changing direction.

R5  The signals sent to the motor are not contradictory.

R6  The elevator starts moving when it should. 

R7  The elevator stays on a floor indefinitely as long as

    there is no call the other floor

*)

-------------------------

-- Auxiliary operators --

-------------------------

node Happened(X : bool) returns (Y : bool);

let

  Y = X or (false -> pre Y) ;

tel

node Since( X, Y : bool ) returns ( Z : bool );

let

  Z =  X or (Y and (false -> pre Z));

tel

node SinceIncl( X, Y : bool ) returns ( Z : bool );

let

  Z =  Y and (X or (false -> pre Z));

tel

node ToInt(X: bool) returns (N: int);

let

  N = if X then 1 else 0;

tel

node MutuallyExcl_4(X1, X2, X3, X4: bool) returns (Y: bool);

let

  Y = ToInt(X1) + ToInt(X2) + ToInt(X3) + ToInt(X4) < 2 ;

tel

---------------------------------

-- Controller high-level specs --

---------------------------------

(*@ 

contract ControlReq( Floor_1, Floor_2, DoorOpen, Call_1, Call_2, Stop : bool )

returns ( MotorUp, MotorDown : bool);

let

  -------------------------------

  -- Environmental assumptions --

  -------------------------------

  -- the elevator starts on the first floor

  assume Floor_1 -> true; 

  -- if the elevator was on the first (second) floor and did not move up (down)

  -- then it is still on that floor

  assume true -> pre (Floor_1 and not MotorUp and not MotorDown) => Floor_1 ; 

  assume true -> pre (Floor_2 and not MotorUp and not MotorDown) => Floor_2 ;

 (*

  -- if the elevator was on the first (second) floor and moved up (down)

  -- then it has left that floor

  assume true -> pre (Floor_1 and MotorUp) => not Floor_1 ;

  assume true -> pre (Floor_2 and MotorDown) => not Floor_2 ;

 *)

  -----------

  -- Modes --

  -----------

  mode blocked (

    require Stop or DoorOpen ;

    ensure not MotorUp ;

    ensure not MotorDown ;

  );

  mode servicing1 (

    require SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  

                              and not (false -> pre MotorUp) 

                              ) ;

    ensure MotorDown ;

    ensure not MotorUp ;

  ) ;

  mode servicing2 (

    require SinceIncl(Call_2, not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  

                              and not (false -> pre MotorUp)))  

                              and not (Stop or DoorOpen) and not Floor_2  

                              and not (false -> pre MotorDown) 

                              ) ;

    ensure MotorUp ;

    ensure not MotorDown ;

  ) ;

 mode waiting (

    require not (Stop or DoorOpen) ;

    require not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  

                              and not (false -> pre MotorUp))) ;

    require not (SinceIncl(Call_2, not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  

                              and not (false -> pre MotorUp)))  

                              and not (Stop or DoorOpen) and not Floor_2  

                              and not (false -> pre MotorDown) 

                              )) ;

    ensure not MotorUp ;

    ensure not MotorDown ;

  ) ;

  -------------------------

  -- Auxiliary variables --

  -------------------------

  -- Moving is true iff the elevator is moving now

  var Moving: bool = MotorUp or MotorDown ;

  -- Halts is true iff the elevator has come to a stop

  var Halts: bool = not Moving and (false -> pre Moving);

  -- The elevator can move now iff 

  --   the Stop button is not pressed and

  --   the door is not closed

  var CanMove: bool = not Stop and not DoorOpen;

  -- The elevator should start moving iff 

  --   it was not moving before

  --   it can move,

  --   there is a call to go to a floor, and

  --   the elevator is not a that floor

    var ShouldMove: bool = (true -> not pre Moving) 

                           and CanMove

                           and ((Call_1 and not Floor_1) or

                                (Call_2 and not Floor_2)) ;

  ----------------

  -- Guarantees --

  ----------------

  -- the execution modes are mutually exclusive  

  guarantee MutuallyExcl_4((Stop or DoorOpen), (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  

                              and not (false -> pre MotorUp))), (SinceIncl(Call_2, not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  

                              and not (false -> pre MotorUp)))  

                              and not (Stop or DoorOpen) and not Floor_2  

                              and not (false -> pre MotorDown) 

                              )), (not (Stop or DoorOpen) and 

    not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  

                              and not (false -> pre MotorUp))) and

    not (SinceIncl(Call_2, not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  

                              and not (false -> pre MotorUp)))  

                              and not (Stop or DoorOpen) and not Floor_2  

                              and not (false -> pre MotorDown) 

                              )))) ;

  -- R1: The elevator moves only when the door is closed and

  --     the Stop button is not pressed

  guarantee Moving => not DoorOpen and not Stop;

  -- R2: The elevator will not pass the end positions, that is,

  --     go through the roof or the floor.

  guarantee (Floor_1 => not MotorDown) ; 

  guarantee (Floor_2 => not MotorUp) ;

  -- R3: A moving elevator halts only if

  --     the Stop button is pressed, or the door is open, or

  --     the elevator has arrived at the destination floor

  guarantee Halts => ( Stop 

                       or DoorOpen

                       or ((true -> pre MotorDown) and Floor_1)

                       or ((true -> pre MotorUp) and Floor_2)

                       ) ;

  -- R4: he elevator halts before changing direction

  guarantee true -> (     not (pre MotorDown and MotorUp)  

                      and not (pre MotorUp and MotorDown)

                      ) ;

  -- R5: The signals sent to the motor are not contradictory

  guarantee not (MotorUp and MotorDown) ;

  -- R6: The elevator starts moving when it should

  guarantee ShouldMove => Moving ;

  -- R7: The elevator stays on a floor indefinitely as long as

  --     there is no call the other floor

  guarantee Since(Floor_1, not Happened(Call_2)) => Floor_1 ;

  guarantee Since(Floor_2, not Happened(Call_1)) => Floor_2 ;

 tel

*)

--------------------------------

-- Controller low-level specs --

--------------------------------

node Control( Floor_1, Floor_2, DoorOpen, Call_1, Call_2, Stop : bool )

returns ( MotorUp, MotorDown : bool) ;

(*@ contract import

  ControlReq( Floor_1, Floor_2, DoorOpen, Call_1, Call_2, Stop )

  returns ( MotorUp, MotorDown ) ;

*)

var CanMove : bool ;

let

  CanMove =  not Stop and not DoorOpen ;

(*

  The elevator goes down iff all the following hold:

  1) there is a call to the first floor or it was already going down

  2) it can move

  3) it is not on the first floor already

  4) it was not going up

*)

  MotorDown =  (Call_1 or (false -> pre MotorDown)) 

               and CanMove 

               and not Floor_1

               and not (false -> pre MotorUp) ;

(*

  The elevator goes up iff all the following hold:

  0) it is not going down (i.e., going down takes precedence over going up)

  1) there is a call to the second floor or it was already going up

  2) it can move

  3) it is not on the second floor already

  4) it was not going down

*)

  MotorUp =  not MotorDown 

             and (Call_2 or (false -> pre MotorUp))

             and CanMove 

             and not Floor_2

             and not (false -> pre MotorDown) ;

  --%MAIN;

tel

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

-- The simulator assumes (for brevity) that it takes 5 execution steps 

-- to go from one floor to the other, each corresponding to an intermediate

-- "level". Level 0 corresponds to the first floor, level 4 to the second 

node Simulator( Call_1, Call_2, Stop, DoorOpen : bool )

returns ( Floor_1, Floor_2 : bool ) ;

var MotorUp, MotorDown: bool ;

    L: int ;

let

  L = 0 -> if pre MotorUp then pre L + 1

           else if pre MotorDown then pre L - 1

           else pre L ;

  Floor_1 =  L = 0 ;

  Floor_2 =  L = 4 ;

  (MotorUp, MotorDown) = Control(Floor_1, Floor_2, DoorOpen, Call_1, Call_2, Stop) ;

  -- %MAIN;

 tel