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.)


  (defquery "global_absence_of_p" "nofair"
        (interval :initial t :ends-with '("P")))))


   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"
        :initial t
        :open t
        :constraints '(
          (= "accept(a1;dispatcher.register_event;art1;e1)"
          (= "accept(a2;dispatcher.register_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