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; .*

Predicates:

   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.

FLAVERS QRE:

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

show no executions satisfy

.*;
{disp_dispatcher_register_event_a1_e1};
[-{disp_dispatcher_unregister_event_a1_e1}]*;
{disp_dispatcher_notify_artists_e1};
[-{disp_artist1_notify_client_event_e1}]*;
[{disp_dispatcher_notify_artists_e1}, {disp_dispatcher_notify_artists_e2}];
.*

Constraints used to verify this property:

• Counter constraint e1_size 0 2
• Enumerated constraint e1_list_1 disp.a_id_type disp_spec a1 a2
• Enumerated constraint e1_list_2 disp.a_id_type disp_spec a1 a2
• Task constraint disp.dispatcher

Up to Property 2: Dispatcher notifies before receiving again

Forward to Property 3: FLAVERS

Back to Property 1: FLAVERS