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