Property 3: CTL for INCA-generated SMV Input

Refinement: Dispatcher does not notify any artists of e1 until it receives e1 from the ADT.

Pattern: Precedence

Scope: Global (S precedes P globally.)

CTL Template: !E[!S U (P & !S)]

Predicates:

   P = notifyclienteventa1e1 | notifyclienteventa2e1
   S = notifyartistse1

!E[!notifyartistse1 U ((notifyclienteventa1e1 | notifyclienteventa2e1) & !notifyartistse1)]

Embedded predicates: notifyartistse1 notifyclienteventa1e1 notifyclienteventa2e1

Defined predicates:

See the INCA-generated SMV input for this property.

Up to Property 3: Dispatcher notifies only after receiving

Forward to Property 4: INCA-SMV

Back to Property 2: INCA-SMV