问题标签 [nusmv]

Suppose I have following structure M = (S, R, L) where S = {s0, s1, s2} is the set of possible states, R is a transition relation such that: s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2, and L is the labeling function for each state defined by: L(s0) = {p, q}, L(s1) = {q, r}, and L(s2) = {r}. I am using notations describe in Logic in Computer Science textbook by Huth and Ryan.

Clearly, from such model, we have X r is satisfied in s0 (the initial state), since r is satisfied in s1 and s2. My NuSMV code for the Kripke structure is as follows (as described here).

But NuSMV returns that specification X r is false and yields a counterexample.

我正在尝试使用 NuSMV 作为 LTL 公式的可满足性检查器，即我想知道给定公式是否存在模型。我知道 NuSMV 也可以用于此目的，既因为它在理论上是可能的，也因为我看到它在许多处理可满足性的论文中被引用（其中一篇还声称 NuSMV 是最快的可满足性检查器之一那里）。

我看到 NuSMV 附带了一个名为的工具，该工具ltl2smv显然将 LTL 公式转换为 SMV 模块，但后来我不知道如何使用输出。将它直接提供给 NuSMV 会返回一条关于“主”未定义的错误消息，所以我想我必须定义一个主模块并以某种方式使用另一个模块。由于我从未将 NuSMV 用作模型检查器，因此我不知道它的语言是如何工作的，而且鉴于我只需要这个特定的用例，用户指南是压倒性的，顺便说一下，该指南中的任何地方都没有提到它。

那么如何使用 NuSMV 来检查 LTL 公式的可满足性呢？是否有记录此用例的地方？

我是 NuSMV 的新手，并尝试为这个简单的回合制游戏建模。10块积木，每个玩家每回合可以拿1-3块积木，谁拿走最后一块积木获胜。假设玩家 A 先走，这是我的尝试。我想表达“最终会有赢家”，但我的代码不起作用，因为它不会阻止玩家在brick = 0之后拿砖，所以最终玩家a，b都会成为赢家。

这是我的代码：

这是我在 SPEC AF 上的输出（获胜者 = a | 获胜者 = 无）来说明我的观点。

如您所见，模型仍然提供了一个反例，其中玩家 b 在玩 a 已经获胜后赢得了游戏。

I am going through the model checking methods and I want to use the techniques in order to solve a game called Numbers Paranoia lite as a planning problem.

Given an MxN, (MxN > 8), matrix in which each plate is either Problem Image - empty - identified by a unique number ranging from 1 to 8

the goal is to find a path that starts from the plate labelled with 1, covers all the plates in the matrix and ends on the plate labelled with 8. All non-empty plates in a valid path must be sorted in increasing order from 1 to 8.

I am confused with modelling the game into transition state and running NuSMV for results. Here is my solution

我下载了适用于 mac 的 NuSMV 源代码并开始使用自述文件进行安装。但是，有一个步骤要求我在运行时使用“cmake ..”进行构建，但我遇到了问题源目录似乎不包含 CMakeLists.txt。

请问有什么帮助吗？

我已经使用提供的自述文件安装了 NuSMV，但是当我尝试使用 NuSMV 命令时，我收到以下消息：-bash: NuSMV: command not found

互联网上没有太多关于此的信息，所以我会很感激任何帮助

我是 NuSMV 的新手，我正在尝试从 Kripke 结构创建自动售货机实现，我有三个布尔值（硬币、选择、酿造）以及三个状态。但是，当我编译代码时，我收到“第 25 行：在令牌":": syntax error" 如果有人在我的代码中看到任何错误，我将不胜感激。

克里普克结构

我编写代码的尝试如下：

我使用 NuSMV 来验证 Dekker 算法，我的代码如下：

但是反馈就像图片一样，它显示了非法的左操作数类型“：”。它应该是布尔值。我不知道为什么。请帮助我...代码 NuSMV 反馈有什么问题

我的教授决定给我们数学学生一个代码来更改为 NuSMV，我似乎无法在其他任何地方寻求帮助，我只阅读了 6 页的教科书，并且只描述了某些属性的作用。模块 main 是 NuSMV 代码的一个示例，他说使用该格式示例来编写伪代码。我不知道如何编写 while 循环并设置为真？并且 flag1 会是一个状态，然后又会是另一个状态吗？

我需要帮助编写这些 CTL。我还不太了解如何以 NuSMV 格式编写代码，希望我的代码对您有意义，因为它是不完整的 atm。

2）如果一个进程正在等待，它最终会到达它的临界区

3）两个进程必须“轮流”进入临界区

4）一个进程有可能连续两次进入临界区（在另一个进程之前）。

5) 进程 1 连续进入临界区将至少间隔 n 个周期，其中 n 是某个常数。你应该为n选择一个合适的值，并且这个值应该被验证（即，不被证明）。

6）您选择的更多非平凡属性