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