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))
See the Never clause generated by SPIN from this LTL formula
Up to Property 9: All artists unregister before termination
Back to Property 8: Native SPIN