The final exam will be available at this course wiki on Wednesday April 8 at 7 pm. Solutions need to be submitted before Wednesday April 8 at 9 pm.

The exam will cover the material covered after the midterm. The exam will consist of one question. The question will be somewhat similar to Labs 5, 6, 7 and 8.

Students are allowed to collaborate with each other. There is no limit on the size of a group. Each group submits their solution, including a file named group.txt that contains the names of the group members. Collaborating but not acknowledging collaboration in the submission is academically dishonest.

The instructor will be on Zoom during the exam to answer questions. Students may want to be on Zoom as well so that they can benefit from answers to questions of other students.

A classical concurrency problem, known as the sleeping barber problem, takes place in a barbershop. This problem is originally due to Dijkstra. Given the current COVID-19 outbreak, the problem has been adjusted. The barbershop has one barber, a barber chair, and n chairs (where n is a positive odd number) for waiting customers, if any, to sit on. To ensure that customers practice social distancing, customers are not allowed to sit on adjacent chairs. To address this, the barber has numbered the chairs 0, 1, 2, …, n-1 and there is a note on the door requiring customers to only use the even-numbered chairs.

If there are no customers present, the barber sits down in the barber chair, takes off his face mask, and falls asleep. When a customer arrives, they have to first use hand sanitizer, put on their face mask, and wake up the sleeping barber by calling the barber's cellphone, as has also been mentioned on the note at the door of the barbershop. If additional customers arrive while the barber is cutting a customer's hair, then they also use hand sanitizer and put on their face mask before sitting down (if there still is hand sanitizer and there are empty even-numbered chairs) or they simply leave the shop (if the barber has run out of hand sanitizer or all even-numbered chairs are full). If the last customer for the day notices that the barber has run out of hand sanitizer and that the barber is asleep, then this customer wakes up the barber. Once awake, the barber puts on his face mask and gives hair cuts to waiting customers.

During the test, you are provided with the classes Shop, Barber, Customer, and Main. These classes and some other code will be available at 7 pm here. The APIs of these classes can be found here. During the exam, you are expected to apply JPF to this code in order to verify properties of the code. You should describe how you applied JPF to the code (such as documenting how you configured JPF, which properties you checked, how you added code to the classes to check for particular properties, what output JPF produced, what you concluded from that output, if you detected any bugs (this does not imply that the code contains any bugs) and how you corrected those bugs (if there are any)). Please describe all the steps in sufficient details so that the instructor can reproduce your work. The focus of the exam is on the process of applying JPF to the provided code. You should submit a report describing all the steps, as well as your modified classes (try to make as few, if any, changes as needed), other code that you developed, application configuration files, etc.

Submit all the files, including group.txt, by using

submit 4315 final <name of file>

before 9 pm.