arrival indication = values: 1-40
NOTES:
indication of floor at which elevator has arrived
at
floor
NOTES:
signal that elevator reached a floor
current floor = values: 1-40
NOTES:
floor number where an elevator is currently located
current-floor = values: 1-40
NOTES:
floor number where an elevator floor is currently located
desired
floor reached
NOTES:
signal
destination direction = [destination-up|destination-down]
destination-down =
NOTES:
signal that required direction is down
destination-floor = values: 1-40
NOTES:
floor numbers where an elevator is scheduled to stop
destination-indication = values: 1-40
NOTES:
indication of floor numbers where an elevator is scheduled
to stop
destination-pending= values: [on
| off]
NOTES:
indication that elevator has destinations subsequent
to current floor
destination-request= @elevator-number+{floor-number}
destination-request-entered
NOTES:
signal that passenger has entered request
destination-request-received
NOTES:
signal that request is ready for scheduling
destination-requests = {destination-request}
destination-schedule = @elevator-number+{destination-floor}+request
-source+destination-pending
destination-schedules= {destination-schedule}
destinations-pending = [summons-pending
| destination-pending | summons-pending + destination-pending]
NOTES:
signal that a destination schedule exists
destination-up
NOTES:
signal that required direction is up
down-direction
NOTES:
*** Generated Entry ***
elevator-control-signal = elevator-up-control+elevator-down-control+elevator-stop-control
elevator-down-control
NOTES:
signal to hardware
elevator-floor = values: 1-40
elevator-not-available
NOTES:
signal that an elevator is not available to honor a
summons request
elevator-number = values: 1-4
elevator-selected
NOTES:
signal that an elevator has been scheduled for a summons
request
elevator-status = @elevator-number+elevator-state+current-floor
elevator-state = [parked|moving-up|moving-down|stopped|out-of-service]
elevator-statuses = {elevator-status}
elevator-stop-control
NOTES:
signal to hardware
elevator-up-control
NOTES:
signal to hardware
floor-number = values: 1-40
NOTES:
*** Generated Entry ***
moving-down
NOTES:
*** Generated Entry ***
moving-up
NOTES:
*** Generated Entry ***
off
NOTES:
*** Generated Entry ***
on
NOTES:
*** Generated Entry ***
out-of-service
NOTES:
signal that elevator has failed to respond to movement
command
overload
NOTES:
signal from hardware
parked
NOTES:
signal
request-received = summons-request-received
+ destination-request-received
request-source = [summons |
destination-floor | summons + destination-floor]
requests = summons-requests + destination-requests
reschedule-elevator
NOTES:
signal to initiate rescheduling summons assigned to
failed elevator
summons-pending = values: [on
| off]
summons-request = @elevator-floor
+ [up-direction | down-direction | up-direction + down-direction]
+ elevator-number
stopped
NOTES:
*** Generated Entry ***
summons
NOTES:
*** Generated Entry ***
summons-indication = values: 1-40
NOTES:
indication of floor numbers where an elevator is scheduled
to stop
summons-request = @elevator-floor
+ [up-direction | down-direction | up-direction + down-direction]
+ elevator-number
summons-request-issued
NOTES:
signal
summons-request-received
NOTES:
signal
summons-requests = {summons-request}
up-direction
NOTES:
*** Generated Entry ***
values
NOTES:
*** Generated Entry ***
Process Specifications
1.1.2
STORE SUMMONS REQUEST
Precondition
input-summons-request occurs
Postcondition
input-summons-request is stored
summons-request-entered is produced
1.1.3
CLEAR COMPLETED SUMMONS
Precondition
There is an elevator-number in elevator-statuses
that matches elevator-number-assigned in summons-request
and
There is a corresponding current-floor in elevator-statuses
that matches floor-number in summons-requests
Postcondition
Corresponding entry in summons-request is null
1.1.4
DISPLAY SUMMONS REQUEST
Precondition
None
Postcondition
summons-requests are displayed
1.2.3
CLEAR COMPLETED DESTINATIONS
Preconditon
There is an elevator-number in elevator-statuses
that matches elevator-number in destination-requests
and
There is a corresponding current-floor in elevator-statuses
that matches floor-number in destination-requests
Postcondition
Corresponding entry in destination-requests is null
1.2.4
DISPLAY DESTINATION REQUEST
Precondition
None
Postcondition
destination-requests are displayed
2.1.2
DETERMINE FINAL DESTINATION
Precondition
There is an elevator-number in elevator-statuses
that matches elevator-number in destination-schedules
and
There is a corresponding current-floor in elevator-statuses
that matches destination-floor in destination-schedules
and
corresponding destination-pending = off in destination-schedules
Postcondition
final-destination-reached is produced
2.1.3
DETERMINE DIRECTION REQUIRED
Local term match is a matching elevator-number in destination-schedules
and elevator-number in elevator-status
Precondition 1
match
exists
and
There exists in destination-schedules a destination-floor
> current-floor in elevator-status
Postcondition 1
destination-up is produced
Precondition 2
match
exists
and
There exists in destination-schedules a destination-floor
< current-floor in elevator-status
Postcondition 2
destination-down is produced
2.2.2
MONITOR FLOOR ARRIVAL
Precondition 1
floor
occurs
Postcondition 1
arrival-indication is cleared
for previous floor
and
arrival-indication is produced
for corresponding floor
and
at-floor is produced
and
current-floor is updated in elevator-statuses
2.2.3
MONITOR ELEVATOR MOVEMENT
current-floor is read from elevator-statuses
Precondition
10 seconds elapse and current-floor is unchanged
Postcondition
move-timeout occurs
2.2.4
STORE ELEVATOR STATUS
Precondition
input
signal is received
Postcondition
elevator-state is updated in elevator-status
2.2.5
DETERMINE DESIRED FLOOR
Precondition
There is an elevator-number in elevator-statuses
that matches elevator-number in destination-statuses
and
There is a corresponding current-floor in elevator-statuses
that matches destination-floor in destination-schedules
Postcondition
desired-floor-reached is produced
3.1.1
SCHEDULE SUMMONS
BEGIN
with summons-request, elevator-status,
and overload
DO WHILE elevator-selected has not been
signaled
Find closest
elevator
IF
elevator is moving in correction direction
or elevator is parked
IF elevator is not overloaded
enter summons-request by elevator-number
in destination-schedule
set request-source to summons
or summons + destination
ENDIF
IF
destination-pending = off
set destination-pending = on
ENDIF
signal
elevator-selected
ELSE
Find next closest
elevator
END
DO
IF no elevator found
Signal elevator
not available
ENDIF
END
3.1.3
CLEAR SUMMONED DESTINATIONS
Precondition
There is an elevator-number in elevator-statuses
that matches elevator-number in destination-schedules
and
corresponding elevator-state = out-of-service
in
elevator-statuses
and
corresponding request-source = summons
in destination-schedules
Postcondition
Corresponding entries of destination-floor are null
3.2.2
SCHEDULE-DESTINATION-REQUEST
Precondition
None
Postcondition
destination-schedules is updated
by destination-requests matching elevator-number
Set request-source = destination or summons + destination
IF destination-pending = off
Set destination-pending = off
ENDIF
3.2.3
UPDATE DESTINATION SCHEDULE
Precondition 1
There is an elevator-number in elevator-statuses
that matches elevator-number in destination-schedules
and
There is a corresponding current-floor in elevator-statuses
that matches destination-floor in destination-schedule
Postcondition 1
Corresponding destination-floor entry is null
Precondition 2
same
condition as Precondition 1
and
no other corresponding destination-floor entries are
present
Postcondition 2
corresponding destination-floor entry is null
and
corresponding destination-pending is set to
off |
