Requirements of the system

• The filling station may have several pumps.
• Cars arrive at a pump to be serviced.
• Each pump has an associated queue of cars waiting to be serviced. This queue may be empty. Cars join on of these
• queues when they arrive.
• Cars sometimes leave before being serviced.
• Cars sometimes switch queues.

The specification starts by introducing the set of all petrol pumps and the set of all cars.

[PUMP,CAR]

The system state

The state of the system is specified in the following schema.

We specify a partial function queues from a petrol pump to an injective sequence of cars queuing at that pump. A sequence is a natural way to model a queue because it captures the importance of ordering. The fact that the sequence is injective ensures that no car sppears in the same queue more than once at any time. The set serviced is used to model the set of cars which have just filled up with petrol and are about to leave the filling station.

The schema also constrains the system such that no car may appear in more than one queue at the same time and no car can be both in a queue and in the set of cars that are serviced.

The Initial state

initially all of the queues at the pumps are empty and no cars have been serviced.

The arrival of a car

When a car arrives at the filling station it joins the end of one of the queues. The set of serviced cars in unaffected.

Leaving

Ordinarily, cars leave having bought petrol.

Here we specify that a car must be at the head of a queue in order to get petrol. When the car has filled up it joins the set of cars that have been serviced. It leaves the queue of cars at pump p? and the queue is replaced by its tail.

Utility Function Specification - Generic Definition

SymbolDefinition: function left 30 ( _ cofilter _ )

If s is a sequence and V is a set, s cofilter V is a sequence which contains those elements of s which are not members of V in the same order as they appear in s.

Sometimes drivers leave the filling station before they have bought petrol.

When a car leaves without buying petrol is does not move into the set of cars that are serviced. A car leaving in such a way can leave from any position in the queue. The utility function cofilter (specified elsewhere in this document) removes the car from the queue and rebuilds the sequence of cars that are left at the pump.

Switching queues

Sometimes drivers swap queues if they think they can be serviced quicker.

Switching ¡ LeavesUnhappy † Arrive

The event of swapping queues is considered to be equivalent to leaving one queue and joining the end of another.

Driving away

ÚÄDriveAwayÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œFillingStation
³ car? : CAR
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ car? ç ran (U (ran queues))
³ car? î serviced
³ queues' = queues
³ serviced' = serviced \ {car?}
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

Once a car has been serviced it will leave the filling station. A car that is serviced cannot be in one of the queues at the pumps. In driving away the car will rejoin the world of cars that, as most of us know to our cost, will once again require petrol.