问题标签 [nusmv]

问问题

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

95 问题

0 投票

2 回答

802 浏览

windows - 执行其他 .exe 后，批处理文件未完全执行

我正在尝试创建应该具有以下命令的批处理文件：

我遇到的问题是：执行第二行后，NuSMV.exe 在 cmd 中运行，其余命令在我退出 NuSMV 之前不会执行，但我想在 NuSMV 中运行命令 3-8。我需要在我的 .bat 文件中进行哪些更改。谢谢。

2011-04-14T21:53:12.237

0 投票

2 回答

502 浏览

logic - 构建有效的 CTL 或 LTL 表达式（在 NuSMV 中）

我正在尝试为 NuSMV 中的模型检查创建一个有效的 CTL 或 LTL 表达式。

我在游戏中有一个变量，演员四处奔跑试图互相抓住。变量是 State_Of_Game : {Win,Lose,Playing}

我想表达的是，从每一个开始状态，游戏都可能输赢。

那么，我将如何在 CTL 或 LTL 中实现这一点？

我在想像 AG (S_O_G = Win | S_O_G = Lose) 之类的东西，但不知道如何实现从每个起始状态都可以看到它。

logic ctl nusmv

2013-12-12T14:44:04.363

0 投票

2 回答

231 浏览

logic - NuSMV 至少 5 个时间步才能获胜

我有一个 NuSMV 程序，我需要在 CTL 或 LTL 中指定程序（这是一个游戏）不能在少于 5 个时间步长内获胜。或更正式：赢得比赛至少需要 5 个时间步长。

我没有明确的时间变量，也不想为验证做一个。有什么方法可以计算已经进行的转换数量吗？访问状态的数量，诸如此类？

目前我有这个：

logic ctl nusmv

2013-12-17T10:26:48.433

0 投票

1 回答

1427 浏览

notepad++ - 如何从记事本++执行.smv文件

我目前正在学习用于 LTL 和 CTL 模型检查的 NuSMV。

我使用 notepad++ 进行编码活动 - 主要是在 python 中 - 我知道我们可以使用 notepad++ 运行 python 脚本（.py 文件）。

我是 NuSMV 的新手，我想知道是否有任何方法可以在 notepad++ 中执行 .smv 脚本。

这是我打算运行的 .smv 代码示例。

但是，使用 NuSMV 交互式 shell 运行上述 SMV 脚本也有一些困难。假设上面的脚本名称是 test.smv。我应该如何使用 NuSMV 交互式 shell 运行它？

notepad++nusmv

2014-04-04T10:36:13.373

0 投票

1 回答

1296 浏览

logic - 如何在 NuSMV 中创建一个简单的 Kripke 模型？

我目前正在做一些 LTL（线性时间逻辑）和 CTL（计算树逻辑）的理论研究。我是 NuSMV 的新手，我很难创建一个简单的 Kripke 结构。

我的结构是 M = (S, R, L) 其中 S = {s0, s1, s2} 是可能状态的集合，R 是转换关系，这样：s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2, L 是每个状态的标记函数，定义为： L(s0) = {p, q}, L(s1) = {q, r}, 和 L( s2) = {r}。我正在使用 Huth 和 Ryan 在计算机科学教科书中的逻辑中描述的符号。我尝试了以下两个代码：

第一个代码：

第二个代码：

出了点问题，我收到了这条消息：“案例条件并不详尽”。这是什么意思？如何解决我的问题？

logic ctl nusmv

2014-04-05T17:18:27.667

0 投票

2 回答

1023 浏览