Property 9: CTL for INCA-generated SMV Input

Refinement: The program never terminates with an artist registered.

Pattern: Absence

Scope: Global (P is false globally.)

CTL Template: AG!P


   P = term & (e1szGT0 | e2szGT0)

CTL Formula:

AG !(term & (e1szGT0 | e2szGT0))

Embedded predicates: term

Defined predicates: e1szGT0 e2szGT0

See the INCA-generated SMV input for this property.

Up to Property 9: All artists unregister before termination

Back to Property 8: INCA-SMV