Property 5: CTL for INCA-generated SMV 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.)

CTL Template: AG!P


   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