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.)
CTL Template: AG!P
Predicates:
P = e1szEQ0 & (notifyclienteventa1e1 | notifyclienteventa2e1)CTL Formula:
AG!(e1szEQ0 & (notifyclienteventa1e1 | notifyclienteventa2e1))
Embedded predicates: notifyclienteventa1e1
notifyclienteventa2e1
Defined predicates: e1szEQ0
See the INCA-generated SMV input for this property.
Up to Property 5: Dispatcher does not block if no one is registered
Forward to Property 6: INCA-SMV
Back to Property 4: INCA-SMV