Requirement: The system does not deadlock.
Scope: Global (
P is false
P = Idle
Idle is built into the
SMV input generated by INCA to denote a point where deadlock
has been reached.
See the INCA-generated SMV input for this property.
See the execution sequence SMV found as a counterexample to this property.
Up to Property 0: System does not deadlock
Forward to Property 1: INCA-SMV