QUESTION 1

We need to write Z specifications to record the information about passengers on board an aircraft. Here you are required to produce the specifications using appropriate schemas. Do not consider seat numbers, passengers are allowed on board on a first-come-first-serve basis. Take only a set as the basic type and the condition that at any time there cannot be more passengers than the maximum limit.
(a) Write the schema to represent the current system state.

(b) Write a valid initial state for the system that is at the time when the aircraft is still empty.

(c) Write an operation to allow a passenger to board the aircraft.

(d) Write an operation for the disembarkation of a passenger.

(e) Write a schema to count the number of passengers on board the aircraft.

(f) Write a schema to verify if a passenger called ‘Peter' is on board the aircraft.

QUESTION 2

The University Badminton Club

Here we need to refine the specification for the badminton club given below to describe the activities in the hall which contains one badminton court, where members of the club come to play.
Members in the hall are either playing a game on the court, or effectively in a queue, waiting to play. Here the queue will be modelled as an injective sequence called waiting and we represent those playing a game by onCourt.

The schema to describe the current system state is currently the following:-

[STUDENT] - basic type→maxPlayers: Ν ∩_______________ →maxPlayers = 20 ∪_ClubState__________________________________ →badminton: Π STUDENT →hall: Π STUDENT ∩_______________ →hall ζ badminton →# hall ? maxPlayers ∠_______________________________________

(a)Rewrite the current state schema to describe the activities inside the hall. You may call the new schema for the current system state ClubState2.

(b)Write a schema for the operation of beginning a new game.

(c)Write a schema for the operation of ending a game.

(d)Write a schema for the operation of removing a person from the hall.

(e)Write a schema to specify an operation for a person to enter the hall and join the back of the waiting queue.

QUESTION 3:

A system records the booking of hotel (Le Coco Beach) rooms on one night. Here you are given the following basic types:

• [ROOM] set of all rooms in the hotel
• [PERSON] set of all possible persons

(a) Write a schema to represent the current system state. You must indicate clearly the type of relation you have identified for this system.

(b) Write a valid schema to represent the initial system state.

(c) Write the schema to represent the successful booking of a room by a person called Anthony.

(d) Write the schema to represent the cancellation of a room by a person called Jimmy.

(e)Write the schema to know if a person has already booked the room 007.