## 3 Two Motivating Examples
### Example: Lift Safety in Emergency  
The next example is adapted from the problem descriptions in [35; 36]:  
_A lift that guarantees safe operation is needed. Normally, the lift provides timely transport service to passengers by taking requests and stopping at the requested floors. However, in the case of an emergency, such as a power outage, a mechanical/electrical malfunction, or an earthquake, the lift must come to a full stop at the nearest floor in the direction of travel, open its doors and keep them open, give safety warnings across all floors, and cancel any outstanding requests._  
In Figure 3, two scenarios are used to specify the requirements. The first scenario (lines 1-7) stipulates that when an emergency has been detected (line 3), the first Then step requires for the lift to stop (line 4), give warning (line 5), and cancel outstanding requests (line 6). The next Then step (line 7) requires that the doors should be open after a short delay for the passengers to exit safely. The first scenario specifies the \"normal path\" of the lift system's response to an emergency. It should be kept in mind that it is possible for any step to fail. In the example, the lift can fail to stop at the first Then step (line 4). Under _the failing-fast policy_, the warning step (line 5), the cancellation step (line 6), and the subsequent Then step (line 7) are skipped. Omission for the former two steps can cause confusion for passengers, but omission of the latter step can pose great risk for passengers. If the doors fail to remain closed, a large gap can open up between the lift and the landing will, which could put the passengers inside the lift in a life-threatening danger as they may attempt to get out of the lift through the gap. The safety requirement must steer the lift and doors clear  
Figure 2: Scheduled sprinkling. It is not possible to fix the problem by turning off the failing-fast feature of the supporting tool used to run the scenario:  
* When the feature is turned off for the whole scenario, the two And steps (lines 5-6) and the Then step (line 7) will be executed. The execution of the two And steps are desirable and correctly checks the warning and cancellation of outstanding requests. Unfortunately, the checking of the lift doors of the Then step can be _misleading_: if it passes, the doors are open when the lift is either in motion or does not stop aligning with the landing, putting the passengers in danger; and if it fails, the doors are correctly closed for passenger safety;
* When the feature can be turned off at the step level, failing-fast at the first Then step (line 4) must be turned off to guarantee execution of the warning and cancellation steps, but doing so could lead to the execution of checking lift doors and obtain a misleading result when the lift has failed to stop. On the other hand, keeping the failing-fast behavior prevents warning and cancellation steps if the first Then step fails. Either way, potential safety checking omissions exist. In summary, the checking of the lift doors of the Then step should take place _only if_ the lift has successfully stopped at the first Then step (line 4), and the checking of warning and request cancellation should be executed _only if_ the lift has failed to stop. For the safety requirement to be completely specified, the second scenario (lines 9-12) is necessary. If the lift fails to stop properly at a floor in an emergency (lines 10-11), the lift doors must remain closed to keep the passengers safe (line 12), presumably to wait for rescue. Note how the situation is encoded in the Given step and the But step. Table 1 lists the combinations of the states of the lift and the lift doors. The lift may or may not be stopped at the nearest floor, and the lift doors may be open or closed. The first scenario in Figure 3 (line 7) checks that the doors are open in success or closed in failure when the lift is stopped at the nearest floor.