Property 4: FLAVERS QRE

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

Pattern: Absence

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

QRE Template: ([- Q]*; Q; [- P,R]*; R)*; [-Q]*; (Q; [- P,R]*)?

Predicates:

   P = {disp_artist1_notify_client_event_e2}, 
       {disp_artist2_notify_client_event_e2}
   Q = {disp_dispatcher_notify_artists_e1}
   R = {disp_dispatcher_notify_artists_e2}

FLAVERS QRE:

for events {{disp_artist1_notify_client_event_e2}, 
            {disp_artist2_notify_client_event_e2},
            {disp_dispatcher_notify_artists_e1},
            {disp_dispatcher_notify_artists_e2}}

show all executions satisfy

(
  [-{disp_dispatcher_notify_artists_e1}]*;
  {disp_dispatcher_notify_artists_e1};
  [-{disp_artist1_notify_client_event_e2},
    {disp_artist2_notify_client_event_e2},
    {disp_dispatcher_notify_artists_e2}]*;
  [{disp_dispatcher_notify_artists_e2}]
)*;
[-{disp_dispatcher_notify_artists_e1}]*;
(
  {disp_dispatcher_notify_artists_e1};
  [-{disp_artist1_notify_client_event_e2},
    {disp_artist2_notify_client_event_e2},
    {disp_dispatcher_notify_artists_e2}]*
)?

Constraints used to verify this property:

• Task constraint disp.dispatcher

Up to Property 4: Dispatcher notifies of what was received

Forward to Property 5: FLAVERS

Back to Property 3: FLAVERS