Property 0: CTL for INCA-generated SMV Input

Requirement: The system does not deadlock.

Pattern: Absence

Scope: Global (P is false globally.)

CTL Template: AG!P

Predicates:

   P = Idle

Note: Idle is built into the SMV input generated by INCA to denote a point where deadlock has been reached.

CTL Formula:

AG (!Idle)

Embedded predicates:

Defined predicates:

See the INCA-generated SMV input for this property.

See the execution sequence SMV found as a counterexample to this property.