Property 0: INCA Query

Requirement: The system does not deadlock.

Pattern: Basic deadlock query

INCA 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