Property 6: FLAVERS QRE

Refinement: Dispatcher never gives event e1 to artist a1 if a1 is not registered for e1.

Pattern: Absence

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

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

   P = {disp_artist1_notify_client_event_e1}
   Q = {disp_dispatcher_unregister_event_a1_e1}
   R = {disp_dispatcher_register_event_a1_e1}

Modifications: Added the first four lines to the property. This catches the case where you never register (first clause of the or). The second clause of the or is the pattern preceded by events to ensure you are not notified until after you register for the first time.

FLAVERS QRE:

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

show all executions satisfy

[-{disp_dispatcher_register_event_a1_e1},
  {disp_artist1_notify_client_event_e1}]* 
|
[-{disp_dispatcher_register_event_a1_e1},
  {disp_artist1_notify_client_event_e1}]*;
{disp_dispatcher_register_event_a1_e1};
(
  [-{disp_dispatcher_unregister_event_a1_e1}]*;
  {disp_dispatcher_unregister_event_a1_e1};
  [-{disp_artist1_notify_client_event_e1},
    {disp_dispatcher_register_event_a1_e1}]*;
  {disp_dispatcher_register_event_a1_e1}
)*;
[-{disp_dispatcher_unregister_event_a1_e1}]*;
(
  {disp_dispatcher_unregister_event_a1_e1}; 
  [-{disp_artist1_notify_client_event_e1},
    {disp_dispatcher_register_event_a1_e1}]*
)?

Constraints used to verify this property:

• Task constraint disp.artist1

Up to Property 6: Dispatcher does not notify wrong artists

Forward to Property 7: FLAVERS

Back to Property 5: FLAVERS