6. You are given the code below for a Pot - a monitor class - in a diner problem. Here, customers can take servings and when the pot is empty a chef can refill the pot. Your task is to use the multiverse library for software transactional memory (STM) to make the following code thread safe. [5 marks]
1 public class Pot {
2 private int servingCount ;
3 private int capacity ;
4 Pot ( int capacity ){
5 this . capacity = this . servingCount = capacity ;
6 }
7 public void take () throws Exception {
8 if ( servingCount > 0){
9 servingCount -= 1;
10 }
11 else {
12 throw new Exception (" Pot is empty .");
13 }
14 }
15 public void refill () throws Exception {
16 if ( servingCount == 0){
17 servingCount = capacity ;
18 }
19 else {
20 throw new Exception (" Pot is not empty yet.");
21 }
22 }
23 }
(a) Write the Finite State Process (FSP) code that models the system. Show the LTS for the SuperStore process composed of all component processes. [6 marks]
(b) Specify a safety property in FSP that ensures that there are at most three shoppers in the store at any point in time, and check the SuperStore system. Take a snapshot of the safety run using the LTSA tool, and show the results of the test. [6 marks]
(c) Provide Java code for the monitor in this problem. [5 marks]