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.

Notes: Part (a) is essentially a statement of the property with the event "dispatcher calls dispatch_e1.notify_e1" in place of "passing this one on to the artist". In parts (b)-(e) we verify that "dispatcher calls dispatch_e1.notify_e1" is equivalent to "notifying the artists registered for e1 of e1" (at least in the case of a1). In particular:

(b) If a1 is registered for e1 and dispatcher calls dispatch_e1.notify_e1 then dispatch_e1 will notify a1 of e1 before returning.
(c) If a1 is not registered for e1 and dispatcher calls dispatch_e1.notify_e1 then dispatch_e1 will not notify a1 of e1 before returning.
(d) The only task to call dispatch_e1.notify_e1 is the dispatcher.
(e) The only calls to a1.notify_client_event(e1) come from dispatch_e1.

Parts (b)-(e) will also be used to justify some of the other queries below.

Part (a)

Refinement (a): 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 calling dispatch_e1.notify_e1.

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;dispatch_e1.notify_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;dispatch_e1.notify_e1"))))))

Part (b)

Refinement (b): If a1 is registered for e1 and dispatcher calls dispatch_e1.notify_e1 then dispatch_e1 will notify a1 of e1 before returning.

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 "dispatch_e1;a1.notify_client_event;e1")
  Q = (rendezvous "dispatcher;dispatch_e1.notify_e1")
  R = (rendezvous "dispatcher;dispatch_e1.notify_e1-end")

Modifcations: Added constraint representing "a1 is registered for e1" in interval 1, again relying on the veracity of Property 1.

INCA Query:

(defquery "p02b" "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 "dispatcher;dispatch_e1.notify_e1")))
      (interval 
        :ends-with '((rendezvous "dispatcher;dispatch_e1.notify_e1-end"))
        :forbid '((rendezvous "dispatch_e1;a1.notify_client_event;e1"))))))

Part (c)

Refinement (c): If a1 is not registered for e1 and dispatcher calls dispatch_e1.notify_e1 then dispatch_e1 will not notify a1 of e1 before returning.

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 "dispatch_e1;a1.notify_client_event;e1")
  Q = (rendezvous "dispatcher;dispatch_e1.notify_e1")
  R = (rendezvous "dispatcher;dispatch_e1.notify_e1-end")

Modifcations: Added constraint representing "a1 is registered for e1" in interval 1, again relying on the veracity of Property 1.

INCA Query:

(defquery "p02c" "nofair" 
  (omega-star-less 
    (sequence 
      (interval 
        :open t 
        :initial t
        :constraints '(
          (= "accept(a1;dispatcher.register_event;art1;e1)"
             "accept(a1;dispatcher.unregister_event;art1;e1)"))
        :ends-with '((rendezvous "dispatcher;dispatch_e1.notify_e1")))
      (interval 
        :ends-with '((rendezvous "dispatch_e1;a1.notify_client_event;e1"))
        :forbid '((rendezvous "dispatcher;dispatch_e1.notify_e1-end"))))))

Part (d)

Refinement: The only task to call dispatch_e1.notify_e1 is the dispatcher.

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 = (contains "dispatch_e1.notify_e1")

Modifcations: Added :forbid clause to allow calls from dispatcher.

INCA Query:

(defquery "p02d" "nofair"
  (omega-star-less
    (sequence
      (interval :initial t
        :ends-with '((contains "dispatch_e1.notify_e1"))
        :forbid    '((contains "dispatcher;dispatch_e1.notify_e1"))))))

Part (e)

Refinement: The only calls to a1.notify_client_event(e1) come from dispatch_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 = (contains "a1.notify_client_event;e1)")

Modifcations: Added :forbid clause to allow calls from dispatch_e1.

INCA Query:

(defquery "p02e" "nofair"
  (omega-star-less
    (sequence
      (interval :initial t
        :ends-with '((contains "a1.notify_client_event;e1)"))
        :forbid '((contains "dispatch_e1;a1.notify_client_event;e1)"))))))

Up to Property 2: Dispatcher notifies before receiving again

Forward to Property 3: INCA

Back to Property 1: INCA