Property 6: CTL for INCA-generated SMV Input

Refinement: Dispatcher never gives event e1 to artist a1 if a1 is not registered for e1.

Pattern: Absence

Scope: Global (P is false globally.)

CTL Template: AG!P

Predicates:

   P = notifyclienteventa1e1 & !isregistereda1e1

AG !(notifyclienteventa1e1 & !isregistereda1e1)

Embedded predicates: notifyclienteventa1e1

Defined predicates: isregistereda1e1

See the INCA-generated SMV input for this property.

Up to Property 6: Dispatcher does not notify wrong artists

Forward to Property 7: INCA-SMV

Back to Property 5: INCA-SMV