Property Pattern Mappings for Inca

Property Pattern Mappings for Inca

This page describe mappings for property patterns in Inca. For other information about the patterns click on the pattern links.

Information about the entire pattern system is available at the Specification Patterns Home Page.

Where more than one Inca query is given for a particular pattern/scope pair, all of the given queries must be checked to verify the requirement.

Pattern Mappings

Absence

P is false:

Globally 
(defquery "global_absence_of_p" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("P"))
    )))
Before R 
(defquery "absence_of_p_before_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("R") :require '("P"))
    )))
After Q 
(defquery "absence_of_p_after_q" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :ends-with '("P"))
    )))
Between Q and R 
(defquery "absence_of_p_between_q_and_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :opent t :ends-with '("Q"))
    (interval :ends-with '("R") :require '("P"))
    )))
After Q until R 
(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"))
    )))

Existence

P becomes true:

Globally 
(defquery "global_existence_of_p" "nofair"
  (omega-star-less
   (sequence
    (interval :intitial t :forbid '("P"))
    (interval :perpetual t :forbid '("P"))  
    )))
Before R 
(defquery "existence_of_p_before_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("R") :forbid '("P"))
    )))
After Q 
(defquery "existence_of_p_after_q" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :forbid '("P"))
    (interval :perpetual t :forbid '("P"))
    )))
Between Q and R 
(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"))
    )))
After Q until R 
(defquery "existence_of_p_after_q_until_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :ends-with '("R") :forbid '("P"))
    )))
(defquery "existence_of_p_after_q_until_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :forbid '("P"))
    (interval :perpetual t :forbid '("P"))
    )))

Bounded Existence

In these mappings we illustrate one instance of the bounded existence pattern, where the bound is at most k designated events.

P occurs at most k times:

Globally 
(defquery "p_occurs_at_most_k_times_globally" "nofair"
  (omega-star-less
   (sequence
    (interval :initial :constraints '((> "P" k)))
    )))
Before R 
(defquery "p_occurs_at_most_k_times_before_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("R")
	      :constraints '((> "P" k)))
    )))
After Q 
(defquery "p_occurs_at_most_k_times_after_q" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :constraints '((> "P" k)))
    )))
Between Q and R 
(defquery "p_occurs_at_most_k_times_between_q_and_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :ends-with '("R") :constraints '((> "P" k)))
    )))
After Q until R 
(defquery "p_occurs_at_most_k_times_after_q_until_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval ::constraints '((> "P" k)) :forbid '("R"))
    )))

Universality

Specifying universality in an event-based formalism requires the identification of complementary events. The positive event, P, is defined such that after an occurrence of P states have the property. The negative event, N, is defined such that after an ocurrence of N states fail to have the property. Then we define universality throughout a scope as having seen a P prior to the beginning of the scope with no N until after the close of the scope.

Our assumption is that the initial state of the system has the desired property.

The property holds:

Globally 
(defquery "property_holds_globally" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("N"))
    )))
Before R 
(defquery "property_holds_before_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t: :ends-with '("R") :require '("N"))
    )))
After Q 
(defquery "property_holds_after_q-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q") :forbid '("N"))
    (interval :ends-with '("N"))
    )))
(defquery "property_holds_after_q-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t  :open t :ends-with '("P"))
    (interval :ends-with '("Q") :forbid '("N"))
    (interval :ends-with '("N"))
    )))
Between Q and R 
(defquery "property_holds_between_q_and_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q") :forbid '("N"))
    (interval :ends-with '("R") :require '("N"))
    )))
(defquery "property_holds_between_q_and_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t  :open t :ends-with '("P"))
    (interval :ends-with '("Q") :forbid '("N"))
    (interval :ends-with '("R") :require '("N"))
    )))
After Q until R 
(defquery "property_holds_after_q_until_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q") :forbid '("N"))
    (interval :ends-with '("R"))
    )))
(defquery "property_holds_after_q_until_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t  :open t :ends-with '("P"))
    (interval :ends-with '("Q") :forbid '("N"))
    (interval :ends-with '("N"))
    )))

Precedence

S precedes P:

Globally 
(defquery "s_precedes_p_globally" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("P") :forbid '("S"))
    )))
Before R 
(defquery "s_precedes_p_before_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("P") :forbid '("S" "R"))
    (interval :ends-with '("R"))
    )))
After Q 
(defquery "s_precedes_p_after_q" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :ends-with '("P") :forbid '("S"))
    )))
Between Q and R 
(defquery "s_precedes_p_between_q_and_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :ends-with '("P") :forbid '("S" "R"))
    (interval :ends-with '("R"))
    )))
