Group Meeting: Open discussion - "Specifying Elevators with CSP-CASL". We are going to try and use the language of CSP-CASL to specify a complex system (A system of elevator), by starting with an informal, natural language specification of an elevator controller. The specification follows.

An elevator control
The controller is responsible for n ≤ 8 elevators (called cars) serving m ≤ 256 floors. At each floor, there are two call buttons (up and down). (At the first floor, there is no down button and at floor m there is no up button, but this is irrelevant). Within each car there are m destination buttons. For each elevator the controller can issue a command to travel to a certain floor. In response, each car reports to the controller when it reaches a certain floor. The basic use case is: An actor wants to travel with a car. S/He pushes a call button, waits for a car, enters the car, pushes a destination button, travels to destination and leaves the car. (Remark: with a "real" elevator control, there are approximately 600 (!!) more use cases to be considered) The functionality of the controller in this case is: Whenever it receives a floor call, it determines a suitable car for this call. It then sends a car to the passenger. When the passenger pushes a destination button, it sends this car to the destination. For sake of simplicity, we can omit in-between stops for picking up other passengers. However, we have to consider that several passengers enter which want to travel to different destinations. Additionally, when there are no pending calls the controller can decide to send cars to certain parking positions; this is important for saving energy.