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

Predicates:

   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