Property 0: LTL for INCA-generated SPIN Input

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