问题标签 [nusmv]

这些天我开始学习 NuSMV。我有这个代码：

我想验证每次我们处于状态“a”时，下一个状态将是状态“b”。哪一个是正确的（即使我尝试了它们并且它们都给了我正确的）：

我的第二个问题是：在上面的模型中，没有从状态“d”到状态“a”的转换，但是当我使用

结果是真的。为什么会这样？

我想在 NuSMv 中制定这个问题：

• 用户可以处于以下三种状态之一：U-need,U-using,U-sad（表示需要服务、开始使用并且他/她对该服务的质量感到满意或开始使用并且他/她分别因为他的服务质量差而感到难过）。

• 服务可以处于以下三种状态之一：S-offer、S-good、S-bad；;（分别代表未使用的服务、提供优质服务或提供劣质服务的服务）。

• 一组事件：look,use,stop,monitor,detect-p,remedy-p，代表寻找服务、开始使用服务、停止使用服务、监控质量、检测服务中的问题并补救分别的问题。

• 这是我的 SMV 代码：

  /li>

- 我想确认这段代码代表了我上面描述的问题 - 我将服务和用户的事件和状态都表示为变量，这是否正确？

我想知道如何计算在 NuSMV 模型检查器中检查 CTL/LTL 属性的执行时间。

... 谢谢

块引用

……

我想声明一个名为 Machine 的数组由 4 个元素组成。每个元素也是一个包含 2 个元素的数组，其中，第一个元素的值是从枚举中获得的： pressionLevel={below, normal, over} 第二个元素的值来自枚举： action={start, pause, stop, restart}

我的第二个问题是如何访问这个数组的元素？

I want to know how to attribute names to properties inside SMV file.

I have done this but only from the terminal (see the following code)

我最近在我的机器上安装了 Ubuntu 19.04（我在这个操作系统上相当新），我正在尝试为一些大学工作安装pynusmv包。

但是，通过运行 pip3 命令来安装它：

我得到一个错误列表并且安装失败。我已经和其他做过同样事情但没有得到任何错误的人交谈过，所以我对导致它的原因感到困惑。

到目前为止，我能找到的唯一区别是我的同学正在运行 Ubuntu 18.04，所以我试图了解问题是否存在。

我尝试了多种方法，例如更新 swig 和其他依赖项，更新 python 和 pip3，安装 python 开发工具；到目前为止，他们都没有工作。

预期结果

Pynusmv 安装成功

实际结果

安装失败。这是我在运行命令时得到的日志的一部分：

之后，它会尝试清理安装，但会出现类似的错误。我还试图通过错误来欺骗自己，并编辑依赖项中明显的拼写错误，但这也不能解决问题（安装继续进行，但在其上运行单元测试只会返回错误）。

有没有办法来解决这个问题？

我必须在我的 Mac 上安装 NuSMV，但我不知道如何安装它。NuSMV 网站上有两个文件，一个是 SourceCode，另一个是二进制文件。我应该安装哪一个？在选择我应该做什么之后，我应该遵循 readme.txt 还是什么？任何帮助将不胜感激，因为互联网上没有太多关于 Mac 的 NuSMV 安装的帮助。PS :- 我已经尝试安装源代码部分并根据 readme.txt 安装它，但我不知道我缺少什么，因为我也不知道运行 smv 文件的程序是什么。

我正在尝试在 NuSMV 中创建一个 4 in a row 实现。不幸的是，我是 NuSMV 的新手，我很难创建它。我尝试为玩家 1 定义所有获胜案例，并使用 2D 数组来表示网格。现在我从 NUSMV 编译器收到一个错误，它在下一个（移动）块中显示：“非法操作数类型的“=”：整数和布尔值”。使用 seq1 到 seq6 定义玩家可以做的所有未来动作（例如，在游戏开始时，玩家只能在前 7 个空格中放置石头）。

我下载了 NuSMV 二进制文件（MacOSX Darwin (x86) 64 位）。

解压后，我前往终端的 bin 文件夹。

我尝试了命令 NuSMV -int，但出现错误：-bash: NuSMV: command not found

我试图临时更改路径：PATH=$PATH:/Users/buzz/Desktop/Hunter/NuSMV/bin echo $PATH

当我回声时，我看到路径就在那里。我再试一次，同样的错误。

如果我手动打开 bin 中标记为 NuSMV 的文件，它会中止：

输入文件为（空）。您必须先设置输入文件。

中止批处理模式

NuSMV 由信号终止

如何让 NuSMV 命令在终端中工作？

谢谢

我正在按照教程在 Windows 10 上安装 NuSMV。它下载正常，但是从压缩 (.tar) 文件夹中提取文件后，我在“bin”文件夹中找不到应该存在的 .exe 文件（当然）。我正在从 NuSMV 网站下载它。我可能做错了什么？