Requirement: The system does not deadlock.
We use SPIN's built-in ability to check for deadlock. SPIN does this automatically when checking for invalid endstates.
See the violating trail SPIN found for this property.
Up to Property 0: System does not deadlock
Forward to Property 1: Native SPIN