Property 7: INCA Query

Requirement: If artist a1 registers for event e1 before artist a2 does, then once dispatcher receives e1 from the ADT, it will not notify a2 before notifying a1.

There does not appear to be any pattern which can be used to express this claim with the predicates available to us. So we must make the following query by hand:

INCA Query:

(defquery "p07a" "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 "a2;dispatcher.register_event;art2;e1")))
      (interval
        :forbid '(
          (rendezvous "a1;dispatcher.unregister_event;art1;e1")
          (rendezvous "a2;dispatcher.unregister_event;art2;e1")
          (rendezvous "dispatcher;a1.notify_client_event;e1"))
        :constraints '(
          (>= 1 "accept(adt_wrapper;dispatcher.notify_artists;e1)"))
        :ends-with '(
          (rendezvous "dispatcher;a2.notify_client_event;e1"))))))

Up to Property 7: Dispatcher notifies artists in order

Forward to Property 8: INCA

Back to Property 6: INCA