(2) Suppose we are developing a Z specification of a system that is used to check staff members in and out of a building. Since we will be dealing with elements of staff type, we introduce the type Staff as a basic type: [Staff ]. The state of the system is described by the following schema Log | users, in, out : P Staff in n out = {} 1 in U out = users The state consists of three components modelling the set of users of the system, the set of staff members who are currently in and the set of staff members who are currently out. The predicate part of the state schema describes an Invariant of the system. The invariant says that No staff member is simultaneously in and out. nut. . . The staff member is added to the set in. The staff member is removed from the set out. The set of users of the system is exactly the union of those who are in and those who are out. i. Give a schema Checkin for the operation to check a staff member into the building. [3 marks] ii. Give a schema Checkout for the operation to check a staff member out of the building. [3 marks] iii. Give a schema StaffQuery for a query operation to check whether a particular member of staff is in or out. An output parameter of the following type will be given as follows: Reply == is in | is out [3 marks] iv. Give robust schemas for Checkin and StaffQuery. Your specification should be robust, in the sense that it should capture error situations (such as finding a name which is not registered. The output parameter will be given: Reply == is in | is out | not registered). [4 marks]