Not Move With Doors Open Property


Description:

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.


Specification:

 


Back to Concurrent Elevator

Back to main