Property 2: CTL for INCA-generated SMV Input

Refinement: If a1 is registered for e1 and the dispatcher receives e1 from the adt_wrapper then it will not accept another event from the adt_wrapper before passing e1 to a1.

Pattern: Existence

Scope: Between (P becomes true between Q and R.)

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

Predicates:

   P = notifyclienteventa1e1
   Q = afternotifyartistse1 & isregistereda1e1
   R = notifyartistse1 | notifyartistse2

AG((afternotifyartistse1 & isregistereda1e1) -> !E[!notifyclienteventa1e1 U (notifyartistse1 | notifyartistse2)])

Embedded predicates: afternotifyartistse1 notifyclienteventa1e1 notifyartistse1 notifyartistse2

Defined predicates: isregistereda1e1

See the INCA-generated SMV input for this property.

Up to Property 2: Dispatcher notifies before receiving again

Forward to Property 3: INCA-SMV

Back to Property 1: INCA-SMV