Z Notation

You are asked to specify a car rental system. There are three categories of cars: small, medium and large. Cars can be rented to persons who when renting a car automatically become members. For each category, cars are rented on a first-in first-out basis: when a car is returned, it is placed at the end of a queue. 1) Specify the system and the initial state. 2) Specify a rental operation, with as input a person and a category, and as output a car. Make sure the operation is robust and use schema compo- sition. If a person wants to rent in a category where no car is available, he returns home emptyhanded but is still made a member. 3)Specify an operation where a person returns a car. The operation does not need to be robust. Give the precondition of the operation. 4)Specify an operation with as input a category, and as output all the persons that have rented a car in this category.