Property 2: FLAVERS QRE

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.)

QRE Template: none: .*; Q; [-P]*; R; .*


   P = {disp_artist1_notify_client_event_e1}
   Q = {disp_dispatcher_notify_artists_e1}
   R = {disp_dispatcher_notify_artists_e1}, {disp_dispatcher_notify_artists_e2}

Modifications: Added a prefix to the pattern to represent the condition that a1 needs to be registered for e1.


for events {{disp_dispatcher_register_event_a1_e1},
            {disp_dispatcher_notify_artists_e1}, {disp_dispatcher_notify_artists_e2}}

show no executions satisfy

[{disp_dispatcher_notify_artists_e1}, {disp_dispatcher_notify_artists_e2}];

Constraints used to verify this property:

Up to Property 2: Dispatcher notifies before receiving again

Forward to Property 3: FLAVERS

Back to Property 1: FLAVERS