Cars

[Gisson]

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.