gisson / es1617 Goto Github PK

The initial model is concerned with the management of the clients. We say that
a client is registered in Z¨ober if he was added to and not yet removed from Z¨ober.
Not all clients are registered in Z¨ober. Those that are registered have a name
and an associated e-mail. A user e-mail should be unique within Z¨ober.
At the beginning there are no registered clients in Z¨ober. One can add new
clients to the system (becoming registered clients), and remove clients from the
system. Clients may also be upgraded to/downgraded from their VIP status.
Notice that all these operations should preserve the conditions above (and
some others specified later in Section 2.6).

client
Upgrades a REGULAR client to VIP

Part of #1

client, name, email
Registers a new client with identifier client, with
the given name, and with the given e-mail

Part of #1

driver
Removes the registered driver driver from Z¨ober

Part of #3

car
Changes the service offered by car to Z¨oberWhite

Part #1

client
Removes the registered client client from Z¨ober

part of #1

driver, name, license Registers a new driver with identifier driver, with
the given name, and with the given driver’s license

Part of #2

This model orchestrates the interactions in Z¨ober.2
Every client may book a ride. A ride is associated with 5 atrributes: a
car, a client, a level of service, and the beggining and end of the ride. As a
simplification, we assume that the beginning and end of a ride are represented as
natural numbers. Consider these to be the number of seconds passed since the
beginning of the year. Upon completion of a ride, the client rates that ride from
1 to 5.
It is also possible for a client to cancel an already booked ride.
Cars registered in Z¨ober provide a given level of service. VIP clients always
book Z¨oberWhite services, whereas regular clients may book Z¨oberY or Z¨oberWhite.
Also, VIP clients may book any number of rides, whereas regular clients can only
book two rides (not completed yet).

car, driver
Associates the registered driver driver to car

Part of #3 and #2

ride
Cancels the previously scheduled ride

Part of #4

This model is supposed to manage the drivers of Z¨ober. We say that a driver is
in Z¨ober if it was added and not yet removed from Z¨ober.
Each driver in Z¨ober has 2 attributes: a name, and a valid driver’s license.
At the beginning there are no drivers in Z¨ober. One can add new drivers to
Z¨ober as long as they do not exist yet in the system, and remove drivers that
already exist in the system. We can also ban drivers from the system, in which
case they will not be able to join again later.
The conditions in which these operations are enabled and the properties they
should satisfy are specified in detail in Section 2.6.

driver
Removes the registered driver driver from Z¨ober,
disallowing him from any future registration. If
driver is the owner of some car, those cars should
also be removed from the system

Part of #2

car Removes car from Z¨ober

Part of #3

ride, srv, client , begin, end
Schedules a new ride ride for this client, in the defined period, for some available car of type srv

Part of #4

Part of #2

car,
driver Associates the registered driver driver to car

Part #2 and #3

This model manages the cars registered in Z¨ober. We say that a car is in Z¨ober
if it was added and not yet removed from Z¨ober.
Each car in Z¨ober has 2 attributes: an owner, and a set of drivers. At the
beginning there are no cars in Z¨ober. One can add cars to Z¨ober as long as they
do not exist yet in the system, and remove cars that exist in the system. One
can also add and remove driver’s from any given car. The maximum number
of drivers per car is 3, and the owner of a car is always a driver of that car.
Moreover, each driver cannot be associated with more than 2 cars.
Cars registered in Z¨ober provide a given level of service, Z¨oberY or Z¨oberWhite,
that can be upgrade (from Z¨oberY to Z¨oberWhite) or downgraded (from Z¨oberWhite
to Z¨oberY). Cars originally provide Z¨oberY service.
The conditions in which these operations are enabled and the properties they
should satisfy are specified in detail in Section 2.6.

car
Changes the service offered by car to Z¨oberWhite

Part of #1

ride, grade
Completes the scheduled ride and assigns the
grade grade to this car

Part of #4

client
Upgrades a REGULAR client to VIP

Part of #1