Gas Station (Non-Queueing) Property Specifications as INCA Queries

This page describes the Gas Station (Non-Queueing) properties as INCA queries. For other property specification formalisms, click on the name of the property.

One Customer Per Pump property

(defquery "no_c1c2" "nofair"
  (omega-star-less 
    (sequence
      (interval :initial t 
                :open t 
                :ends-with '("call(cust_1-task;pump_1-task.start_pumping)"
                             "call(cust_2-task;pump_1-task.start_pumping)")))))
    

Receive Correct Change property

(defquery "no_c1p2" "nofair" 
  (omega-star-less 
    (sequence 
      (interval :initial t
                :open t
                :ends-with '((rend "operator-task;customer_1-task.operator-prepay_1_pump_1-end")))
      (interval :ends-with '((rend "operator-task;customer_1-task.change"))
                :require '((rend "pump_2-task;operator-task.charge_1_pump_2"))
                :forbid '((rend "pump_1-task;operator-task.charge_1_pump_1"))))))

with constraints:

(defquery "no_c1p2_con" "nofair"
  (omega-star-less
    (sequence
      (interval :initial t
                :open t
                :ends-with '((rend "operator-task;customer_1-task.change"))
                :constraints '(>= 
                                ( - "call(operator-task;customer_1-task.operator-prepay_1_pump_1-end)"
                                    "call(pump_1-task;operator-task.charge_1_pump_1)")
                                2)))))
    

Back to Gas Station (Non-Queueing)

Back to main