----------------------------------------------------------------------------- -- COMP424-06A - Assignment 2 - Exercise 2 - Elevator ----------------------------------------------------------------------------- -- This file contains the work of -- - First Name: -- - Last Name: -- - Student ID: ----------------------------------------------------------------------------- -- IMPORTANT -- Please only make the following changes to this file. -- 1. Fill in your name and student ID into the comments above. -- 2. Add SPEC or LTLSPEC sections wherever you like. -- 3. Modify the identified part of the controller (module controller) -- to fix all the bugs you find. ----------------------------------------------------------------------------- -- This file models an elevator and its controller. -- The system consists of -- - An elevator cabin, which can service 4 floors, number 0 to 3. -- The cabin can move up and down between the floors. -- At each floor, there is a position detector reporting when the -- cabin has safely reached the corresponding floor. -- - The cabin door, which can be opened and closed. -- There is a sensor that reports that the door is completely open or -- completely closed. -- It is a control objective to make sure that the door is completely -- closed when the elevator is travelling between floors. -- - The request buttons. There are request buttons at each floor and -- in the cabin, by which users can request the elevator to travel -- to the different floors. Requests to travel to each floor are modelled -- as a bit of their own, making no distinction whether the request -- originates from inside or outside of the cabin. ----------------------------------------------------------------------------- ----------------------------------------------------------------------------- -- Plant model of cabin ----------------------------------------------------------------------------- -- Controls: -- do_up - set by the controller to make cabin move upwards -- do_down - set by the controller to make cabin move downwards -- Sensors: -- at[0] - set to true if cabin is at floor 0 -- at[1] - set to true if cabin is at floor 1 -- at[2] - set to true if cabin is at floor 2 -- at[3] - set to true if cabin is at floor 3 ----------------------------------------------------------------------------- -- Internal: -- position - the detailed position of the cabin: -- 0 = cabin is at floor 0 -- 1 = cabin is between floors 0 and 1 -- 2 = cabin is at floor 1 -- 3 = cabin is between floors 1 and 2 -- 4 = cabin is at floor 2 -- 5 = cabin is between floors 2 and 3 -- 6 = cabin is at floor 3 -- broken - flag indicating that something has gone wrong. -- The cabin can break by being moved upwards beyond -- floor 3, by being moved downwards beyond floor 0, -- or by being moved upwards and downwards at the same time. -- running - flag indicating whether the cabin state will change. -- At each step, the cabin may or may not change its position, -- even if the up or down command has been activated. -- If running is set to true, the cabin will move, -- otherwise it remains where it is. ----------------------------------------------------------------------------- MODULE cabin(do_up, do_down) VAR at : array 0..3 of boolean; position : 0..6; broken : boolean; running : boolean; DEFINE MAX_POS := 6; -- the maximum value of the 'position' variable ASSIGN -- Compute the outputs of the position sensors from the detailed position: at[0] := position = 0; at[1] := position = 2; at[2] := position = 4; at[3] := position = 6; -- Compute the next value of the detailed position: -- initially at floor 0 ... init(position) := 0; next(position) := case -- unchanged if not running ... !running : position; -- move upwards ... do_up & (position < MAX_POS) : position + 1; -- or downwards ... do_down & (position > 0) : position - 1; -- or stay in place if no command has been set. 1 : position; esac; -- How the cabin can break: -- initially all is fine ... init(broken) := 0; next(broken) := case -- unchanged if not running ... !running : broken; -- or if already broken ... broken : broken; -- can break when going up and down at the same time ... do_up & do_down : {0, 1}; -- or when going up beyond the maximum ... do_up & (position = MAX_POS) : {0, 1}; -- or when going down beyond the minimum ... do_down & (position = 0) : {0, 1}; -- otherwise all is fine. 1 : 0; esac; ----------------------------------------------------------------------------- -- Fairness assumption: -- The cabin gets to move infinitely often. JUSTICE running ----------------------------------------------------------------------------- -- Add specifications here, if you want. ----------------------------------------------------------------------------- -- Plant model of elevator door ----------------------------------------------------------------------------- -- Controls: -- do_open - set by the controller to make the door open. -- do_close - set by the controller to make the door close. -- Sensors: -- is_open - set to true if the door is completely open. -- is_closed - set to true if the door is completely closed. ----------------------------------------------------------------------------- -- Internal: -- state - the door can be in five possible states: -- OPEN -- the door is completely open so it is safe -- for passengers to enter or leave the cabin. -- CLOSED -- the door is completely closed so it is safe -- for the cabin to move between floors. -- HALFOPEN -- the door is in an intermediate state -- while being opened or closed. -- BROKEN -- the door is in a bad state because the -- do_open and do_close commands have been -- used inappropriately. -- running - flag indicating whether the door state will change. -- At each step, the door may or may not change its state, -- even if the do_open or do_close command has been activated. -- If running is set to true, the door will change its state, -- otherwise it remains unchanged. ----------------------------------------------------------------------------- MODULE door(do_open, do_close) VAR state : {OPEN, CLOSED, HALFOPEN, BROKEN}; running : boolean; DEFINE is_open := state = OPEN; is_closed := state = CLOSED; ASSIGN -- Changing the door state: -- initially closed ... init(state) := CLOSED; next(state) := case -- unchanged if not running ... !running : state; -- can be closed ... state = OPEN & do_close & !do_open : {HALFOPEN, CLOSED}; state = HALFOPEN & do_close & !do_open : CLOSED; -- and opened ... state = CLOSED & do_open & !do_close : {HALFOPEN, OPEN}; state = HALFOPEN & do_open & !do_close : OPEN; -- unchanged if no command set. !do_open & !do_close : state; -- remains broken once broken ... state = BROKEN : state; -- undefined otherwise ... 1 : {OPEN, CLOSED, HALFOPEN, BROKEN}; esac; ----------------------------------------------------------------------------- -- Fairness assumption: -- The door gets to move infinitely often. JUSTICE running ----------------------------------------------------------------------------- -- Add specifications here, if you want. ----------------------------------------------------------------------------- -- Plant model of elevator requests ----------------------------------------------------------------------------- -- Inputs: -- at - the position indicators (at[0]...at[3]) from the cabin. -- is_open - flag indicating that the elevator door is open. -- Sensors: -- req[0] - set to true if the cabin has been requested to move to floor 0 -- Once received, a request remains set until it is -- fulfilled, i.e., until the elevator reaches the -- corresponding floor and the door is opened. -- req[1] - set to true if the cabin has been requested to move to floor 1 -- req[2] - set to true if the cabin has been requested to move to floor 2 -- req[3] - set to true if the cabin has been requested to move to floor 3 ----------------------------------------------------------------------------- -- Internal: -- req_fair - A flag used to model a fairness assumption for requests. -- When the elevator is at a certain floor i and closes its -- doors in order to move somewhere else, it may be forced -- to stop and reopen its door by a new request from floor i. -- This can be considered as correct behaviour, but it may -- prevent the elevator from ever leaving floor i. -- Therefore, a fairness assumption is created, stating -- that such last-minute requests do not occur infinitely -- often. Once req_fair is set to true, there will be no -- further request until the elevator leaves the current floor. ----------------------------------------------------------------------------- MODULE requests(at, is_open) VAR req : array 0..3 of boolean; req_fair : boolean; ASSIGN -- Initially, all requests are off. init(req[0]) := 0; next(req[0]) := case -- Clear request if elevator is at the floor with open door ... at[0] & is_open : 0; -- otherwise keep request if already present ... req[0] : 1; -- otherwise do not set requests for the current floor -- if req_fair is set (see above) ... at[0] & req_fair : 0; -- in all other cases requests may appear. 1 : {0, 1}; esac; -- Same procedure for each floor. init(req[1]) := 0; next(req[1]) := case at[1] & is_open : 0; req[1] : 1; at[1] & req_fair : 0; 1 : {0, 1}; esac; init(req[2]) := 0; next(req[2]) := case at[2] & is_open : 0; req[2] : 1; at[2] & req_fair : 0; 1 : {0, 1}; esac; init(req[3]) := 0; next(req[3]) := case at[3] & is_open : 0; req[3] : 1; at[3] & req_fair : 0; 1 : {0, 1}; esac; -- The req_fair flag may go on at anytime when it is off. -- As long as there are no requests, it may go off again. -- Otherwise, once on, it remains on until the elevator leaves the current -- floor (if it is at any floor), only afterwards it may go off again. next(req_fair) := case !req_fair : {0, 1}; !req[0] & !req[1] & !req[2] & !req[3] : {0, 1}; at[0] & next(at[0]) : 1; at[1] & next(at[1]) : 1; at[2] & next(at[2]) : 1; at[3] & next(at[3]) : 1; 1 : {0, 1}; esac; ----------------------------------------------------------------------------- -- The fairness assumption states that the elevator is not held off -- by last-minute requests to open the door infinitely often (see above). JUSTICE req_fair ----------------------------------------------------------------------------- -- Add specifications here, if you want. ----------------------------------------------------------------------------- -- Plant model ----------------------------------------------------------------------------- -- All the components of the elevator system to be controlled are included -- here. ----------------------------------------------------------------------------- -- Actuators: -- do_up - the up command for the cabin -- do_down - the down command for the cabin -- do_open - the open command for the door -- do_close - the close command for the door ----------------------------------------------------------------------------- -- Sensors: -- at - the position indicators (at[0]...at[3]) from the cabin -- is_open - door sensor: true if the door is completely open. -- is_closed - door sensor: true if the door is completely closed. -- req - the request signals (req[0]...req[3]) from the request module ----------------------------------------------------------------------------- MODULE elevator(do_up, do_down, do_open, do_close) VAR cabin: cabin(do_up, do_down); door: door(do_open, do_close); requests: requests(at, is_open); DEFINE -- Sensors are just passed on from the components that generate them ... at[0] := cabin.at[0]; at[1] := cabin.at[1]; at[2] := cabin.at[2]; at[3] := cabin.at[3]; is_open := door.is_open; is_closed := door.is_closed; req[0] := requests.req[0]; req[1] := requests.req[1]; req[2] := requests.req[2]; req[3] := requests.req[3]; ----------------------------------------------------------------------------- -- Add specifications here, if you want. ----------------------------------------------------------------------------- -- The control program for the entire elevator ----------------------------------------------------------------------------- -- Inputs: -- at - the position indicators (at[0]...at[3]) from the cabin -- is_open - door sensor: true if the door is completely open. -- is_closed - door sensor: true if the door is completely closed. -- req - the request signals (req[0]...req[3]) from the request module -- Outputs: -- do_up - the up command for the cabin -- do_down - the down command for the cabin -- do_open - the open command for the door -- do_close - the close command for the door ----------------------------------------------------------------------------- -- Internal: -- up_sweep - a flag indicating whether the elevator is moving up or down. -- When up_sweep is true, requests from floors above the -- current position have priority above requests from below; -- otherwise requests from below have priority. ----------------------------------------------------------------------------- -- NOTE: -- This controller is buggy! It is your task to fix it! ----------------------------------------------------------------------------- MODULE controller(at, is_open, is_closed, req) VAR do_up: boolean; do_down: boolean; do_open: boolean; do_close: boolean; -- >>> Feel free to make changes below this line <<<<<<<<<<<<<<<<<<<<<<<<<<<< VAR up_sweep : boolean; DEFINE -- Some auxiliary status flags: -- The elevator is between floors. nowhere := !at[0] & !at[1] & !at[2] & !at[3]; -- There is an unsatisfied request originating from the current floor. req_here := case at[0] : req[0]; at[1] : req[1]; at[2] : req[2]; at[3] : req[3]; esac; -- There is an unsatisfied request originating from a floor above the -- current position. req_up := case at[0] : req[1] | req[2] | req[3]; at[1] : req[2] | req[3]; at[2] : req[3]; at[3] : 0; esac; -- There is an unsatisfied request originating from a floor below the -- current position. req_down := case at[0] : 0; at[1] : req[0]; at[2] : req[0] | req[1]; at[3] : req[0] | req[1] | req[2]; esac; ASSIGN -- And here is the actual controller ... do_up := case nowhere : up_sweep; req_here : 0; req_up & !req_down : 1; 1 : 0; esac; do_down := case nowhere : !up_sweep; req_here : 0; req_down : 1; 1 : 0; esac; do_open := case nowhere : 0; is_closed & req_here : 1; 1 : 0; esac; do_close := case nowhere : 0; is_open & !req_here : 1; 1 : 0; esac; init(up_sweep) := 1; next(up_sweep) := case req_down & !req_up : 0; req_up & !req_down : 1; 1 : up_sweep; esac; -- >>> Feel free to make changes above this line <<<<<<<<<<<<<<<<<<<<<<<<<<<< ----------------------------------------------------------------------------- -- Putting it all together ----------------------------------------------------------------------------- -- The system consists of the controller and the plant, -- which in turn is composed of cabin, door, and requests module. ----------------------------------------------------------------------------- MODULE main VAR controller: controller(plant.at, plant.is_open, plant.is_closed, plant.req); plant: elevator(controller.do_up, controller.do_down, controller.do_open, controller.do_close); ----------------------------------------------------------------------------- -- Add specifications here, if you want.