Requirement: The system does not deadlock.
Pattern: Basic deadlock query
(defquery "pDLa" "nofair" (omega-star-less (sequence (interval :initial t :progress t :costs "connect-arc-unit-self-loops-bad"))))
See the violation INCA found for this property (with the help of CPLEX).
Up to Property 0: System does not deadlock
Forward to Property 1: INCA