Property 4: CTL for INCA-generated SMV Input

Requirement: Having received event e1, dispatcher never notifies artists of e2.

Pattern: Absence

Scope: After-Until (P is false after Q until R.)

CTL Template: AG(Q -> !E[!R U (P & !R)])

Predicates:

   P = notifyclienteventa1e2 | notifyclienteventa2e2
   Q = notifyartistse1
   R = notifyartistse2

AG(notifyartistse1 -> !E[!notifyartistse2 U ((notifyclienteventa1e2 | notifyclienteventa2e2) & !notifyartistse2)])

Embedded predicates: notifyartistse1 notifyartistse2 notifyclienteventa1e2 notifyclienteventa2e2

Defined predicates:

See the INCA-generated SMV input for this property.

Up to Property 4: Dispatcher notifies of what was received

Forward to Property 5: INCA-SMV

Back to Property 3: INCA-SMV