After Q until R 
(defquery "s_precedes_p_after_q_until_r" "nofair"
  (omega-star-less
   (sequence 
    (interval :initial t :open t :ends-with '("Q"))
    (interval :ends-with '("P") :forbid '("S" "R"))
    )))

Response

S responds to P:

Globally 
(defquery "s_responds_to_p_globally" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P"))
    (interval :forbid '("S"))
    (interval :perpetual t :forbid '("S"))
    )))
Before R 
(defquery "s_responds_to_p_before_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("S"))
    )))
After Q 
(defquery "s_responds_to_p_after_q" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :open t :ends-with '("P"))
    (interval :forbid '("S"))
    (interval :perpetual t :forbid '("S"))
    )))
Between Q and R 
(defquery "s_responds_to_p_between_q_and_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("S"))
    )))
After Q until R 
(defquery "s_responds_to_p_after_q_until_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("S"))
    )))
(defquery "s_responds_to_p_after_q_until_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :forbid '("S" "R"))
    (interval :perpetual t :forbid '("S" "R"))
    )))

Precedence Chain

This illustrates the 2 cause-1 effect precedence chain.

S, T precedes P:

Globally 
(defquery "s-t_precedes_p_globally-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("P") :forbid '("S"))
    )))
(defquery "s-t_precedes_p_globally-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("S") :forbid '("P"))
    (interval :ends-with '("P") :forbid '("T"))
    )))
Before R 
(defquery "s-t_precedes_p_before_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("P") :forbid '("S" "R"))
    (interval :ends-with '("R"))
    )))
(defquery "s-t_precedes_p_before_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("S") :forbid '("P" "R"))
    (interval :ends-with '("R") :require '("T"))
    )))
After Q 
(defquery "s-t_precedes_p_after_q-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :ends-with '("P") :forbid '("S"))
    )))
(defquery "s-t_precedes_p_after_q-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :ends-with '("S") :forbid '("P"))
    (interval :ends-with '("P") :forbid '("T"))
    )))
Between Q and R 
(defquery "s-t_precedes_p_between_q_and_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :ends-with '("P") :forbid '("S" "R"))
    (interval :ends-with '("R"))
    )))
(defquery "s-t_precedes_p_between_q_and_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :ends-with '("S") :forbid '("P" "R"))
    (interval :ends-with '("P") :forbid '("T" "R"))
    (interval :ends-with '("R"))
    )))
After Q until R 
(defquery "s-t_precedes_p_after_q_until_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :ends-with '("P") :forbid '("S" "R"))
    )))
(defquery "s-t_precedes_p_after_q_until_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :ends-with '("S") :forbid '("P" "R"))
    (interval :ends-with '("P") :forbid '("T" "R"))
    )))

This illustrates the 1 cause-2 effect precedence chain.

P precedes (S, T):

Globally 
(defquery "p_precedes_s-t-globally" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("T") :forbid '("P") :require '("S"))
    )))
Before R 
(defquery "p_precedes_s-t_before_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("S") :forbid '("P" "R"))
    (interval :ends-with '("R") :require '("T"))
    )))
After Q 
(defquery "p_precedes_s-t_after_q" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :ends-with '("S") :forbid '("P"))
    (interval :ends-with '("T"))
    )))
Between Q and R 
(defquery "p_precedes_s-t_between_q_and_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :ends-with '("S") :forbid '("P" "R"))
    (interval :ends-with '("R") :require '("T"))
    )))
After Q until R 
(defquery "p_precedes_s-t_after_q_until_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :ends-with '("S") :forbid '("P" "R"))
    (interval :ends-with '("T") :forbid '("R"))
    )))

Response Chain

This illustrates the 2 stimulus-1 response chain.

P responds to S,T:

Globally 
(defquery "p_responds_to_s-t-globally" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("S"))
    (interval :ends-with '("T"))
    (interval :forbid '("P"))
    (interval :perpetual t :forbid '("P"))
    )))
Before R 
(defquery "p_responds_to_s-t_before_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("T") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("P"))
    )))
After Q 
(defquery "p_responds_to_s-t_after_q" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :open t :ends-with '("S"))
    (interval :ends-with '("T"))
    (interval :forbid '("P"))
    (interval :perpetual t :forbid '("P"))
    )))
Between Q and R 
(defquery "p_responds_to_s-t_between_q_and_r" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("T") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("P"))
    )))
After Q until R 
(defquery "p_responds_to_s-t_after_q_until_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("T") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("P"))
    )))
(defquery "p_responds_to_s-t_after_q_until_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("T") :forbid '("R"))
    (interval :forbid '("P" "R"))
    (interval :perpetual t :forbid '("P" "R"))
    )))

This illustrates the 1 stimulus-2 response chain.

S,T responds to P:

