c) You are given the following state schema for a hotel room booking system, using types [ROOM] and [PERSON]: Hotel bookedTo: ROOM PERSON cl) What is the detailed meaning of the given specification? What would be a suitable initial state schema (initial state operation)? [5 marks] c2) Write Z specifications for the following two operations: Someone books a room. Query the number of rooms which are currently booked. (Remark: it is not necessary to provide error handling in your answers.) [6 marks]