Lift System: Properties

CALL(f1) incompatible with CALL(f2)
No two calls may be received simultaneously

     if CALL(f) happen then
     in any case eventually LP.cabinPosition = f and 
                            LP.motorStatus = stop and 
                            LP.doorPosition(f) = open
Any received call for a given floor will be eventually satisfied in any case

     in any case eventually in one case CALL(f) happen

In any case eventually the lisft system will be able to receive a call for a given floor

    if CALL(f) happen  then CN.CALL(f) happen
    if CN.CALL(f) happen  then CALL(f)

The calls are received by the controller
	
if LP.CABINPOSITION(f) happen then CN.CABINPOSITION(f) happen  
if CN.CABINPOSITION(f) happen  then LP.CABINPOSITION(f) happen   
     	
if LP.DOORPOSITION(f,dps) happen then CN.DOORPOSITION(f,dps) happen 
if CN.DOORPOSITION(f,dps) happen  then LP.DOORPOSITION(f,dps) happen   
    	
if LP.MOTORSTATUS(ms) happen then CN.MOTORSTATUS(ms) happen  
if CN.MOTORSTATUS(ms) happen  then LP.MOTORSTATUS(ms) happen   
 
if LP.CLOSEDOOR(f) happen then CN.CLOSEDOOR(f) happen 
if CN.CLOSEDOOR(f) happen  then LP.CLOSEDOOR(f) happen  

if LP.OPENDOOR(f) happen then CN.OPENDOOR(f) happen
if CN.OPENDOOR(f) happen  then LP.OPENDOOR(f) happen 
    	
if LP.MOTORSTOP happen then CN.MOTORSTOP happen
if CN.MOTORSTOP happen  then LP.MOTORSTOP happen   
    	
if LP.MOTORUP happen then CN.MOTORUP  happen  
if CN.MOTORUP happen  then LP.MOTORUP happen   

if LP.MOTORDOWN happen then CN.MOTORDOWN  happen  
if CN.MOTORDOWN(f) happen  then LP.MOTORDOWN happen   
    	
if LP.USERINSIDE(b) happen then CN.USERINSIDE(b) happen   
if CN.USERINSIDE(b) happen  then LP.USERINSIDE(b) happen   

Lift Plant: CASL_LTL Specification

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

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

     
     S -- L --> S' and CABINPOSITION(f) in L  => 
       cabinPosition(S) = f
      	
    cabinPosition(S) = f =>  
       in_one_case(S, next =< L' • CABINPOSITION(f) in L' =>)
    
     S -- L --> S' and OPENDOOR(f) in L  => 
         cabinPosition(S) = f
  
     S -- L --> S' and CLOSEDOOR(f) in L  => 
         cabinPosition(S) = f
 
     S -- L --> S' and MOTORSTOP in L  => 
        cabinPosition(S') = cabinPosition(S)    	
       
    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)
      
    motorStatus(S) = up =>  in_any_case(S, next [ S' • cabinPositionS') = next(cabinPosition(S)])
    
    motorStatus(S) = down =>  in_any_case(S, next [ S' • cabinPositionS') = previous(cabinPosition(S)])
    
    doorPosition(S,f) = open =>  cabinPosition(S) = f
 
     S -- L --> S' and DOORPOSITION(f,dps) in L  => 
         doorPosition(S,f) = dps

    doorPosition(S,f) = dps =>  
         in_one_case(S,next < L' •DOORPOSITION(f,dps)  in L'>)
     
     S -- L --> S' and OPENDOOR(f) in L  => 
         doorPosition(S,f) = open
      
     S -- L --> S' and CLOSEDOOR(f) in L  => 
          doorPosition(S,f) = closed
     
    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  and cabinPosition(S) = f 
    
     S -- L --> S' and  MOTORSTATUS = ms in L  => 
        motorStatus(S) = ms
    
     S -- L --> S' and motorStatus(S) = ms => 
        MOTORSTATUS(ms) in L  
    
    motorStatus(S) =/= stop  =>
       forall f • doorPosition(S,f) = closed
    
    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
  
     userInside(S) >= 0 and userInside(S) =< 5
       
    userInside(S) =/= 0 =>  
        in_any_case(S, eventually [ S' • userInside(S') = 0])