Property 1: INCA Query

Part (a)

Refinement, part (a): Artist a1 never registers for event e1 if she is already registered for 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 "a1;dispatcher.unregister_event;art1;e1")
   Q = (rendezvous "a1;dispatcher.register_event;art1;e1")
   R = (rendezvous "a1;dispatcher.register_event;art1;e1")

(defquery "p01a1e1" "nofair"
   (omega-star-less
      (sequence
         (interval
            :initial t
            :open t
            :ends-with '((rendezvous "a1;dispatcher.register_event;art1;e1")))
         (interval
            :ends-with '((rendezvous "a1;dispatcher.register_event;art1;e1"))
            :forbid '((rendezvous "a1;dispatcher.unregister_event;art1;e1"))))))

Part (b)

Refinement, part (b): Artist a1 never unregisters for event e1 unless she is already registered for e1.

Pattern: This is similar to (a), but it is harder to find an event that marks "becoming unregistered". The reason is that the artists start out in the unregistered state. So one cannot simply identify the "becoming unregistered event" with an (rendezvous "a1;dispatcher.unregister_event;art1;e1") occurring. However, part (a) tells us that the artist will never register when registered. Relying on this, we know that a violation to (b) must involve a sequence in which the number of registers equals the number of unregisters (hence the artist is in an unregistered state) and then the artist attempts to unregister.

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

Up to Property 1: Artists register and unregister properly

Forward to Property 2: INCA

Back to Property 0: INCA