Gas Station (Non-Queueing) Property Specifications in CTL

This page describes the gas station (non-queueing) properties in Computation Tree Logic (CTL). For other property specification formalisms, click on the name of the property.

One Customer Per Pump property

AG ((( customer_1 = s5 ) -> !( customer_2 = s5 )) &
    (( customer_2 = s5 ) -> !( customer_1 = s5 )))
    

Receive Correct Change property

with variables prepay_1_pump_1 and cust_1_pump_2_change:

AG ( cust_1_pump_2_change -> !prepay_1_pump_1 ) 
    
without additional variables:
    
FAIRNESS
(customer__1_task=s1)
SPEC
AG (
    (customer__1_task=s4) -> A[!(customer__1_task_s1) U
                                  ((operator_task=s29) | 
                                   (operator_task=s24) | 
                                   (operator_task=s14) | 
                                   (operator_task=s20))])
    

Back to Gas Station (Non-Queueing)

Back to main