Not Move With Doors Open Property


The Not Moves With Doors Open property specifies that it is never the case that the car can move between floors with its doors open. 

This property should be valid when analyzed by any of the finite state verification tools.



Back to Sequential Elevator

Back to main