Property 0: LTL for Native SPIN

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