Description:
The One Customer Per Pump property says that no two customers may be pumping gas from the same pump at the same time. This ensures that access to the pumps is mutually exclusive.
The customers all behave in a symmetric way with regard to the pumps. Due to this, it is sufficient to check this property for an arbitrary pair of customers and any one pump. If these two customers use the pump in a mutually exclusive fashion, then all pairs of customers will. This property is specified in terms of customer 1, customer 2, and pump 1. 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