问题描述
我正在使用 nusmv 软件进行一个具有以下规范的考试项目：
一位著名厨师在乌尔比诺开设了一家寿司吧。酒吧有一个回合
桌子有 N 把椅子，客户可以坐在那里。厨师花了整个
服务时间准备他在盘子上和地方上的饭菜
桌子上的第一个可用位置。客户到达酒吧并
要么在餐桌旁坐下，要么等待空位。
使用了以下配置变量：
private sem
空 = N; // [0..N]
中的值 private sem full = 0; // 中的值
[0..N]
私有 sem 就绪 = 0; // [0..N]
私有 sem 中的值
互斥量 = 1; // {0,1}
private int[] bar 中的值； // N 个位置
在构造函数中初始化为 0
private int front = 0;
private int后 = 0;
private bool endservice = false;
sem 类型是用于拒绝或授予访问权限的信号量。有可能
如果使用 P（等待）为正则递减并使用 V 递增
（信号）。信号量 empty、full 和 mutex 用于处理
准备好的桌子座位用于处理桌子本身。这
矢量条描述了桌子上盘子的位置（0 表示
那里没有盘子）。变量front和rear描述的是
访问厨师和客户。布尔端服务决定
如果厨师可以完成上桌。
到目前为止，我已经制作了 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 模块中创建的那样。
但是，如果您查看我的客户端模块的实现，您会发现除了 table 模块之外，我还传递了另一个参数：spot，它存储了客户端希望坐在的座位号。我的理由是，因为客户只有在有盘子的情况下才能吃饭，所以需要检查它所坐的座位前面是否有盘子。为此，它需要跟踪它所坐的座位。这就是我计划使用 spot 变量的地方。现在您可能已经猜到了，但我对这种编程（模型检查）并不是特别熟悉，我不知道这种实现是否正确，但我所知道的是我不知道我是怎么做的将点变量传递给我想要模拟的每个客户端。这是怎么做的？我在正确的轨道上吗？
解决方法
暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！
如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@）