COMP2111 Assignment 4
Ken Robinson 10th May 2012
Name of assignment: LiftController Assessment: 20 marks
Submission: give cs2111 ass4 LiftController.zip Deadline: Friday June 1 (23:59:59)
1 Overview of assignment
This assignment extends the lecture example of a simple lift controller, that you can extract from an archive (see 2.2). The archive contains:
Lift ctx: the basic lift context;
BasicLift: the machine that models all the basic lift movements; Doors ctx: the context for lift and floor doors;
LiftPlusDoors: BasicLift extended with lift doors;
Buttons ctx: context for lift and floor buttons;
LiftButtons: LiftPlusDoors extended by buttons in lifts;
1.1 Requirements
Req 1: There is a finite non-empty set of lifts.
Req 2: There is a finite non-empty set of floors.
Req 3: All lifts operate over the full set of floors
Req 4: Lifts may be one of moving, stopped, idle. An idle lift is inactive and must be activated before it can move.
Req 5: A moving lift may be moving UP or DOWN.
Req 5a: A lift at level 0 (lowest level) must be moving UP
Req 5b: A lift at the maximum level must be moving DOWN
Req 6: A stopped lift may change the direction of movement; a moving lift may not change direction, it must stop in order to change direction.
Req 7: Each lift has a door.
Req 8: On each floor there is a door for each lift.
Req 9: The lift door of a moving lift must be closed.
Req10: If a lift is moving then all floor doors for that lift must be closed.
Req 11: If a lift is stopped then the lift door for that lift may be open.
Req 12: If a lift is stopped and the lift door for that lift is open, then the floor door for that lift may be open.
Req 13: The lift door opens before the corresponding floor door, and the floor door closes before the corresponding lift door.
Req14: After the floor door opens there should be a delay before the floor door closes.
off. Req 20:
a) After stopping a lift must continue on its current direction of travel if there are floors in that direction that are in the liftschedule. This strategy is intended to ensure that all lift passengers —that is passengers in a lift— experience the smallest possible number of lift stops before the lift stops at the floor requested by the lift buttons.
b) After stopping, a lift must change direction if the liftschedule is not empty but does not contain floors in the direction of travel.
Req 22: When a lift stops at a requested stop, then the doors must open, and remain open for an interval to allow passengers to leave the lift.
1.2 The Current State
BasicLift, LiftPlusDoors contain basic lift movement and safety constraints. These machines concentrate on establishing the rules for lift and door movements consistent with the above re- quirements, so that any further refinements will be constrained by those rules. All activities are currently nondeterministic and don’t describe a useful lift system. For example: there is no reli- able way of entering a lift, and once in a lift there is no assurance you will be able to get out of the lift again, let alone get out at the desired floor.
Both the lift and floor doors are closed for an idle lift.
Each lift is equipped with a set of lift-buttons corresponding to all floors for the building. Each lift button is either on or off.
If a lift button is on then the lift must stop at the floor corresponding to that button. When the lift stops at a floor then the lift button corresponding to that floor must be
Each lift should be associated with a liftschedule that contains all the floors at which the lift must stop.
1.3 Adding Lift Buttons
Lift buttons are added to each lift, providing a capability for lift passengers to request for the lift to stop at particular floors. The modelling of the servicing of lift button requests must guarantee that all requests are serviced in the shortest possible time, as assessed across all current requests. The requirements are set ouf in section 1.1, where a simple lift schedule that provides for simple scheduling of lift button requests is described.
The refinement for LiftButtons shown here consists of:
LiftButtons: add lift buttons to each lift. These buttons select floors and are either ON or OFF.
Lift scheduling: at the same time as the addition of lift buttons, a lift schedule is introduced. The lift schedule records the floors to stop assigned to each lift. The requests recorded in the lift buttons are assigned to that lift’s schedule.
1.4 Adding Floor Buttons
Each floor needs to be associated with buttons, which we will call Floor Buttons that are used by people on a floor to request a lift that will take them either UP or DOWN. Floor buttons are not associated with a lift, only a floor. Excepting the top and bottom floors, each floor will have two buttons, associated respectively with UP and DOWN. Each button will be either ON or OFF. For uniformity sake the extreme floors can also be associated with two buttons, one of which is always OFF.
LiftButtons and FloorButtons should enforce what might be described as “passenger satisfac- tion policies”. For LiftButtons, that policy is an expression of the idea that when passengers in a lift select floors –by pressing lift buttons— the lift will deliver all of those passengers to the chosen floors in the shortest journeys, subject to the context of the lift when the buttons were pressed.
1.5 Requirements for floor buttons
Req 23: Each floor is equipped with buttons for requesting a lift travelling either up or down. Obviously the bottom and top floors do not need a button for requesting a lift travelling down or up, respectively. Note that floor buttons are associated with a floor. There is no association with any particular lift.
Req 24: Every activated floor request must be scheduled. That is, at least one lift must eventually be scheduled to service each floor request. Of course, there may be more than one lift that is able to service a particular floor request.
Req 25: Scheduling must ensure that every floor request will be serviced, eventually; not neces- sarily optimally.
Req 26: Scheduling of floor requests must not compromise the scheduling strategy for lift button requests described in Req 21.
1.6 Rules for Lift System
The following rules are required to model a lift system that provides an acceptable level of service.
Buttons remain ON until the request is serviced: a button, whether a lift button or a floor button remains ON until the request implied by that button is serviced. In the case of a lift button this means the lift stops at the selected floor, and in the case of a floor button it means a lift travelling in the required direction stops at the floor.
Lifts continue as long as possible in the same direction: having stopped at a floor a lift should continue in the same direction it was travelling, if there are scheduled requests in that direction. If there are no such requests, but there are scheduled requests in the other direction then the lift will change direction and proceed using this same rule.
Lifts without scheduled requests should become IDLE: having stopped, if a lift has no scheduled requests remaining then the lift should close its doors and enter the IDLE state.
Floor requests are given to the nearest lift: as far as possible requests for a lift initiated by a floor request are assigned to the nearest lift, see below.
1.7 Scheduling floor buttons
Scheduling floor buttons is more difficult than scheduling lift buttons.
• when stopping at a floor to service a floor request the lift must not only be at the floor on which the request was made, but must be travelling in the required direction;
• of course, any lift stopping at a floor may service a floor request and this may render redundant the earlier scheduling of a lift to service the request, and in some circumstances the floor may be safely removed from the schedule;
• it would appear that a floor request should be assigned to the “nearest lift”, but that concept is quite difficult to measure, and, given the dynamic nature of the system, is likely to be less effective than expected. Remember that the extent of a lift’s travel in a particular direction is not deterministic. A lift could travel to the topmost floor or to the bottommost floor, or it may exhaust schedule requests before that happens;
• floor requests could be assigned randomly to lifts;
1.8 Policy for Floor requests
While we can construct a reasonable policy for lift requests that is capable of being implemented reasonably simply, it is more difficult for floor requests. The minimum policy is:
floor requests are scheduled in finite time and the scheduling must guarantee that the request is serviced.
The scheduling should allow for the possibility that the request could be serviced by a lift other than the intended lift.
Another possibility is that servicing of a request ma be assigned to multiple lifts, with only one lift actually carrying out the task. Scheduling for requests that are no longer required can be removed.
What you should do
First, download LiftController.zip from the class archive. A link will be found on the class webpage.
Create a refinement of LiftButtons using the Event-B explorer. Name it Floorbuttons.
Add the following to the refinement: New variable
floorbuttons
floorbuttons ∈ FLOOR → (DIRECTION → BUTTON) floorbuttons(0)(DOWN) = OFF floorbuttons(MAXFLOOR)(UP) = OFF
4. Next, read the given parts of the model, especially the LiftButtons machine, and understand how the model achieves the requirements. Special attention should be paid to understanding the role of the invariants and guards.
5. Devise a scheme to schedule the floor requests and develop a model based on that scheme.
6. Special attention should be paid to developing invariants that will assist in assuring that the model is behaving as your expect it to.
7. Read and consider carefully the following item on data refinement.
8. Animate: you will almost certainly find it useful to animate in order to to get an appreciation of whether your scheduling is following the type of discipline you require. Remember that animation can’t be used to verify your model. Animation will not be assessed.
9. Discharge as many POs as you can.
2.1 Data refinement of liftschedule
It is almost certain that the best refinement will be achieved by data refinement. The reason is that while the current scheduling, using liftschedule as it stands, will not be able to be used to schedule the floor button requests, because it is not sensitive to direction, the fact is that you do have a scheduling strategy. What is required is to be able to extend the direction insensitive liftschedule to incorporate the direction sensitive requirements.
That is data refinement.
If you can do that then the current framework only needs to be adapted to incorporate the data refinement.
2.2 Initiating the data refinement
Data refinement requires the following steps:
Delete liftschedule the variable liftschedule must be deleted. Simply delete the variable from the variables.
Do not make any other changes at the moment.
Decide how you are going to use the liftschedule strategy this involves creating new vari- ables that you can use to schedule both liftbutton and floorbutton requests, and
Decide how you can extract the value of liftschedule this forms the refinement relation that relates the new set of variables to the deleted liftschedule.
The above exercise involves determining how you can use information from the floor requests that can be used at the appropriate time to drive the same scheduling model.
Since liftschedule has been deleted most of the places where you will need to do something will be highlighted with error diagnostics. What is required at these points is a description of how the current state relates to the deleted liftschedule. That is the verification of the refinement relation.
The above shows one of the big advantages of using data refinement: the structure of the floorbuttons machine remains significantly the same as the structure of liftbuttons. To a significant degree you only have to supply the information that allows the refinement relation to be verified.
Of course, there will be new cases that apply specifically to the function of the floor buttons.
Programming Help, Add QQ: 749389476
CONTEXT Lift ctx SETS
axm1 : MAXFLOOR ∈ N1
axm2 :MAXFLOOR≥2
axm3 :FLOOR=0..MAXFLOOR
axm4 : finite(LIFT)
axm5 : partition(DIRECTION,{UP},{DOWN})
axm6 : partition(STATUS,{IDLE},{STOPPED},{MOVING}) axm7 : CHANGE ∈ DIRECTION DIRECTION
axm8 : CHANGE = {UP 7→ DOWN,DOWN 7→ UP}
thm1 : FLOOR ̸= ∅
thm2 : finite(FLOOR)
thm3 : finite(STATUS)
thm4 : finite(DIRECTION)
thm5 : finite(CHANGE)
MACHINE BasicLift
This machine models the basic lift movements,
SEES Lift ctx VARIABLES
lif tposition
lif tstatus
lif tdirection
INVARIANTS
EVENTS Initialisation
Event IdleLift =b
and establishes the basic lift constraints.
The behaviour is non-deterministic:
there is no attempt to express any sort of lift control or scheduling. A discpline of lift direction is established:
* level 0: direction is UP
* level MAXFLOOR: direction is DOWN
* other floors: either direction is valid
A lift at any time has one of the following statuses:
IDLE: not currently an active lift
STOPPED: not moving
MOVING: moving between floors
The status of a lift must be STOPPED before it becomes IDLE; and must be STOPPED before it becomes MOVING
There are no doors.
inv1 :liftposition∈LIFT→FLOOR thm1 : finite(liftposition)
inv2 :liftstatus∈LIFT→STATUS thm2 : finite(liftstatus)
inv3 : liftdirection ∈ LIFT → DIRECTION thm3 : finite(liftdirection)
inv4 : ∀l·l ∈ LIFT ∧ liftposition(l) = 0
⇒ lif tdirection(l) = U P
inv5 : ∀l·l ∈ LIFT ∧ liftposition(l) = MAXFLOOR
⇒ lif tdirection(l) = DOW N
thm4 : ∀l·l ∈ LIFT ∧ liftdirection(l) = DOWN
⇒ lif tposition(l) ̸= 0
thm5 : ∀l·l ∈ LIFT ∧ liftdirection(l) = UP
⇒ liftposition(l) ̸= MAXFLOOR thm6 : ∀l·l ∈ LIFT ∧ liftdirection(l) = UP
⇒ liftposition(l) + 1 ≤ MAXFLOOR
act1 :liftposition:=LIFT×{0} act2 :liftdirection:=LIFT×{UP} act3 :liftstatus:=LIFT×{IDLE}
Idle lifts cannot move
grd1 : liftstatus(lift) = STOPPED then
act1 : liftstatus(lift) := IDLE end
Event ActivateLift =b any
Ready an Idle lift to enable moving
grd1 : liftstatus(lift) = IDLE then
act1 : liftstatus(lift) := STOPPED end
Event StartLift =b any
Models the starting of a STOPPED lift, maintaining previous direction
grd1 : liftstatus(lift) = STOPPED then
act1 : liftstatus(lift) := MOV ING end
Event ChangeDir =b
Models the changing of direction of a STOPPED lift
act1 : liftdirection(lift) := CHANGE(liftdirection(lift)) end
Event MoveUp =b
Models a lift moving up to the next floor
grd1 : liftstatus(lift) = STOPPED grd2 : liftposition(lift) ̸= 0
grd3 : liftposition(lift) ̸= MAXFLOOR
where its status is either MOVING or STOPPED
grd1 : liftstatus(lift) = MOV ING
grd2 : liftdirection(lift) = UP then
act1 :liftposition(lift):=liftposition(lift)+1
act2 : liftdirection : |liftdirection′ ∈ LIFT → DIRECTION
∧ (liftposition(lift) + 1 = MAXFLOOR
liftdirection′ =liftdirection▹−{lift7→DOWN})
∧ (liftposition(lift) + 1 ̸= MAXFLOOR
liftdirection′ = liftdirection)
act3 : liftstatus : |liftstatus′ ∈ LIFT → STATUS ∧
((liftstatus′ = liftstatus ▹− {lift 7→ MOV ING}) ∨
(liftstatus′ = liftstatus ▹− {lift 7→ STOPPED}))
Event MoveDown =b
Models a lift moving down to the next floor where its status is either MOVING or STOPPED
grd2 : liftdirection(lift) = DOWN then
grd1 : liftstatus(lift) = MOV ING
act1 :liftposition(lift):=liftposition(lift)−1
act2 : liftdirection : |liftdirection′ ∈ LIFT → DIRECTION
∧ (lif tposition(lif t) = 1
liftdirection′ =liftdirection▹−{lift7→UP})
∧ (lif tposition(lif t) ̸= 1
liftdirection′ = liftdirection)
act3 : liftstatus : |liftstatus′ ∈ LIFT → STATUS ∧
((liftstatus′ = liftstatus ▹− {lift 7→ MOV ING}) ∨
(liftstatus′ = liftstatus ▹− {lift 7→ STOPPED}))
CONTEXT Doors ctx SETS
OPEN CLOSED
axm1 : partition(DOORS,{OPEN},{CLOSED}) END
MACHINE LiftPlusDoors
Add doors to the floors and also the lifts.
Floor doors requirements:
When a lift stops at a floor the status of the doors moves through the
CLOSED OPEN, CLOSED.
1) the lift door may be opened only if the lift status is STOPPED, and the liftdoorstatus is CLOSED
2) the floor door may be opened only if the lift status is STOPPED, the liftdoorstatus is OPEN and the floordoorstatus is CLOSED
3) the floor door may be closed only if the lift status is STOPPED, the liftdoorstatus and floordoorstatus are both OPEN
4) the lift door may be closed only if the lift status is STOPPED,
the floordoorstatus is CLOSED and liftdoorstatus is OPEN
5) the lift floordoor may be OPEN only on the floor on which the lift is
6) it is clear that the above door opening/closing sequence can cycle; this will be prevented by scheduling
Lift doors requirements:
1) a Lift door may be open only if
a) the lift is STOPPED, and
b) the floor door is OPEN
The lift door opens AFTER the floor door
and closes AFTER the floor door.
A new event OpenDoors is introduced.
This event can only be activated when the lift status is STOPPED and
initiate a cycle through the door opening sequence.
REFINES BasicLift SEES Lift ctx, Door ctx VARIABLES
lif tposition
lif tstatus
lif tdirection
f loordoorstatus
lif tdoorstatus
INVARIANTS
inv1 : floordoorstatus ∈ LIFT → (FLOOR → DOOR)
inv2 :liftdoorstatus∈LIFT→DOOR
inv3 :∀l,f·f∈FLOOR∧f̸=liftposition(l) ⇒
floordoorstatus(l)(f) = CLOSED
Floor doors may be OPEN only on the floor that is the current position of the lift
inv4 :∀l·liftstatus(l)∈{MOVING,IDLE} ⇒
liftdoorstatus(l) = CLOSED
浙大学霸代写 加微信 cstutorcs
inv5 :∀l,f·liftstatus(l)∈{MOVING,IDLE}∧f∈FLOOR ⇒
floordoorstatus(l)(f) = CLOSED If a lift is MOVING or IDLE
then the lift door and all floor doors are CLOSED
inv8 :∀l,f·f=liftposition(l)∧floordoorstatus(l)(f)=OPEN
liftdoorstatus(l) = OPEN
Floor door may be OPEN only if the lift door is OPEN
thm1 :∀l,f·f∈FLOOR∧floordoorstatus(l)(f)=OPEN ⇒
f = liftposition(l)
thm2 : ∀l·liftdoorstatus(l) = OPEN
liftstatus(l) = STOPPED
thm3 : ∀l·floordoorstatus(l)(liftposition(l)) = OPEN
liftstatus(l) = STOPPED ∧ liftdoorstatus(l) = OPEN
inv6 : waiting ⊆ LIFT inv7 : ∀l·l ∈ waiting
Event OpenLiftDoor =b any
floordoorstatus(l)(liftposition(l)) = OPEN ∧ liftdoorstatus(l) = OPEN
waiting is used to provide a simple model of a pause before closing doors
EVENTS Initialisation
act6 : waiting := ∅ end
Event OpenFloorDoor =b any
act2 : waiting := waiting ∪ {lift} end
act1 :liftposition:=LIFT×{0}
act2 :liftdirection:=LIFT×{UP}
act3 :liftstatus:=LIFT×{IDLE}
act4 : floordoorstatus := LIFT × {FLOOR × {CLOSED}}
act5 : liftdoorstatus := LIFT × {CLOSED}
grd1 : liftstatus(lift) = STOPPED
grd2 : floordoorstatus(lift)(liftposition(lift)) = CLOSED grd3 : liftdoorstatus(lift) = OPEN
act1 : floordoorstatus(lift) := floordoorstatus(lift) ▹− {liftposition(lift) 7→ OPEN}
Code Help, Add WeChat: cstutorcs
act1 : liftdoorstatus(lift) := OPEN end
Event CloseFloorDoor =b any
grd4 : lift ∈/ waiting then
act1 : floordoorstatus(lift) := floordoorstatus(lift) ▹− {liftposition(lift) 7→ CLOSED} end
Event CloseLiftdoor =b any
act1 : liftdoorstatus(lift) := CLOSED end
grd1 : liftstatus(lift) = STOPPED
grd2 : floordoorstatus(lift)(liftposition(lift)) = OPEN grd3 : liftdoorstatus(lift) = CLOSED
grd1 : liftstatus(lift) = STOPPED
grd2 : floordoorstatus(lift)(liftposition(lift)) = OPEN
grd3 : liftdoorstatus(lift) = OPEN
grd1 : liftstatus(lift) = STOPPED
grd2 : floordoorstatus(lift)(liftposition(lift)) = CLOSED grd3 : liftdoorstatus(lift) = OPEN
Event Release =b any
grd1 : lift ∈ waiting then
act1 : waiting := waiting \ {lif t} end
Event MoveUp =b
Models a lift moving up to the next floor and continuing to move
refines MoveUp any
Models pausing between opening and closing lift doors
grd2 : liftdirection(lift) = UP then
act1 :liftposition(lift):=liftposition(lift)+1
act2 : liftdirection : |liftdirection′ ∈ LIFT → DIRECTION
∧ (liftposition(lift) + 1 = MAXFLOOR
liftdirection′ =liftdirection▹−{lift7→DOWN})
∧ (liftposition(lift) + 1 ̸= MAXFLOOR
liftdirection′ = liftdirection)
act3 : liftstatus : |liftstatus′ ∈ LIFT → STATUS ∧
(liftstatus′ = liftstatus ▹− {lift 7→ MOV ING}) Event MoveUpAndStop =b
grd1 : liftstatus(lift) = MOV ING
refines MoveUp any
grd2 : liftdirection(lift) = UP then
act1 :liftposition(lift):=liftposition(lift)+1
act2 : liftdirection : |liftdirection′ ∈ LIFT → DIRECTION
∧ (liftposition(lift) + 1 = MAXFLOOR
liftdirection′ =liftdirection▹−{lift7→DOWN})
∧ (liftposition(lift) + 1 ̸= MAXFLOOR
liftdirection′ = liftdirection) act3 : liftstatus(lift) := STOPPED
Event MoveDown =b
Models a lift moving up to the next floor and stopping
grd1 : liftstatus(lift) = MOV ING
Models a lift moving down to the next floor and continueing to move
refines MoveDown any
grd2 : liftdirection(lift) = DOWN then
act1 :liftposition(lift):=liftposition(lift)−1
grd1 : liftstatus(lift) = MOV ING
act2 : liftdirection : |liftdirection′ ∈ LIFT → DIRECTION ∧ (lif tposition(lif t) = 1
liftdirection′ =liftdirection▹−{lift7→UP})
∧ (lif tposition(lif t) ̸= 1
liftdirection′ = liftdirection)
act3 : liftstatus : |liftstatus′ ∈ LIFT → STATUS ∧
(liftstatus′ = liftstatus ▹− {lift 7→ MOV ING}) Event MoveDownAndStop =b
refines MoveDown any
grd2 : liftdirection(lift) = DOWN then
act1 :liftposition(lift):=liftposition(lift)−1
act2 : liftdirection : |liftdirection′ ∈ LIFT → DIRECTION
∧ (lif tposition(lif t) = 1
liftdirection′ =liftdirection▹−{lift7→UP})
∧ (lif tposition(lif t) ̸= 1
liftdirection′ = liftdirection) act3 : liftstatus(lift) := STOPPED
Models a lift moving down to the next floor and stopping
grd1 : liftstatus(lift) = MOV ING
Event StartLift =b
extends StartLift any
act1 : liftstatus(lift) := MOV ING end
Event ChangeDir =b
Models the changing of direction of a STOPPED lift
extends ChangeDir any
Models the starting of a STOPPED lift, maintaining of previous direction
grd1 : liftstatus(lift) = STOPPED
grd2 : liftdoorstatus(lift) = CLOSED
grd3 : floordoorstatus(lift)(liftposition(lift)) = CLOSED
act1 : Event IdleLift =b
extends IdleLift any
liftstatus(lift) := IDLE
act1 : Event ActivateLift =b
Ready an Idle lift to enable moving
grd1 : grd2 : grd3 :
liftstatus(lift) = STOPPED liftposition(lift) ̸= 0 liftposition(lift) ̸= MAXFLOOR
liftdirection(lift) := CHANGE(liftdirection(lift))
Idle lifts cannot move
liftstatus(lift) = STOPPED floordoorstatus(lift)(liftposition(lift)) = CLOSED liftdoorstatus(lift) = CLOSED
extends ActivateLift any
grd1 : liftstatus(lift) = IDLE then
act1 : liftstatus(lift) := STOPPED end
MACHINE LiftPlusFloorDoors This machine completes the modelling of doors for a lift by introducing floor doors.
REFINES LiftPlusDoors SEES Lift ctx, Doors ctx VARIABLES
lif tposition
lif tstatus
lif tdirection
lif tdoorstatus
f loordoorstatus
INVARIANTS
inv1 : floordoorstatus ∈ LIFT → (FLOOR → DOORS) thm1 : finite(floordoorstatus)
inv2 : ∀l·l ∈ LIFT ∧ liftdoorstatus(l) = CLOSED
floordoorstatus(l)(liftposition(l)) = CLOSED
Req 13: The floor door opens AFTER the lift door opens
inv3 :∀l,f·l∈LIFT∧f∈FLOOR\{liftposition(l)} ⇒
floordoorstatus(l)(f) = CLOSED
Req 11: Floor doors may be OPEN only on the floor where a lift is stopped
thm2 :∀l,f·l∈LIFT∧f∈FLOOR∧liftstatus(l)=MOVING ⇒
floordoorstatus(l)(f) = CLOSED
Req 10: If a lift is MOVING then the floor door for that lift is CLOSED on all floors
thm3 : ∀l·l ∈ LIFT ∧ floordoorstatus(l)(liftposition(l)) = OPEN ⇒
liftdoorstatus(l) = OPEN
Req 13, 14: Floor door OPEN implies lift door OPEN
inv4 : ∀l·l ∈ LIFT ∧ floordoorstatus(l)(liftposition(l)) = OPEN ⇒
liftstatus(l) = WAITING
Req 11 (variant): Floor door may be OPEN only in WAITING state
EVENTS Initialisation
Event OpenFloorDoor =b Req 11: The floor door opens when the status of the lift is WAITING
act1 :liftposition:=LIFT×{0}
act2 :liftdirection:=LIFT×{UP}
act3 :liftstatus:=LIFT×{IDLE}
act4 : liftdoorstatus := LIFT × {CLOSED}
act5 : floordoorstatus := LIFT × {FLOOR × {CLOSED}}
lift f loor
act1 : floordoorstatus(lift) := floordoorstatus(lift) ▹− {floor 7→ OPEN} end
Event CloseFloorDoor =b Req 14 refines ChangeStatus
grd2 : liftstatus(lift) = WAITING then
act1 : floordoorstatus(lift) := floordoorstatus(lift) ▹− {liftposition(lift) 7→ CLOSED}
act2 : liftstatus(lift) := STOPPED end
Event OpenLiftDoor =b extends OpenLiftDoor
grd2 : liftdoorstatus(lift) = CLOSED then
act1 : liftdoorstatus(lift) := OPEN end
Event CloseLiftdoor =b extends CloseLiftdoor
grd2 : floordoorstatus(lift)(liftposition(lift)) = CLOSED then
act1 : liftdoorstatus(lift) := CLOSED
act2 : liftstatus(lift) := STOPPED end
Event StartLift =b Models the starting of a STOPPED lift, maintaining of previous direction 19
grd1 : floor = liftposition(lift)
grd2 : liftdoorstatus(lift) = OPEN
grd3 : floordoorstatus(lift)(floor) = CLOSED
grd4 : liftstatus(lift) = WAITING
grd1 : (floordoorstatus(lift))(liftposition(lift)) = OPEN
grd1 : liftstatus(lift) = WAITING
grd1 : liftdoorstatus(lift) = OPEN
extends StartLift any
act1 : liftstatus(lift) := MOV ING end
Event ChangeDir =b Models the changing of direction of a STOPPED lift extends ChangeDir
grd1 : liftstatus(lift) = STOPPED grd2 : liftdoorstatus(lift) = CLOSED
act1 : liftdirection(lift) := CHANGE(liftdirection(lift)) end
Event IdleLift =b extends IdleLift
act1 : liftstatus(lift) := IDLE end
Event ActiveateLift =b extends ActiveateLift
grd1 : liftstatus(lift) = IDLE then
grd1 : liftstatus(lift) = STOPPED grd2 : liftposition(lift) ̸= 0
grd3 : liftposition(lift) ̸= MAXFLOOR
grd1 : liftstatus(lift) = STOPPED grd2 : liftdoorstatus(lift) = CLOSED
act1 : liftstatus : |liftstatus′ ∈ LIFT → STATUS ∧
((liftstatus′ = liftstatus ▹− {lift 7→ STOPPED}) ∨
(liftstatus′ = liftstatus ▹− {lift 7→ WAITING})) 20
Idle lifts cannot move
Ready an Idle lift to enable moving
Event MoveUp =b Models a lift moving up to the next floor
extends MoveUp any
grd2 : liftdirection(lift) = UP then
act1 :liftposition(lift):=liftposition(lift)+1
act2 : liftdirection : |liftdirection′ ∈ LIFT → DIRECTION ∧ (liftposition(lift) + 1 = MAXFLOOR
liftdirection′ =liftdirection▹−{lift7→DOWN}) ∧ (liftposition(lift) + 1 ̸= MAXFLOOR
liftdirection′ = liftdirection) Req 5a and 5bReq 5a and 5b
act3 : liftstatus : |liftstatus′ ∈ LIFT → STATUS ∧ ((liftstatus′ = liftstatus ▹− {lift 7→ MOV ING})
(liftstatus′ = liftstatus ▹− {lift 7→ WAITING})
(liftstatus′ = liftstatus ▹− {lift 7→ STOPPED}))
Event MoveDown =b Models a lift moving down to the next floor
extends MoveDown any
grd2 : liftdirection(lift) = DOWN then
act1 :liftposition(lift):=liftposition(lift)−1
act2 : liftdirection : |liftdirection′ ∈ LIFT → DIRECTION ∧ (lif tposition(lif t) = 1
liftdirection′ =liftdirection▹−{lift7→UP}) ∧ (lif tposition(lif t) ̸= 1
grd1 : liftstatus(lift) = MOV ING
grd1 : liftstatus(lift) = MOV ING
liftdirection′ = liftdirection) Req 5a and 5b
act3 : liftstatus : |liftstatus′ ∈ LIFT → STATUS ∧ ((liftstatus′ = liftstatus ▹− {lift 7→ MOV ING}) ∨
(liftstatus′ = liftstatus ▹− {lift 7→ WAITING}) ∨
(liftstatus′ = liftstatus ▹− {lift 7→ STOPPED})) end
CONTEXT Buttons ctx SETS
axm1 : partition(BUTTONS,{ON},{OFF}) Req 17
MACHINE LiftButtons
This machine extends the LiftPlusDoors model to
1) add buttons within each lift by which passengers indicate the floor to which they want to travel;
2) establish a lift schedule associated with each lift.
The lift schedule:
* is used to determine the direction of travel of a lift and the floors at
which the lift should stop
* the lift adopts a strategy by which a lift keeps travelling in its cur- rent direction while the schedule
contains floors in that direction.
This strategy ensures satisfaction of Req21 a & b
REFINES LiftPlusDoors
SEES Lift ctx, Door ctx, Button ctx VARIABLES
lif tposition
lif tstatus
lif tdirection
lif tdoorstatus f loordoorstatus lif tbuttons
lif tschedule
INVARIANTS
inv1 : liftbuttons ∈ LIFT → (FLOOR → BUTTON) inv2 : liftschedule ∈ LIFT → P(FLOOR)
inv3 :∀l,f·l∈LIFT∧f∈FLOOR
(lif tbuttons(l)(f ) = ON ⇒ f ∈ lif tschedule(l))
EVENTS Initialisation
Event SelectFloor =b
act1 :liftposition:=LIFT×{0}
act2 :liftdirection:=LIFT×{UP}
act3 :liftstatus:=LIFT×{IDLE}
act4 : floordoorstatus := LIFT × {FLOOR × {CLOSED}} act5 : liftdoorstatus := LIFT × {CLOSED}
act6 : waiting := ∅
act7 : liftbuttons := LIFT × {FLOOR × {OFF}}
act8 :liftschedule:=LIFT×{∅}
Select floor to stop using lift buttons; also adds floor to liftschedule
lift f loor
act2 : liftschedule(lift) := liftschedule(lift) ∪ {floor} end
Event StartLift =b extends StartLift
Models the starting of a STOPPED lift, maintaining of previous direction
act1 : Event ChangeDir =b
extends ChangeDir any
grd1 : floor ∈ FLOOR
grd2 : liftbuttons(lift)(floor) = OFF
grd3 : floor ̸= liftposition(lift)
act1 :liftbuttons(lift):=liftbuttons(lift)▹−{floor7→ON}
grd1 : grd2 : grd3 : grd4 : grd5 :
grd6 : grd7 :
liftstatus(lift) = STOPPED
liftdoorstatus(lift) = CLOSED floordoorstatus(lift)(liftposition(lift)) = CLOSED liftschedule(lift) ̸= ∅