Property 2: INCA Query

Refinement: If a1 is registered for e1 and the dispatcher receives e1 from the adt_wrapper then it will not accept another event from the adt_wrapper before passing e1 to a1.

Pattern: Existence

Scope: Between (P becomes true between Q and R.)

Template:

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

Predicates:

  P = (rendezvous "dispatcher;a1.notify_client_event;e1")
  Q = (rendezvous "adt_wrapper;dispatcher.notify_artists;e1")
  R =     (and
            (or (prefix "call") (prefix "accept"))
            (contains "adt_wrapper;dispatcher.notify_artists"))

Modifcations: Added constraint representing "a1 is registered for e1" in interval 1. Here we are relying on the fact that Property 1 has been verified to simplify the interpretation of "a1 is registered for e1".

INCA Query:

(defquery "p02a" "nofair"
  (omega-star-less
    (sequence
      (interval 
        :initial t
        :open t 
        :constraints '(
          (>=
            "accept(a1;dispatcher.register_event;art1;e1)"
            (+ 1 "accept(a1;dispatcher.unregister_event;art1;e1)")))
        :ends-with '(
          (rendezvous "adt_wrapper;dispatcher.notify_artists;e1")))
      (interval
        :ends-with '(
          (and
            (or (prefix "call") (prefix "accept"))
            (contains "adt_wrapper;dispatcher.notify_artists")))
        :forbid '((rendezvous "dispatcher;a1.notify_client_event;e1"))))))

Up to Property 2: Dispatcher notifies before receiving again

Forward to Property 3: INCA

Back to Property 1: INCA