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 = (rendezvous "dispatcher;dispatch_e2.notify_e2")
   Q = (rendezvous "adt_wrapper;dispatcher.notify_artists;e1")
   R = (rendezvous "dispatcher;dispatch_e1.notify_e1")

Notes:

INCA Query: Because of Property 2, parts (b)-(e), we know that R (resp. P) is equivalent to notifying registered artists of event e1 (resp. e2).

(defquery "p04a" "nofair"
  (omega-star-less
    (sequence
      (interval
        :initial t
        :open t
        :ends-with '((rendezvous "adt_wrapper;dispatcher.notify_artists;e1")))
      (interval
        :ends-with '((rendezvous "dispatcher;dispatch_e2.notify_e2"))
        :forbid '((rendezvous "dispatcher;dispatch_e1.notify_e1"))))))

Up to Property 4: Dispatcher notifies of what was received

Forward to Property 5: INCA

Back to Property 3: INCA