问题标签 [model-checking]

我目前正在学习模型检查（模态逻辑、LTL、CTL、SAL 模型检查器等），在业余时间我正在学习 Idris，它是一种支持依赖类型的强类型函数式编程语言。由于我同时关注模型检查和 Idris，我开始对 Idris 与形式方法和模型检查的关系感到好奇。

在学习模型检查时，感觉提出的大多数示例要么是关于验证以命令式方式编写的系统，要么是关于硬件组件。因此，我对模型检查在强类型函数式编程语言中的相关性感到困惑，尤其是在 Idris 等依赖类型语言中，在我看来，类型检查器在验证正确性方面已经做得非常出色。 然而，我的直觉告诉我，模型检查可能与不提供任何终止承诺的部分函数有关。

使用 Idris 等强依赖类型编程语言时，模型检查是否相关？

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

请问有什么帮助吗？

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

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

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

克里普克结构

我编写代码的尝试如下：

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

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

如何在 Windows 上安装 NuSMV 2.6 工具？我尝试但我不能，我不知道如何安装它。我应该在安装 NuSMVV 之前安装任何程序吗？

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

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

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

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

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

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

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

我正在尝试使用 NuSMV 作为 java 中的模型检查器。但是，我无法在线找到相关的 JAR 库。

我在这里找到的唯一一个下载链接不再有效。显然，该库存在，但访问链接不起作用。

有谁知道我如何访问 NuSMV java API 库或知道任何替代方式？

AG(~q ∨ Fp)LTL 公式是否满足以下模型？为什么或者为什么不？

模型？