Property 9: LTL for INCA-generated SPIN Input

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))

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