Property 9: INCA Query

Refinement: The program never terminates with an artist registered.

Pattern: Absence

Scope: Global (P is false globally.)

Template:

  (defquery "global_absence_of_p" "nofair"
    (omega-star-less
      (sequence
        (interval :initial t :ends-with '("P")))))

Predicates:

   P = (rendezvous "artist_manager;a1.terminate_artist-end")
       (rendezvous "artist_manager;a2.terminate_artist-end")

Modifications: Added constraint which says that the sum of all unregister events is strictly less than the sum of all register events. By Property 1, this means that some artist is still registered.

INCA Query:

(defquery "p09a" "nofair"
  (omega-star-less
    (sequence
      (interval
        :initial t
        :ends-with '(
          (rendezvous "artist_manager;a1.terminate_artist-end")
          (rendezvous "artist_manager;a2.terminate_artist-end"))
        :constraints '(
          (<=
            (+ 
              "accept(a1;dispatcher.unregister_event;art1;e1)"
              "accept(a1;dispatcher.unregister_event;art1;e2)"
              "accept(a2;dispatcher.unregister_event;art2;e1)"
              1)
            (+ 
              "accept(a1;dispatcher.register_event;art1;e1)"
              "accept(a1;dispatcher.register_event;art1;e2)"
              "accept(a2;dispatcher.register_event;art2;e1)")))))))

Up to Property 9: All artists unregister before termination

Back to Property 8: INCA