Property 5: LTL for Native SPIN

Refinement: If no artists are registered for event e1, dispatcher does not notify any artist of e1.

Pattern: Absence

Scope: Global (P is false globally.)

LTL Template: []!P


   P = e1szEQ0 && (notifyclienteventa1e1 || notifyclienteventa2e1)

LTL Formula:

[]!(e1szEQ0 && (notifyclienteventa1e1 || notifyclienteventa2e1))

See the Never clause generated by SPIN from this LTL formula

Up to Property 5: Dispatcher does not block if no one is registered

Forward to Property 6: Native SPIN

Back to Property 4: Native SPIN