-- ------------------------------------------------------------
-- ------------------------------------------------------------
-- 			5-floor lift 
--
--
-- NuSMV + TKS sample file     
-- N. Markey <markey (a) lsv.ens-cachan.fr>          18-10-2003
-- ------------------------------------------------------------
-- ------------------------------------------------------------


MODULE door(floor, cabin)
-- Each "door" knows its (fix) floor and the position of the cabin


VAR
  call_light: boolean;		-- whether the lift has been called or not
  call_button: boolean;		-- whether someone is pushing on the call button
  open: boolean;		-- whether the door is open or not

DEFINE
  call := call_light | call_button;

INIT
  !call & !open;

TRANS
  next(open) = case 
     -- The door will be open at the next step if the lift has been 
     -- called or sent at this floor, and the cabin is to arrive.
     (call | (cabin.sent_light=floor) | (cabin.sent_button=floor)) 
                  & cabin.moving & (floor = cabin.floor+cabin.dir) : TRUE;
     -- Another possibility is when the lift is "waiting"
     -- at this floor and someone calls (or sends it ?) here.
     (call | (cabin.sent_light=floor) | (cabin.sent_button=floor)) 
                         & (!cabin.moving) & (floor = cabin.floor) : TRUE;
     -- Otherwise, no need to open the door...
     1 : FALSE; 
  esac
  &
  next(call_light) = case 
     open : FALSE;
     call_light|call_button : TRUE;
     1 : FALSE;
  esac



MODULE cabin(door0, door1, door2, door3, door4)
-- the cabin knows the states of all the doors

VAR
  floor: 0..4;			-- where the cabin is
  sent_light: -1..4;		-- if the lift has been sent at some floor
  sent_button: -1..4;		-- if a "send" button is being pushed on
  moving: boolean;		-- if the cabin is moving
  dir: -1..1;			-- direction (down, "here" or up) of the cabin

INIT
  floor=0 & !moving & dir=0 & sent_light=-1 & sent_button=-1

DEFINE 
  -- if the cabin has been called at an upper floor
  callup := (door4.call & floor<4) |
            (door3.call & floor<3) |
            (door2.call & floor<2) |
            (door1.call & floor<1);
  -- if the cabin has been called downstairs
  calldown := (door3.call & floor>3) |
              (door2.call & floor>2) |
              (door1.call & floor>1) |
              (door0.call & floor>0);
  -- if the cabin has been called at all
  call := door0.call | door1.call | door2.call | door3.call | door4.call ;
  -- if a door is open somewhere
  open := door0.open | door1.open | door2.open | door3.open | door4.open ;


TRANS
  next(floor) = case
    moving : floor + dir;
    1 : floor;
  esac
  &
  next(sent_light) = case
    open & (floor=sent_light) : -1;
    (sent_light!=-1) : sent_light;
    1 : sent_button;
  esac
  &
  next(moving) = case
    -- won't move if a door will open
    next(open) : FALSE;
    -- won't move if not been asked to
    (!call) & (sent_light=-1) & (sent_button=-1) : FALSE;
    -- otherwise, let's go !
    1 : TRUE;
  esac
  &
  next(dir) = case
    -- if we don't know where to go...
    (!call) & (sent_light=-1) & (sent_button=-1) : 0;
    -- if we're busy: have to go both up- and downstairs
    (callup | (sent_light>floor) | ((sent_light=-1) & (sent_button>floor))) &
      (calldown | ((sent_light<floor) & (sent_light>-1)) | ((sent_light=-1) & (sent_button>-1) & (sent_button<floor))) & 
      dir!=0 : dir;
    -- if we just have to go upstairs
    callup | (sent_light>floor) | ((sent_light=-1) & (sent_button>floor)) : 1;
    -- or downstairs
    calldown | ((sent_light<floor) & (sent_light>-1)) | ((sent_light=-1) & (sent_button>-1) & (sent_button<floor)) : -1;
    -- don't know if something else if possible, but I would not know what to do...
    1 : 0;
  esac;



MODULE main

VAR
  -- one door at each floor hopefully
  door0: door(0, cabine);
  door1: door(1, cabine);
  door2: door(2, cabine);
  door3: door(3, cabine);
  door4: door(4, cabine);
  -- only one cabin here
  cabine: cabin(door0,door1,door2,door3,door4);
  -- the "duration" variable
  duration: 0..5;

DEFINE
  twoopen := (door0.open & (door1.open | door2.open | door3.open | door4.open)) |
             (door1.open & (door2.open | door3.open | door4.open)) |
	     (door2.open & (door3.open | door4.open)) |
	     (door3.open & door4.open);


INIT
  duration=0

FAIRNESS
  cabine.moving

TRANS
  next(duration) = case
   -- 5 time units for one move of the cabin
   cabine.moving : 5;
   -- possibly 2 time units for doors opening/closing 
   -- (in that case, infinite worst waiting time)
   --cabine.open : 2;
    1 : 0;
  esac

SPEC
  AG (cabine.moving -> !cabine.dir=0)			-- true
SPEC
  AG(cabine.moving -> !cabine.open)			-- true
SPEC
  AG !twoopen						-- true
SPEC
  AG (door2.open -> cabine.floor=2)			-- true
SPEC
  AG ( door0.call -> AF door0.open )			-- true
SPEC
  AG ( (door2.call) -> AF_ 0..20 ( door2.open ) )	-- true
SPEC
  AG ( (door2.call) -> AF<= 19 ( door2.open ) )		-- false
SPEC
  AG ( (door4.call) -> AF<= 40 ( door4.open ) )		-- true
SPEC
  AG ( (door4.call) -> AF<= 39 ( door4.open ) )		-- false

COMPUTE MAX[door4.call, door4.open] 			-- 8 / infinite

COMPUTE MAX[door2.call, door2.open] 			-- 6 / infinite