[2021] Swansea - CS210 Concurrency - Final Exam - Q5 Finite State Process
5. A supermarket has an entrance and an exit. The policy is that at most 3 shoppers will be allowed in a store at any point in time. Therefore the supermarket has deployed an assistant to count how many customers come in, and only allow someone to enter if the store is open and there are fewer than 3 customers in the store. On the other hand, if the store has been closed, then the assistant only allows people to leave. The manager usually instructs the assistant to open or close the store at any time.
Naturally, no one can leave if the store is empty.
(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]
Get the Solution to This Question
WeChat (微信)
WhatsApp
