Refinement: The program never terminates with an artist registered.
Pattern: Absence
Scope: Global (P is false
globally.)
LTL Template: []!P
Predicates:
P = term && (e1szGT0 || e2szGT0)LTL Formula:
[]!(term && (e1szGT0 || e2szGT0))
Embedded predicates:
term
Defined predicates:
e1szGT0 e2szGT0
See the INCA-generated SPIN input for this property.
See the Never clause generated by SPIN from this LTL formula
Up to Property 9: All artists unregister before termination
Back to Property 8: INCA-SPIN