Property 6: INCA Query

Refinement: Dispatcher never gives event e1 to artist a1 if a1 is not registered for e1.

Pattern: Absence

Scope: Global (P is false globally.)


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


   P = "call(dispatcher;a1.notify_client_event;e1)"

Modifications: Added a :constraint which represents a1 not being registered for e1 (relying on Property 1). Added ":open t" to allow multiple occurences of P in the interval.

INCA Query:

(defquery "p06a" "nofair"
        :initial t
        :open t
        :constraints '(
          (= "accept(a1;dispatcher.register_event;art1;e1)"
        :ends-with '("call(dispatcher;a1.notify_client_event;e1)")))))

Up to Property 6: Dispatcher does not notify wrong artists

Forward to Property 7: INCA

Back to Property 5: INCA