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:

• Computation Tree Logic (CTL )
• INCA Query
• Never Claim
• Quantified Regular Expression ( QRE )

Back to Concurrent Elevator

Back to main