I'm working on an exam project in the software NuSMV with the following specification:
A famous cook opens a sushi bar in Urbino. the bar has a single round table with N chairs where client can seat. The cook spends the whole serving time preparing meals which he serves on plates and places on the first available spot on the table. Clients arrive at the bar and either take a seat at the table or wait for an available seat.
The following configuration variables are used:
private sem empty = N; // values in [0..N]
private sem full = 0; // values in [0..N]
private sem ready = 0; // values in [0..N]
private sem mutex = 1; // values in {0,1}
private int[] bar; // N positions initialized to 0 in a constructor
private int front = 0;
private int rear = 0;
private bool endservice = false;
the sem type is a semaphore used to deny or give access. it can be decremented if it's positive using P (wait) and incremented using V (signal). the semaphores empty, full and mutex are used to handle the seats of the table while ready is used to handle the table itself. the vector bar describes the positions of plates on the table (0 meaning no plate there). The variables front and rear describe points of access to the cook and the clients. The boolean endservice determines if the cook can finish serving the table.
so far I've made 3 modules to emulate the cook, clients and the table(which functions like how a shared object would function in multithreading)
here is the module for the cook:
MODULE cook (table)
VAR
state : {working, serving, served, idle, finished};
endservice : boolean;
ASSIGN
-- The state determines at what cycle the cook is in it's working phase with the options being:
-- 1. Working: The cook has no access to the mutex yet but it would like to deliver a plate to the table.
-- 2. Serving: The cook is currently placing a plate on the table. The cook has the mutex.
-- 3. Served: The cook has finished placing a plate on the table and the mutex can be released.
-- 4. idle: There are no clients on the table that don't have a plate.
-- 5. finished: Serving has finished, only reachable by setting endservice to true, which puts the cook
-- immediately in the state finished from any other state.
-- A diagram of states would look like this:
-- +-----------------------------------------------+
-- | |
-- | -> [WORKING] ------------------> [SERVING] |
-- | | ^ | |
-- | | | | |
-- | | | | |
-- | | +----------- [SERVED] <------+ |
-- | | | | | |
-- | | | | | |
-- | | | | | |
-- | | +----- [IDLE] <--------------+ |
-- | | | | | |
-- | | | | | |
-- | | V V | |
-- | +----------> [FINISHED] <--------+ |
-- | |
-- +-----------------------------------------------+
init(state) := working;
next(state) := case
(endservise = true) : finished; -- finished service.
(table.semReady = N) & (!endservice) : idle; -- no plates to fill.
(table.semReady != N) & (table.semMutex = 0) & (!endservice) : working; -- mutex request.
(table.semReady != N) & (table.semMutex = 1) & (!endservice) : serving; -- inside critical section.
(state = serving) & (!endservice) : served; -- notify end critical section.
TRUE : state;
esac;
-- The variable endservice is used to tedermine when the cook should exit his work cycle and finish execution.
-- Currently it is set to always continue working. In a future implementation the cook will stop working when all
-- clients have finished eating.
init(endservice) := false;
-- The variable endservice is used to tedermine when the cook should exit his work cycle and finish execution.
-- Currently it is set to always continue working. In a future implementation the cook will stop working when all
-- clients have finished eating.
init(endservice) := false;
Here is the module for the table which handles all the variables mentioned in the specification above:
MODULE table (cook, client)
VAR
-- We are emulating a table with 4 spaces to sit and eat sushi, therefore we need a an array to store if each of the 4
-- spots to sit at have a plate in front of them or not.
bar: array 0..3 of boolean;
semEmpty: 0..4; -- The number of empty seats.
semFull: 0..4; -- The number of clients with a plate.
semReady: 0..4; -- The number of clients without a plate.
semMutex: {0,1}; -- A mutex to ensure mutual exclution of the array bar.
front: 0..3; -- the first seat with no plate in the bar.
rear: 0..3; -- the first empty seat at the bar.
ASSIGN
init(bar[0]) := 0;
next(bar[0]) := case
(cook.state = serving) & (front = 0) : 1; -- add plate to the table on spot 1
(client.state = eating) & (client.spot = 0) : 0; -- remove plate from the table on spot 1
TRUE : bar[0];
esac;
init(bar[1]) := 0;
next(bar[1]) := case
(cook.state = serving) & (front = 1) : 1; -- add plate to the table on spot 2
(client.state = eating) & (client.spot = 1) : 0; -- remove plate from the table on spot 2
TRUE : bar[1];
esac;
init(bar[2]) := 0;
next(bar[2]) := case
(cook.state = serving) & (front = 2) : 1; -- add plate to the table on spot 3
(client.state = eating) & (client.spot = 2) : 0; -- remove plate from the table on spot 3
TRUE : bar[2];
esac;
init(bar[3]) := 0;
next(bar[3]) := case
(cook.state = serving) & (front = 3) : 1; -- add plate to the table on spot 4
(client.state = eating) & (client.spot = 3) : 0; -- remove plate from the table on spot 4
TRUE : bar[3];
esac;
-- The semEmpty variable contains the number of empty seats at the sushi bar.
init(semEmpty) := N;
next(semEmpty) := case
(client.state = seated) : semEmpty - 1; -- A client has entered the sushi bar.
(client.state = left) : semFull + 1; -- A client has left the sushi bat.
TRUE : semEmpty;
esac;
-- The semFull variable contains the number of clients with a plate at the table.
init(semFull) := 0;
next(semFull) := case
(client.state = eating) : semFull - 1; -- A client has started eating.
(cook.state = served) : semFull + 1; -- The cook has finished serving a plate.
TRUE : semFull;
esac;
-- The semReady variable is used to see how many clients are seated at the table but don't have a plate of food.
init(semReady) := 0;
next(semReady) := case
(client.state = seated) : semReady + 1; -- A client has entered the sushi bar.
(cook.state = serving) : semReady - 1; -- The cook has placed a plate on the table.
TRUE : semMutex;
esac;
-- The semMutex variable is used as a lock for mutual exclusion on the array variable: "bar". It switches state depending
-- on whether either the cook or client are in a state where they require the mutex lock or are able to release said lock.
init(semMutex) := 0;
next(semMutex) := case
(cook.state = working) & (semMutex = 0) : 1; -- the cook wants to modify "bar", obtain mutex.
(cook.state = served) & (semMutex = 1) : 0; -- the cook has finished modifying "bar", release mutex.
(client.state = seated) & (semMutex = 0) : 1; -- the client wants to modify "bar", obtain mutex.
(client.state = left) & (semMutex = 1) : 0; -- the client has finished modifying "bar", release mutex.
TRUE : semMutex;
esac;
-- The front variable is used to determine where the first open spot is for a cook to place a plate on the table.
init(front) := 0;
next(front) := case
(bar[0] = 0) : 0;
(bar[0] = 1) & (bar[1] = 0) : 1;
(bar[0] = 1) & (bar[1] = 1) & (bar[2] = 0) : 2;
(bar[0] = 1) & (bar[1] = 1) & (bar[2] = 1) & (bar[3] = 0) : 3;
TRUE : front;
esac;
-- The rear variable is used to determine where the first empty seat is at the bar for a new client to sit.
init(rear) := 0;
next(rear) := case
(semEmpty = 0) : 0;
(semEmpty = 1) : 1;
(semEmpty = 2) : 2;
(semEmpty = 3) : 3;
TRUE : rear;
esac;
Finally here is the table module:
MODULE client (table, spot)
VAR
state : {new, seated, eating, left};
ASSIGN
-- The state determines at what cycle the client is in it's eating phase with the options being:
-- 1. New: The client has entered the sushi bar and is looking for a place to sit.
-- 2. Seated: The client has found a place to sit and is waiting for his food to arrive.
-- 3. Eating: The client has food and is able to eat said food.
-- 4. left: The client has finished his food and has left the sushi bar.
-- A diagram of states would look like this:
-- +-----------------------------------------------+
-- | |
-- | -> [NEW] -----------------------> [SEATED] |
-- | | |
-- | | |
-- | | |
-- | +-------------------------------+ |
-- | | |
-- | | |
-- | V |
-- | [EATING] ----------------------> [LEFT] |
-- | |
-- +-----------------------------------------------+
init(state) := new;
next(state) := case
(table.semEmpty != 4) : seated; -- There is an empty spot.
(table.bar[spot] = 1) : eating; -- The client is eating.
(state = eating) : left; -- The client finished eating.
TRUE : state;
esac;
I hope the comments make it easy to read what i'm trying to do. Currently i'm working on the final main module, which as far as I understand connects all other modules together and set's up how they interact. currently it looks like this:
-- Main module(unfinished)
MODULE main
VAR
t : table(cook, client)
c : cook(table)
cl : client(table)
A friend of mine told me that you only need 1 of each module to link them together in the main module, even if you want multiple instances of a module. For example let's say we want to emulate 8 clients eating at the sushi bar, we till only need 1 client variable like I've created in my main module.
however if you look at the implementation of my client module you see that apart from the table module I pass another parameter: spot which stores the number of the seat the client wishes to sit on. My rational is that, because a client can only eat if it has a plate, it needs to check if the seat it's sitting on has a plate in front of it. to do so it needs to keep track of the seat it's sitting on. that's where I planned to use the spot variable. Now you may have guessed it but I'm not particularly handy with this kind of programming(model checking) and I don't know if this implementation is the right way, but what I do know is that I don't know how I pass the spot variable to each client I want to emulate. How is this done? Am I on the right track?