Gas Station (Non-Queueing) Property Specifications as QREs

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

One Customer Per Pump property

for events { {cust_1_start_pumping}, {cust_1_stop_pumping},
             {cust_2_start_pumping}, {cust_2_stop_pumping} } 
    
show no executions satisfy

[-{cust_1_start_pumping}, {cust_2_start_pumping}]*; 
(
  (
    ( {cust_1_start_pumping}; 
      [-{cust_2_start_pumping}, {cust_1_stop_pumping}]*; 
      {cust_1_stop_pumping}
    ) 
    |
    ( {cust_2_start_pumping}; 
      [-{cust_1_start_pumping}, {cust_2_stop_pumping}]*; 
      {cust_2_stop_pumping}
    )
  ); 
  [-{cust_1_start_pumping}, {cust_2_start_pumping}]* 
)*;
(
  ( {cust_1_start_pumping};
    [-{cust_2_start_pumping}, {cust_1_stop_pumping}]*;
    {cust_2_start_pumping}
  )
  |
  ( {cust_2_start_pumping};
    [-{cust_1_start_pumping}, {cust_2_stop_pumping}]*;
    {cust_1_start_pumping}
  )
);
[{cust_1_start_pumping}, {cust_1_stop_pumping},
 {cust_2_start_pumping}, {cust_2_stop_pumping}]*
	

Receive Correct Change property

for events { {gas_operator_prepay_1_pump_1},
             {cust_1_pump_1_change},
             {cust_1_pump_2_change} }

show all executions satisfy
    
[-{gas_operator_prepay_pump_1}]*;
( {gas_operator_prepay_pump_1};
  [-{cust_1_pump_1_change}, {cust_1_pump_2_change}]*;
  {cust_1_pump_1_change};
  [-{gas_operator_prepay_1_pump_1}]*
)*
	 

Back to Gas Station (Non-Queueing)

Back to main