Property 1: FLAVERS QRE

Part (a)

Refinement, part (a): Artist a1 never registers for event e1 if she is already 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]*)?

Predicates:

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

FLAVERS QRE:

for events {{disp_dispatcher_register_event_a1_e1},
            {disp_dispatcher_unregister_event_a1_e1}}

show all executions satisfy

(
  [-{disp_dispatcher_register_event_a1_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_dispatcher_register_event_a1_e1}]*;
(
  {disp_dispatcher_register_event_a1_e1};
  [-{disp_dispatcher_register_event_a1_e1},
    {disp_dispatcher_unregister_event_a1_e1}]*
)?

Constraints used to verify this property:

• Task constraint disp.artist1

Part (b)

Refinement, part (b): Artist a1 never unregisters for event e1 unless she is already registered for e1.

Pattern: None

FLAVERS QRE:

for events {{disp_dispatcher_register_event_a1_e1},
            {disp_dispatcher_unregister_event_a1_e1}}

show no executions satisfy

([-{disp_dispatcher_register_event_a1_e1}]* |
 (.*;
  {disp_dispatcher_unregister_event_a1_e1};
  [-{disp_dispatcher_register_event_a1_e1}]*));
{disp_dispatcher_unregister_event_a1_e1};
.*

Constraints used to verify this property:

• Task constraint disp.artist1

Up to Property 1: Artists register and unregister properly

Forward to Property 2: FLAVERS