Globally 
(defquery "s-t_responds_to_p_globally-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P"))
    (interval :forbid '("S"))
    (interval :perpetual t :forbid '("S"))
    )))
(defquery "s-t_responds_to_p_globally-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P"))
    (interval :ends-with '("S"))
    (interval :forbid '("T"))
    (interval :perpetual t :forbid '("T"))
    )))
Before R 
(defquery "s-t_responds_to_p_before_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("S"))
    )))
(defquery "s-t_responds_to_p_before_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("T"))
    )))
After Q 
(defquery "s-t_responds_to_p_after_q-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :open t :ends-with '("P"))
    (interval :forbid '("S"))
    (interval :perpetual t :forbid '("S"))
    )))
(defquery "s-t_responds_to_p_after_q-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :open t :ends-with '("P"))
    (interval :ends-with '("S"))
    (interval :forbid '("T"))
    (interval :perpetual t :forbid '("T"))
    )))
Between Q and R 
(defquery "s-t_responds_to_p_between_q_and_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("S"))
    )))
(defquery "s-t_responds_to_p_between_q_and_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("T"))
    )))
After Q until R 
(defquery "s-t_responds_to_p_after_q_until_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("S"))
    )))
(defquery "s-t_responds_to_p_after_q_until_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("T"))
    )))
(defquery "s-t_responds_to_p_after_q_until_r-3" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :forbid '("S" "R"))
    (interval :perpetual t :forbid '("S" "R"))
    )))
(defquery "s-t_responds_to_p_after_q_until_r-4" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :forbid '("T" "R"))
    (interval :perpetual t :forbid '("T" "R"))
    )))

Constrained Chain Patterns

This is the 1-2 response chain constrained by a single event.

S,T without Z responds to P:

Globally 
(defquery "s-t_without_z_responds_to_p_globally-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P"))
    (interval :forbid '("S"))
    (interval :perpetual t :forbid '("S"))
    )))
(defquery "s-t_without_z_responds_to_p_globally-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P"))
    (interval :ends-with '("S"))
    (interval :forbid '("T"))
    (interval :perpetual t :forbid '("T"))
    )))
(defquery "s-t_without_z_responds_to_p_globally-3" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P"))
    (interval :ends-with '("S"))
    (interval :ends-with '("T") :require '("Z"))
    )))
Before R 
(defquery "s-t_without_z_responds_to_p_before_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("S"))
    )))
(defquery "s-t_without_z-responds_to_p_before_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("T"))
    )))
(defquery "s-t_without_z-responds_to_p_before_r-3" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("T") :forbid '("R") :require '("Z"))
    (interval :ends-with '("R"))
    )))
After Q 
(defquery "s-t_without_z-responds_to_p_after_q-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :open t :ends-with '("P"))
    (interval :forbid '("S"))
    (interval :perpetual t :forbid '("S"))
    )))
(defquery "s-t_without_z-responds_to_p_after_q-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :open t :ends-with '("P"))
    (interval :ends-with '("S"))
    (interval :forbid '("T"))
    (interval :perpetual t :forbid '("T"))
    )))
(defquery "s-t_without_z-responds_to_p_after_q-3" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :ends-with '("Q"))
    (interval :open t :ends-with '("P"))
    (interval :ends-with '("S"))
    (interval :ends-with '("T") :require '("Z"))
    )))
Between Q and R 
(defquery "s-t_without_z-responds_to_p_between_q_and_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("S"))
    )))
(defquery "s-t_without_z-responds_to_p_between_q_and_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("T"))
    )))
(defquery "s-t_without_z-responds_to_p_between_q_and_r-3" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("T") :require '("Z"))
    (interval :ends-with '("R"))
    )))
After Q until R 
(defquery "s-t_without_z-responds_to_p_after_q_until_r-1" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("S"))
    )))
(defquery "s-t_without_z-responds_to_p_after_q_until_r-2" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("R") :forbid '("T"))
    )))
(defquery "s-t_without_z-responds_to_p_after_q_until_r-3" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("T") :require '("Z"))
    (interval :ends-with '("R"))
    )))
(defquery "s-t_without_z-responds_to_p_after_q_until_r-4" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :forbid '("S" "R"))
    (interval :perpetual t :forbid '("S" "R"))
    )))
(defquery "s-t_without_z-responds_to_p_after_q_until_r-5" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :forbid '("T" "R"))
    (interval :perpetual t :forbid '("T" "R"))
    )))
(defquery "s-t_without_z-responds_to_p_after_q_until_r-6" "nofair"
  (omega-star-less
   (sequence
    (interval :initial t :open t :ends-with '("Q"))
    (interval :open t :ends-with '("P") :forbid '("R"))
    (interval :ends-with '("S") :forbid '("R"))
    (interval :ends-with '("T") :require '("Z"))
    )))