DESCRIPTION
The gas station (non-queueing) problem is a simulation of a self-serve gas station. It originated in [DBDS93]. In this version of the problem, service is not guarenteed to be provided in a first-come-first-serve manner.
Customers prepay the operator for gas at a specific pump. The operator only keeps track of the number of customers waiting at each pump and activates a pump if there are customers remaining to be served. Once the pump is activated, a customer uses it to pump gas. When the customer finishes, the pump reports the amount of gas actually pumped to the operator who then gives the customer change.
This problem can be viewed using the client-server model. It is similiar to the readers/writers problem in this way. The server includes the operator and pumps which are a scalable collection of co-operating tasks. It provides the services neccessary to obtain gas. The clients are the customers who wish to use these services.
Our implementation of this problem consists of at least 4 tasks; the operator task, 2 pump tasks, and a customer task. It is scalable; both additional pumps and customers can be added.
ADA SOURCE
We chose to only scale the number of customers in the problem not the number of pumps. This means that the size specifies the number of customers there are in the source code. There will always be 2 pumps in each implementation. For example for size 2, there are a total of five tasks: the operator, 2 pumps, and 2 customers.
PROPERTIES
Some specific properties are provided below:
The property specifications by formalism are:
Back to main