问题标签 [model-checking]

我下载了 nusmv-2.6.0.tar.gz 并按照 nusmv-2.6.0/nusmv/README.TXT 中的自述文件进行构建，但出现了一些问题。我想某处可能有错误的配置，但我没有找到它。

错误信息

我已经安装了 readline-common ，这是新的输出，

`

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 公式的可满足性呢？是否有记录此用例的地方？

考虑这个简单的 PROMELA 模型：

我想用这个简单的声明来验证这个模型，它是使用 spin -f 生成的：

但是，使用验证

没有结果。尝试 -a 选项也不会产生结果。任何随机模拟都表明，在某些时候显然 p 是错误的，那么尽管我用自旋生成了它，为什么 never 声明不起作用？

我错过了一些基本的东西吗？

这是我的合金代码：

所以我想添加一个断言，即两个 Patron 目前不能拥有同一本书。这是我提出的断言：

因此，当检查断言时：

合金没有找到任何反例。但是当我使用 run 命令时，Alloy 给了我很多反例：

另外，我读到添加一个否定有效断言的事实不应该给出任何实例。我补充说：

当我运行模型时，Alloy 会找到有效的实例。

我究竟做错了什么？谢谢你。

我正在使用 Windows 操作系统并在 Cygwin 中输入：wish -f ispin.tcl打开 ispin 界面。我打开一个文件test.pml，其中包含：

之后，我使用种子 = 123 的随机方式运行它。结果打印在输出中没有问题：

当我尝试验证此模型时出现问题。验证结果为：

我该如何解决这个问题？我在互联网上搜索，但找不到可以帮助我的东西。

注意：我没有更改任何验证属性：

[] = 总是

O = 下一个

！= 否定

<> = 最终

想知道 []<> 是否等同于 []？

也很难理解如何分配时间逻辑。

1. [][] (a OR !b)

2. !<>(!a AND b)

3. []([] a ==> <> b)

我正在尝试在 Ubuntu 中将CBMC Bounded Model Checker 用于 C 和 C++ 程序。我已经下载了 gcc (4.9 v) 和 g++ (4.9 v) 编译器，并通过终端安装了 CBMC。

我能够使用以下过程验证 C 程序并且没有出现任何问题：

具有名称的 .c 文件file2.c：

在终端类型中：

输出：

当我尝试执行以下 .cpp 文件时出现错误。

sum_num.cpp文件：

输入终端：

输出 - 错误：

我是 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