Property 3: INCA Query

Refinement: Dispatcher does not notify any artists of e1 until it receives e1 from the ADT.

Pattern: Precedence

Scope: Global (S precedes P globally.)

Template:

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

Predicates:

  P = (contains "notify_client_event;e1)")
  S = (rendezvous "adt_wrapper;dispatcher.notify_artists;e1")

INCA Query:

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

Note: The ')' at the end of the contains string is not a typo; it is needed so that events e10, e11, etc., are not included in the list.

Up to Property 3: Dispatcher notifies only after receiving

Forward to Property 4: INCA

Back to Property 2: INCA