DESCRIPTION
The Sequential Elevator problem models the behavior of a elevator system within a building. The elevator system consists of a controller and a single car. The controller's behavior is modeled explicitly within the system. It accepts requests from the passengers and dispatches the car appropriately. The following commands may be sent to the car: open/close doors, move up/down, continue in the current direction, and stop. The car's behavior is not explicitly modeled within the system. This means the controller is chiefly responsible for the safe and correct functioning of the elevator system.
Our implementation of this problem uses a single task; the elevator. It is not scalable.
ADA SOURCE
The elevator is the single task. This problem cannot be scaled.
size : 1
PROPERTIES
Some specific properties are provided below:
The property specifications by formalism are:
Back to main