2

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

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

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

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

MODULE main
 VAR
  variable : boolean;
 ASSIGN
  init(variable) := true;
  next(variable) := !variable;
 LTLSPEC
  G (variable & X !variable)
 CTLSPEC
  EF (!variable & AX variable)

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

4

1 回答 1

1

如果你能弄清楚命令行来运行你的代码，那么解决方案是：

  1. 安装 NPPExec 插件
  2. 找出您要执行的命令行并对其进行测试
  3. 在 N++ 中，按F6或使用 NPPExec 插件菜单中的等效菜单项
  4. 填写你需要的命令行
  5. 用令牌替换命令行中的文件名"$(FULL_CURRENT_PATH)"- N++ 将把当前文件的文件名放在这里
  6. [可选] 按Save...按钮并保存命令
  7. 按OK按钮运行您的命令
  8. 要重复运行相同的命令，只需按Ctrl+F6

要将命令输出显示到控制台，请按Ctrl+`（1234567890 的左侧键）。

NuSMV 支持从命令行启动，并且在文档的第 4 章（截至今天的当前版本）中提供了大量命令行选项。但是，如果它们仍然不能满足您的要求并且无法从命令行运行您的代码，那么您可能需要考虑自定义编程解决方案（如果您有足够的时间和技能） - 考虑编写自己的 N++ 插件。或者编写可从命令行控制的小工具，该工具使用其 API 调用所有必要的 NuSMV 方法。也许这也可以在 Python 中完成。然后，您只需从 NPPExec 调用您的工具。

于 2014-04-04T11:50:01.597 回答