Description:
The Opens Doors When Ordered To Stop property specifies that whenever the car is ordered to stop at a particular floor, that its doors open before moving on to the next floor.
NOTE: We have to take note of the event of the car reporting that it is approaching a particular floor to check whether the car moved to the next floor after being ordered to stop at the current one.
This property should be valid when analyzed by any of the finite state verification tools.
Specification:
Back to Concurrent Elevator
Back to main