LiftPlant: Properties

    
SENSORS

The sensors cannot communicate two different data simultaneously;
recall that in the property  "X incompatible with Y" it is implicitly assumed that "X" is different from "Y".

    CABINPOSITION(f1) incompatible with CABINPOSITION(f2)
    DOORPOSITION(f,dps1) incompatible with DOORPOSITION(f,dps2)
    MOTORSTATUS(ms1) incompatible with MOTORSTATUS(ms2)
    USERINSIDE(b) incompatible with 
    USERINSIDE(b')

The sensors always communicate the correct data.

    if CABINPOSITION(f) happen then cabinPosition = f
    if DOORPOSITION(f,dps) happen then doorPosition(f) = dps
    if MOTORSTATUS(ms) happen then motorStatus = ms
    if USERINSIDE(b) happen then b = (userInside ≠ 0)
 
The sensors never break down, thus they are always able to communicate the correct data.   
  
    in one case next CABINPOSITION(cabinPosition) happen
    in one case next DOORPOSITION(f,doorPosition(f)) happen
    in one case next MOTORSTATUS(motorStatus) happen
    in one case next USERINSIDE(userInside ≠ 0) happen  

The sensors and the devices for receiving the orders are independent, 
that is  they can send their data and receive the orders also simultaneously. 

Motor and door orders may be received simultaneously.  


DOORS


No two door orders may be received simultaneously.
              	
    OPENDOOR(f1) incompatible with OPENDOOR(f2)
    OPENDOOR(f1) incompatible with CLOSEDOOR(f2)
    CLOSEDOOR(f1) incompatible with CLOSEDOOR(f2) 
  
The open door at floor f order can be executed only when the motor is stopped, the 
cabin is  at floor f, and the doors at all the other floors are closed
(thus also if the door at f is already open), and it is always correctly executed.

    if OPENDOOR(f) happen then 
        motorStatus = stop  and  cabinPosition = f and
        for all f' • if f ≠ f' then doorPosition(f') = closed and
        doorPosition'(f) = open

Whenever the open door order may be executed, it can be received  
   
    if motorStatus = stop  and  cabinPosition = f and
       for all f' • if f ≠ f' then doorPosition(f') = closed then
            in one case next OPENDOOR(f) happen
     
The close door at floor f order can be executed only when the motor is stopped and the cabin is  at floor f
(thus also if the door at f is already open), and it is always correctly executed.
     	   
    if CLOSEDOOR(f) happen then 
        motorStatus = stop  and  cabinPosition = f and
        doorPosition'(f) = closed

Whenever the close door order may be executed, it can be received.
    
    if motorStatus = stop  and  cabinPosition = f  then
        in one case next CLOSEDOOR(f) happen
    
The  door at floor f can be open only when the cabin is at f.    
    if doorPosition(f) = open then cabinPosition = f
        
The door at f becomes closed /open only if the corresponding order is executed.
    
    if doorPosition(f) = open and doorPosition'(f) = closed then
        CLOSEDOOR(f) happen
    
    if doorPosition(f) = closed and doorPosition'(f) = open then
        OPENDOOR(f) happen


MOTOR & CABIN


No two motor orders may be received simultaneously.

    MOTORSTOP incompatible with MOTORDOWN
    MOTORSTOP incompatible with MOTORUP
    MOTORDOWN incompatible with MOTORUP
    
The motor stop order can be always executed, and it is always correctly 
executed stopping immediately the cabin.

    if MOTORSTOP happen then 
        motorStatus' =  stop and  cabinPosition' = cabinPosition
      
The  motor stop order can be always be received.
    
    in one case next MOTORSTOP happen

The  motor up order can be executed only when the motor is stopped and the cabin is not at the top floor
(while the doors may be in any position), and it is always correctly executed.
                 	
     if MOTORUP happen then 
          motorStatus = stop and cabinPosition ≠ top and
          motorStatus' = up    
   
If the motor is stopped and the cabin is not at the top floor, the  motor up 
order can be  received.

    if motorStatus = stop and cabinPosition ≠ top then
        in one case next MOTORUP happen    
    
The  motor down order can be executed only when the motor is stopped and the cabin is not at the ground floor
(while the doors may be in any position), and it is always correctly executed.

    if MOTORDOWN happen then 
        motorStatus = stop and cabinPosition ≠ ground and 
        motorStatus' = down

If the motor is stopped and the cabin is not at the ground floor, then the  motor down order can be  received.
  
    if motorStatus = stop and cabinPosition ≠ ground then
        in one case next MOTORDOWN happen

The cabin changes position only if the motor is moving up/down.
    	
    if cabinPosition ≠ cabinPosition' then
        (cabinPosition' = next(cabinPosition) and motorStatus = up) or
        (cabinPosition' = previous(cabinPosition) and motorStatus = down)
    
If the motor is moving up/down, then the cabin changes position.  
   
    if motorStatus = up then in any case next cabinPosition = next(cabinPosition) 
    if motorStatus = down then in any case next cabinPosition = previous(cabinPosition)
    
The motor changes its status only when it receive the corresponding order.

    if motorStatus = stop and motorStatus' = up then
        MOTORUP happen
    
    if motorStatus = stop and motorStatus' = down then
        MOTORDOWN happen
    
    if motorStatus ≠ stop and motorStatus' = stop then
        MOTORSTOP happen
    


USERS


The phisical limits of the cabin is five persons.
   
   userInside >= 0 and userInside =< 5
   
User may enter/leaving the cabin only when the cabin is stopped at a floor with open doors.

   if userInside ≠ userInside' = then
      exists f s.t. doorPosition(f) = open and cabinPosition = f and motorStatus = Stop
    
It is assumed that in any case eventually the users will leave the cabin; 
this information helps understand the typical user behaviour.
   
    if userInside ≠ 0 then in any case eventually userInside = 0

LiftPlant: CASL_LTL Specification

spec ELEMINTER =
free type elemInter ::=
     CABINPOSITION(Floor) |
     OPENDOOR(Floor) |
     CLOSEDOOR(Floor) |
     DOORPOSITION(Floor,DoorPosition) |
     MOTORUP |
     MOTORDOWN |
     MOTORSTOP |
     MOTORSTATUS(MotorStatus) |
     USERINSIDE(Bool)

spec LiftPlant =
     FINITESET[ ELEMINTER] and Floor and MotorStatus and DoorPosition  then
     dsort St  label FiniteSet[elemInter]
     ops cabinPosition: St -> Floor
         doorPosition: St x Floor -> DoorPosition
         motorStatus: St -> MotorStatus
         usersInside:St -> Int
     axioms

%% SENSORS

%% The sensors cannot communicate two different data simultaneously;
%% recall that in the property  "X incompatible with Y" it is implicitly assumed that "X" is different from "Y".

    not (f1 = f2)  and  S -- L --> S'  =>
        not(CABINPOSITION(f1) in L  and  CABINPOSITION(f2) in L)
    not (dps1 = dps2)  and  S -- L --> S'  =>
        not(DOORPOSITION(f,dps1) in L  and  DOORPOSITION(f,dps2) in L)
    not (ms1 = ms2)  and  S -- L --> S'  =>
        not(MOTORSTATUS(ms1) in L  and  MOTORSTATUS(ms2) in L)
    not (b = b')  and  S -- L --> S'  =>
        not(USERINSIDE(b) in L  and  
        USERINSIDE(b') in L)

%% The sensors always communicate the correct data.

    S -- L --> S'  and  CABINPOSITION(f) in L  => cabinPosition(S) = f
    S -- L --> S'  and  DOORPOSITION(f,dps) in L  => doorPosition(S,f) = dps
    S -- L --> S'  and  MOTORSTATUS(ms) in L  =>  motorStatus(S) = ms
    S -- L --> S'  and  USERINSIDE(b) in L  =>  
    b = (userInside(S) ≠ 0)
 
%% The sensors never break down, thus they are always able to communicate the correct data.   
  
    in_one_case(S, next < L • CABINPOSITION(cabinPosition(S)) in L >)
    in_one_case(S, next < L •  DOORPOSITION(f,doorPosition(S,f)) in L >)
    in_one_case(S, next < L •  MOTORSTATUS(motorStatus(S)) in L >)
    in_one_case(S, next < L • USERINSIDE(userInside(S) ≠ 0) in L >)  

%% The sensors and the devices for receiving the orders are independent, 
%% that is  they can send their data and receive the orders also simultaneously. 

%% Motor and door orders may be received simultaneously.  


%% DOORS


%% No two door orders may be received simultaneously.
              	
    not (f1 = f2)  and  S -- L --> S'  =>
        not(OPENDOOR(f1) in L  and  OPENDOOR(f2) in L)
    S -- L --> S'  =>
        not(OPENDOOR(f1) in L  and  CLOSEDOOR(f2) in L)
    not (f1 = f2)  and  S -- L --> S'  =>
        not(CLOSEDOOR(f1) in L  and  CLOSEDOOR(f2) in L)
  
%% The open door at floor f order can be executed only when the motor is stopped, the 
%% cabin is  at floor f, and the doors at all the other floors are closed
%% (thus also if the door at f is already open), and it is always correctly executed.

    S -- L --> S'  and  OPENDOOR(f) in L  => 
        motorStatus(S) = stop  and  cabinPosition(S) = f  and  
        for all f' • if f ≠ f'  => doorPosition(S,f') = closed  and  
        doorPosition(S',f) = open

%% Whenever the open door order may be executed, it can be received  
   
    S -- L --> S'  and  motorStatus(S) = stop  and  cabinPosition(S) = f  and  
    (for all f' • if f ≠ f'  =>  doorPosition(S,f') = closed)  =>  
        in_one_case(S, next < L •  OPENDOOR(f) in L >)
     
%% The close door at floor f order can be executed only when the motor is stopped and the cabin is  at floor f
%% (thus also if the door at f is already open), and it is always correctly executed.
     	   
    S -- L --> S'  and  CLOSEDOOR(f) in L  =>  
        motorStatus(S) = stop  and  cabinPosition(S) = f  and  
        doorPosition(S',f) = closed

%% Whenever the close door order may be executed, it can be received.
    
    S -- L --> S'  and  motorStatus(S) = stop  and  cabinPosition(S) = f   =>  
        in_one_case(S, next < L •  CLOSEDOOR(f) in L >)
    
%% The  door at floor f can be open only when the cabin is at f.    
    doorPosition(S,f) = open  =>  cabinPosition(S) = f
        
%% The door at f becomes closed /open only if the corresponding order is executed.
    
    S -- L --> S'  and  doorPosition(S,f) = open  and  doorPosition(S',f) = closed  =>  
        CLOSEDOOR(f) in L
    
    S -- L --> S'  and  doorPosition(S,f) = closed  and  doorPosition(S',f) = open  =>  
        OPENDOOR(f) in L


%% MOTOR & CABIN


%% No two motor orders may be received simultaneously.

    S -- L --> S'  =>
        not(MOTORSTOP in L  and  MOTORDOWN in L)
    S -- L --> S'  =>  
        not(MOTORSTOP in L  and  MOTORUP in L)
    S -- L --> S'  =>  
        not(MOTORDOWN in L  and  MOTORUP in L)
    
%% The motor stop order can be always executed, and it is always correctly 
%% executed stopping immediately the cabin.

    S -- L --> S'  and  MOTORSTOP in L  =>  
        motorStatus(S') =  stop  and  cabinPosition(S') = cabinPosition(S)
      
%% The  motor stop order can be always be received.
    
    in_one_case(S, next < L •  MOTORSTOP in L >)

%% The  motor up order can be executed only when the motor is stopped and the cabin is not at the top floor
%% (while the doors may be in any position), and it is always correctly executed.
                 	
    S -- L --> S'  and  MOTORUP in L  =>  
          motorStatus(S) = stop  and  cabinPosition(S) ≠ top  and  
          motorStatus(S') = up    
   
%% If the motor is stopped and the cabin is not at the top floor, the  motor up 
%% order can be  received.

    motorStatus(S) = stop  and  cabinPosition(S) ≠ top  =>  
        in_one_case(S, next < L •  MOTORUP in L >)    
    
%% The  motor down order can be executed only when the motor is stopped and the cabin is not at the ground floor
%% (while the doors may be in any position), and it is always correctly executed.

    S -- L --> S'  and  MOTORDOWN in L  =>  
        motorStatus(S) = stop  and  cabinPosition(S) ≠ ground  and  
        motorStatus(S') = down

%% If the motor is stopped and the cabin is not at the ground floor, if the  motor down order can be  received.
  
    motorStatus(S) = stop  and  cabinPosition(S) ≠ ground  =>  
        in_one_case(S, next < L •  MOTORDOWN in L >)

%% The cabin changes position only if the motor is moving up/down.
    	
    S -- L --> S'  and  cabinPosition(S) ≠ cabinPosition(S')  =>  
        (cabinPosition(S') = next((cabinPosition(S))  and  motorStatus(S) = up) or
        (cabinPosition(S') = previous(cabinPosition(S))  and  motorStatus(S) = down)
    
%% If the motor is moving up/down,  =>  the cabin changes position.  
   
    motorStatus(S) = up  =>  in_any_case(S, next < S • cabinPosition(S) =  next(cabinPosition(S))>)
    motorStatus(S) = down  =>  in_any_case(S, next < S • cabinPosition(S) = previous(cabinPosition(S))>)
    
%% The motor changes its status only when it receive the corresponding order.

    S -- L --> S'  and  motorStatus(S) = stop  and  motorStatus(S') = up  =>  
        MOTORUP in L
    
    S -- L --> S'  and  motorStatus(S) = stop  and  motorStatus(S') = down  =>  
        MOTORDOWN in L
    
    S -- L --> S'  and  motorStatus(S) ≠ stop  and  motorStatus(S') = stop  =>  
        MOTORSTOP in L
    


USERS


%% The phisical limits of the cabin is five persons.
   
   userInside(S) >= 0  and  userInside(S) =< 5
   
%% User may enter/leaving the cabin only when the cabin is stopped at a floor with open doors.

    S -- L --> S'  and  userInside(S) ≠ userInside(S')  =>  
      exists f • doorPosition(S,f) = open  and  cabinPosition(S) = f  and  motorStatus(S) = Stop
    
%% It is assumed that in any case eventually the users will leave the cabin; 
%% this information helps understand the typical user behaviour.
   
    userInside(S) ≠ 0  =>  in_any_case(S, eventually  < S • userInside(S) = 0>)