Property 9: FLAVERS QRE

Refinement: The program never terminates with an artist registered.

Comments: We rely on Property 1 and Property 8.

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. We want to ensure that the program only exits in this state.

Pattern: None

FLAVERS QRE:

for events {{registered},
            {unregistered}}

show all executions satisfy

[-{registered}, {unregistered}]*;
(
  {registered};
  [-{registered}, {unregistered}]*;
  (
    {registered};
    [-{registered}, {unregistered}]*;
    (
      {registered};
      [-{registered}, {unregistered}]*;
      (
        {registered};
        [-{registered}, {unregistered}]*;
        {unregistered};
        [-{registered}, {unregistered}]*
      )*;
      {unregistered};
      [-{registered}, {unregistered}]*
    )*;
    {unregistered};
    [-{registered}, {unregistered}]*
  )*;
  {unregistered};
  [-{registered}, {unregistered}]*
)*;
[-{registered}, {unregistered}]*

Constraints used to verify this property:

• Task constraint disp.artist1
• Task constraint disp.artist2

Up to Property 9: All artists unregister before termination

Back to Property 8: FLAVERS