Property 5: FLAVERS QRE

Refinement: If no artists are registered for event e1, dispatcher does not notify any artist of e1.

Comments: Since FLAVERS cannot reference a predicate similar to e1szEQ0, another approach must be taken, and there does not appear to be an applicable pattern for QREs. In attempting to verify this property, we may assume the following:

We never see more registrations for e1 than we have artists (by Property 8)
No artist registers twice without an intervening unregister (by Property 1)
No artist unregisters when she is not registered (again by Property 1)

This means registers/unregisters always come in pairs. To check that no one is registered, we only have to ensure we have seen an equal number of register/unregister pairs. If this is true, we have a point where no one is registered. A notify at this point violates the property.

Pattern: None

FLAVERS QRE:

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

show no executions satisfy

[-{disp_dispatcher_register_event_a1_e1},
  {disp_dispatcher_register_event_a2_e1},
  {disp_dispatcher_unregister_event_a1_e1},
  {disp_dispatcher_unregister_event_a2_e1}]*;
(
  [{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_unregister_event_a2_e1}]*;
  (
    [{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_unregister_event_a2_e1}]*;
    [{disp_dispatcher_unregister_event_a1_e1},
     {disp_dispatcher_unregister_event_a2_e1}];
    [-{disp_dispatcher_register_event_a1_e1},
      {disp_dispatcher_register_event_a2_e1},
      {disp_dispatcher_unregister_event_a1_e1},
      {disp_dispatcher_unregister_event_a2_e1}]*
  )*;
  [{disp_dispatcher_unregister_event_a1_e1},
   {disp_dispatcher_unregister_event_a2_e1}];
  [-{disp_dispatcher_register_event_a1_e1},
    {disp_dispatcher_register_event_a2_e1},
    {disp_dispatcher_unregister_event_a1_e1},
    {disp_dispatcher_unregister_event_a2_e1}]*
)*;
[{disp_artist1_notify_client_event_e1},
 {disp_artist2_notify_client_event_e1}];
.*

Constraints used to verify this property:

Task constraint disp.artist1
Task constraint disp.artist2

Up to Property 5: Dispatcher does not block if no one is registered

Forward to Property 6: FLAVERS

Back to Property 4: FLAVERS