问题标签 [nusmv]

有人有用 smv（nusmv 或 nuxmv）编写的四骑士拼图的代码吗？我用网格描述了问题，但是当我尝试编写约束/移动时，出现如下错误：

第 35 行：递归定义：S1

在第 43 行的 next(S3) 的定义中

在第 35 行的 next(S1) 的定义中

我理解这个问题，但不知道如何实现这个问题并递归地避免这个问题。

谢谢！

我写了以下代码：

但是，当我执行命令“flatten_hierarchy”时，出现以下错误：“x-1”未定义

我不知道为什么 x-1 是未定义的。

1. 有什么方法可以对 CTL 使用同情心吗？
2. 是否可以选择在同情表达上使用 next(state) 编写表达式？谢谢

我是 NuSMV 的新手。我正在尝试定义一个模块，其中每个状态都有一个持续时间变量，其范围可以从 0 到指定范围。

但是，这会产生语法错误：A variable is expected in left-hand-side of assignment: init(duration) := 0. 我可以通过声明duration来解决这个问题duration : 0..1+bound。

在我的主模块中，我希望计算运行我的模型的总持续时间（或实际计算状态持续时间的所有可能组合，并确保没有组合超过规范中的 ei 3），并确保该变量不超过特定限制.

这是我的主要模块：

我的问题是：当我运行模型时，NuSMV 不断添加到total_duration变量中，因此失败并显示消息“ line 39: cannot assign value 5 to variable total_duration”。这是由于 的声明duration : 0..1+bound，因为在 s0.duration = 0、s1.duration = 0 和 s2.duration = 3 的特定示例中，它将尝试将 1 + 1 + 4 添加到total_duration，因为那是状态的绑定+1。

但是，如果我检查跟踪，total_duration 不会超过 3。我检查了以下规格：

我怎样才能解决这个问题？通过以其他方式声明持续时间或更改其他任何内容？

问题图片

如何将最后一部分（一盏灯只能进行 10 次转换）添加到此代码中？

我正在尝试从源代码编译软件 NuSMV 2.6.0。

• 我克隆了回购https://github.com/hklarner/NuSMV-a
• 我按照 README.md 中的说明进行操作：

但我收到以下错误：

我在 Ubuntu 20.04 LTS 上。我不知道我能做些什么来解决这个问题。它曾经工作过。

任何人都可以帮忙吗？

我正在使用以下规范在软件 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 个模块来模拟厨师、客户端和表（其功能类似于共享对象在多线程中的功能）

这是厨师的模块：

这是处理上述规范中提到的所有变量的表格模块：

最后是表格模块：

我希望这些评论可以让您轻松阅读我正在尝试做的事情。目前我正在研究最终main模块，据我所知，它将所有其他模块连接在一起并设置它们的交互方式。目前它看起来像这样：

我的一个朋友告诉我，即使你想要一个模块的多个实例，你也只需要每个模块中的 1 个就可以在主模块中将它们链接在一起。例如，假设我们想模拟 8 个客户在寿司吧吃饭，我们直到只需要 1 个客户变量，就像我在我的main模块中创建的那样。

但是，如果您查看我的客户端模块的实现，您会发现除了表格模块之外，我还传递了另一个参数：spot它存储了客户希望坐在的座位号。我的理性是，因为客户只有在有盘子的情况下才能吃饭，所以需要检查它所坐的座位前面是否有盘子。为此，它需要跟踪它所坐的座位。那就是我计划使用该spot变量的地方。现在您可能已经猜到了，但是我对这种编程（模型检查）并不是特别方便，而且我不知道这种实现是否正确，但我所知道的是我不知道我是怎么做的将 spot 变量传递给我要模拟的每个客户端。这是怎么做到的？我在正确的轨道上吗？

在我的 NuSMV 脚本中，我试图捕捉 LTLSPEC 的反例的踪迹，但我设法得到它的唯一方法是通过 shell。

是否有可能在易于处理的数据结构中捕获该跟踪？我读过可以以 XML 格式返回，但不幸的是我没能做到。

一定有办法的。

我正在尝试使用 GNuSMV 网站的用户界面安装 NuSMV 检查器，我应用了所有步骤，但它无法正常工作。有没有人可以帮助在我的 64 位笔记本电脑 Windows 10 上运行带有用户界面的 NuSMV？

先感谢您