Description:
The Receive Correct Change property says that a customer will never prepay on one pump and get change based on the other pump.
The customers all behave in a symmetric way with regard to the pumps. Due to this, it is sufficient to check this property for any customer and pump. If this customer receives the correct change, then all customers will. This property is specified in terms of customer 1, pump 1, and pump 2. This allows the same property specification to be used when the problem is scaled.
This property should be valid when analyzed by any of the finite state verification tools.
Specification:
Back to Gas Station (Non-Queueing)
Back to main