Property 4: INCA Query

Requirement: Having received event e1, dispatcher never notifies artists of e2.

Pattern: Absence

Scope: After-Until (P is false after Q until R.)

Template:

  (defquery "absence_of_p_after_q_until_r" "nofair"
    (omega-star-less
      (sequence
        (interval :initial t :open t :ends-with '("Q"))
        (interval :ends-with '("P") :forbid '("R")))))

Predicates:

   P = (contains "notify_client_event;e2)")
   Q = (rendezvous "adt_wrapper;dispatcher.notify_artists;e1")
   R = (contains "notify_client_event;e1)")

INCA Query:

(defquery "p04a" "nofair"
  (omega-star-less
    (sequence
      (interval
        :initial t
        :open t
        :ends-with '((rendezvous "adt_wrapper;dispatcher.notify_artists;e1")))
      (interval
        :ends-with '((contains "notify_client_event;e2)"))
        :forbid '((contains "notify_client_event;e1)"))))))

Up to Property 4: Dispatcher notifies of what was received

Forward to Property 5: INCA

Back to Property 3: INCA