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

Template:

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

Predicates:

   P = "call(dispatch_e1;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"
  (omega-star-less
    (sequence
      (interval
        :initial t
        :open t
        :constraints '(
          (= "accept(a1;dispatcher.register_event;art1;e1)"
             "accept(a1;dispatcher.unregister_event;art1;e1)"))
        :ends-with '("call(dispatch_e1;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