A central computer, connected to remote terminals via communication links, is used to automate seat reservations for a concert hall. A booking clerk can display the current state of seat reservations on the terminal screen. In order to book a seat, a client chooses a free seat and then the clerk enters the number of the chosen seat at the terminal and issues a ticket. A system is required which avoids the double-booking of seats while allowing clients free choice of the available seats.

(a) Construct a model and prove that the model does not permit double-booking.

(b)Construct a model using Petri Nets (any kind).

(c) Write a Java program implementing the seat reservation system.

Hint:

(a) For the LTSA model possible processes are SEAT, CLERK (or CLIENT). Moreover, it is only necessary to model a small number of them.

(c) For the Java implementation, identify properly the active and passive processes. Moreover, implement the selection of a seat by a client as a procedure which selects a seat randomly.