我正在使用以下规范在软件 NuSMV 中进行考试项目：
一位著名的厨师在乌尔比诺开了一家寿司店。酒吧有一张圆桌，有 N 把椅子供客人就座。厨师将整个上菜时间都花在准备饭菜上，这些饭菜放在盘子里，放在桌子上第一个可用的地方。客户到达酒吧后，要么在餐桌旁就座，要么等待空位。
使用了以下配置变量：
private sem empty = N; // [0..N]
private sem full = 0; // [0..N] 中的值
private sem ready = 0; // [0..N] 中的值
private sem mutex = 1; // {0,1}
private int[] bar 中的值；// N 个位置在构造函数中初始化为 0
private int front = 0;
私人 int 后方 = 0;
私人布尔终端服务=假；
sem 类型是用于拒绝或给予访问的信号量。如果它是正的，可以使用 P（等待）递减，使用 V（信号）递增。信号量 empty、full 和 mutex 用于处理桌子的座位，而 ready 用于处理桌子本身。矢量条描述了桌子上盘子的位置（0 表示那里没有盘子）。变量front 和rear 描述了访问厨师和客户的点。布尔值 endservice 确定厨师是否可以完成餐桌服务。
到目前为止，我已经制作了 3 个模块来模拟厨师、客户端和表（其功能类似于共享对象在多线程中的功能）
这是厨师的模块：
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;
这是处理上述规范中提到的所有变量的表格模块：
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;
最后是表格模块：
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;
我希望这些评论可以让您轻松阅读我正在尝试做的事情。目前我正在研究最终main模块，据我所知，它将所有其他模块连接在一起并设置它们的交互方式。目前它看起来像这样：
-- Main module(unfinished)
MODULE main
VAR
t : table(cook, client)
c : cook(table)
cl : client(table)
我的一个朋友告诉我，即使你想要一个模块的多个实例，你也只需要每个模块中的 1 个就可以在主模块中将它们链接在一起。例如，假设我们想模拟 8 个客户在寿司吧吃饭，我们直到只需要 1 个客户变量，就像我在我的main模块中创建的那样。
但是，如果您查看我的客户端模块的实现，您会发现除了表格模块之外，我还传递了另一个参数：spot它存储了客户希望坐在的座位号。我的理性是，因为客户只有在有盘子的情况下才能吃饭，所以需要检查它所坐的座位前面是否有盘子。为此，它需要跟踪它所坐的座位。那就是我计划使用该spot变量的地方。现在您可能已经猜到了，但是我对这种编程（模型检查）并不是特别方便，而且我不知道这种实现是否正确，但我所知道的是我不知道我是怎么做的将 spot 变量传递给我要模拟的每个客户端。这是怎么做到的？我在正确的轨道上吗？