Property 9: LTL for Native SPIN

Refinement: The program never terminates with an artist registered.

Pattern: Absence

Scope: Global (P is false globally.)

LTL Template: []!P


   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