Property 5: INCA Query

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

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 = (and (prefix "call") (contains "notify_client_event;e1)"))

Modifications: Added a :constraint which represents the condition that no artist is registered for event e1 (relying on Property 1). Added ":open t" to allow multiple occurences of P in interval.

INCA Query:

(defquery "p05a" "nofair"
  (omega-star-less
    (sequence
      (interval
        :initial t
        :open t
        :constraints '(
          (= "accept(a1;dispatcher.register_event;art1;e1)"
             "accept(a1;dispatcher.unregister_event;art1;e1)")
          (= "accept(a2;dispatcher.register_event;art2;e1)"
             "accept(a2;dispatcher.unregister_event;art2;e1)"))
        :ends-with '(
          (and (prefix "call") (contains "notify_client_event;e1)")))))))

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

Forward to Property 6: INCA

Back to Property 4: INCA