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
Predicates:
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