Property 5: LTL for INCA-generated SPIN Input

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

Embedded predicates: notifyclienteventa1e1 notifyclienteventa2e1

Defined predicates: e1szEQ0

See the INCA-generated SPIN input for this property.

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: INCA-SPIN

Back to Property 4: INCA-SPIN