Gas Station (Non-Queueing) Property Specifications as Never Claims

This page describes the gas station (non-queueing) properties as Never Claims. For other property specification formalisms, click on the name of the property.

One Customer Per Pump property

never {
  do
    :: customer__1[cust_1_pid]@state_5 & 
       customer__2[cust_2_pid]@state_5 -> goto accept
    :: else -> skip 
  od;
  accept:
    do
      :: skip
    od
}
	

Receive Correct Change property

with variables prepay_1_pump_1 and cust_1_pump_2_change:

never {
  do
    :: prepay_1_pump_1 == true &
    :: cust_1_pump_2_change == true -> goto accept
    :: else -> skip
  od;
  accept:
    do
      :: skip
    od
}
	

Back to Gas Station (Non-Queueing)

Back to main