Property 3: FLAVERS QRE

Pattern: Precedence

Scope: Global (S precedes P globally.)

QRE Template: all [-P]* | ([-S,P]*; S; .*)

Predicates:

   P = {disp_artist1_notify_client_event_e1}, 
       {disp_artist2_notify_client_event_e1}
   S = {disp_dispatcher_notify_artists_e1}

FLAVERS QRE:

for events {{disp_artist1_notify_client_event_e1}, 
            {disp_artist2_notify_client_event_e1},
            {disp_dispatcher_notify_artists_e1}}

show all executions satisfy

[-{disp_artist1_notify_client_event_e1}, 
  {disp_artist2_notify_client_event_e1}]* |
(
  [-{disp_dispatcher_notify_artists_e1},
    {disp_artist1_notify_client_event_e1},
    {disp_artist2_notify_client_event_e1}]*;
  {disp_dispatcher_notify_artists_e1};
  .*
)

Constraints used to verify this property:

• Task constraint disp.dispatcher

Up to Property 3: Dispatcher notifies only after receiving

Forward to Property 4: FLAVERS

Back to Property 2: FLAVERS