Requirement: The system does not deadlock.
We use SPIN's built-in ability to check for invalid endstates. The SPIN input generated by INCA indicates which endstates are to be considered valid.
See the INCA-generated SPIN input for this property.
See the violating trail SPIN found for this property.
Up to Property 0: System does not deadlock
Forward to Property 1: INCA-SPIN