Property 7: FLAVERS QRE

Requirement: If artist a1 registers for event e1 before artist a2 does, then once dispatcher receives e1 from the ADT, it will not notify a2 before notifying a1.

Pattern: None

FLAVERS QRE:

for events {{disp_dispatcher_register_event_a1_e1},
            {disp_dispatcher_unregister_event_a1_e1},
            {disp_artist1_notify_client_event_e1},
            {disp_dispatcher_register_event_a2_e1},
            {disp_dispatcher_unregister_event_a2_e1},
            {disp_artist2_notify_client_event_e1},
            {disp_dispatcher_notify_artists_e1}}

show no executions satisfy

[-{disp_dispatcher_register_event_a1_e1}, 
  {disp_dispatcher_register_event_a2_e1}]*;
{disp_dispatcher_register_event_a1_e1};
[-{disp_dispatcher_register_event_a2_e1}, 
  {disp_dispatcher_unregister_event_a1_e1}]*;
{disp_dispatcher_register_event_a2_e1};
[-{disp_dispatcher_unregister_event_a1_e1},
  {disp_dispatcher_unregister_event_a2_e1}]*;
{disp_dispatcher_notify_artists_e1};
[-{disp_artist1_notify_client_event_e1},
  {disp_artist2_notify_client_event_e1}]*;
{disp_artist2_notify_client_event_e1};
.*

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
• Task constraint disp.dispatcher

Up to Property 7: Dispatcher notifies artists in order

Forward to Property 8: FLAVERS

Back to Property 6: FLAVERS