问题标签 [model-checking]

我正在关注 Daniel Jackson 的优秀著作（软件抽象）中的一个示例，特别是他设置令牌环以选举领导者的示例。

我正在尝试扩展此示例（Ring 选举）以确保令牌（而不是仅限于一个）在规定的时间内传递给所有成员（并且每个成员只被选举一次，而不是多次）。但是（主要是由于我对合金缺乏经验），我在找出最佳方法时遇到了问题。最初我认为我可以与一些运算符一起玩（将 - 更改为 + ），但我似乎并没有完全击中头部。

下面是示例中的代码。我已经用问题标记了一些区域......感谢任何和所有帮助。我正在使用合金 4.2。

从这个问题跟进...

我有一个完全连通的图，这很棒。我也加入了时间的概念。我现在正在为围绕我的图表传递数据的概念而苦苦挣扎。

我正在为一个系统建模，该系统的任务是确保每个节点都有一个已插入系统的数据副本。我脑子里有关于如何做到这一点的程序，但是我正在努力将其翻译成合金术语。

一个典型的算法看起来像这样：

为简单起见，假设每个节点都有一个唯一的数据，它们必须将该数据提供给所有其他节点。由于这是完全连接的，它应该相对简单（翻译成合金/形式逻辑对我来说有点困难）。

这是我目前所在的位置：

从我的运行谓词中，您可以看到我希望在 20 个时间步内发送所有消息，因此到那时每个 DataMirror 都应该有一组由 5 个唯一消息组成的数据。

我很确定我想做的是让每个 DataMirror 有 2 个属性：

• 要发送的唯一消息（此时可以只是一个简单的变量）
• 收到的消息集（包括原始消息）

当所有 DataMirror 具有相同的消息集时，系统会感到满意。

例如，如果我们有：

那么系统将在以下情况下完成：

我为让任何形式逻辑的高级用户畏缩而提前道歉......我正试图在试炼中学习这一点:)。

是否可以对合金中的随机故障进行建模？

例如，我目前有一个连通图，它以不同的时间步长将数据传递给它的邻居。我想要做的是找出一些允许模型随机终止链接的方法，并且在这样做的过程中，仍然设法实现其目标（确保所有节点的数据状态都设置为 On）。

我试图建模的软件处理不确定性。基本上，节点之间的链接可能会失败，并且软件会沿着另一条路径重新路由。我想在合金中尝试做的是在某些时间步长（最好是随机的）有一些链接到“死”的设施。在最重要的事实中，我有能力使图完全连接，因此，如果一个链接死掉，另一个可能会弥补这一缺陷（因为 simple_change 将 Datum 的状态切换为 On所有连接的邻居）。

编辑：

所以，我按照建议做了并遇到了以下错误：
我很困惑，因为我认为邻居和节点仍然是集合？

这是我更新的代码：

我想在源代码级别自动展开用 C 编写的目标程序中的循环（仅供参考，我使用 linux 和 gcc 编译器）。详细说明，我们看下面的简单源码。

我想将上面的源代码转换如下。

我知道CBMC会自动展开循环以进行软件模型检查，但我不确定 CBMC 是否会将源代码转换为展开循环的源代码。我需要获得一个所有循环都展开的程序源代码。

我试图为此找到工具或解决方案，但我找不到。任何建议或意见将不胜感激。谢谢！

很抱歉让您感到困惑。我将详细解释我的最终目标“在源代码级别展开循环”。我展开循环的最终目标是测量执行从循环展开生成的语句的测试用例的数量。参考下面的一个例子。

当我转换上面的源代码时，我想得到以下源代码

从上面转换的源代码中，我将测量执行来自“循环展开”的每个语句的测试用例的数量。例如，执行第3,4行或第7,8行或第11,12行的测试用例从原始源代码中的第4行和第5行转换而来的测试用例的数量与测试用例执行行的数量不同#4,5 在原始源代码中。

仅供参考，如果有一种方法可以在不展开循环的情况下实现我的最终目标，那么方法也很好！谢谢！

下面是我最近为手机短信完成的一个马马虎虎的合金规格。这只是基本的发短信要求，因为这是一种做法，我没有严格的要求要坚持。但是，我有一些尴尬的问题，例如为什么我不能获得超过 1 对 Name-Mobile 对？为什么 2 个 MessageSets 坚持指向一个 Name？除了问题之外，事实和谓词非常直截了当。请随意批评，因为我需要反馈来学习合金本身。

我在做以下事情时的想法；

一个 Message Box 有 0 个或多个 MessageSet。一套只属于一个人，没有一套是免费的。每组有 1 个或多个消息，由消息行、开始和结束键和行以及光标位置组成。多条消息可以属于同一个人，但一条消息不能同时属于 2 个人。每行有 1 个或多个键，并有它们的开始键和结束键。此外，一行可能有也可能没有新行。每个键可能有也可能没有下一个键。通过触摸板按下按键。每个名字都有一个手机号码，并记录在 ContactList 中。没有两个名字可以有相同的手机，但一个人可以有多个电话号码。

谢谢。

什么是用于检查 Kripke 结构上的不变量的（伪代码）算法，以便在违反不变量的情况下，算法返回的反例具有最小长度？

我正在尝试重现 Dijkstra 在题为“协作顺序进程”的论文中编写的 ALGOL 60 代码，该代码是解决互斥锁问题的第一次尝试，语法如下：

所以我试图在 Promela 中重现上面的代码，这是我的代码：

我要做的是，验证公平属性永远不会成立，因为标签 L1 无限运行。

这里的问题是我的 never claim 块没有产生任何错误，我得到的输出只是说我的语句从未到达..

这是 iSpin 的实际输出

我已经阅读了有关never{..}块旋转的所有文档，但找不到我的答案（这里是链接），我也尝试过使用ltl{..}块（链接）但这只是给了我语法错误，即使它明确在文档中提到它可以在initand之外proctypes，有人可以帮我更正这段代码吗？

谢谢

我正在尝试对以下 LTL 属性的简单 Promela 模型进行模型检查：

我得到一个错误，错误线索上的引导模拟产生以下输出：

现在我看不到“M [0]直到M [1]”在这里被违反。M[0] 在初始化过程中被设置为 1，并且一直如此，直到 M[1] 变为 1。并且跟踪结束得这么早，或者我可能完全误解了“stronguntil”的语义。我非常有信心是这种情况......但我做错了什么？在 Promela 文件中指定 LTL 可以吗？

有问题的模型如下（一个简单的 petri 网）：

我是新手。我想检查转换系统是否满足给定的 LTL 属性。但我不知道如何在 promela 中建模过渡系统。例如下图所示的转移系统有两种状态，初始状态为s0。如何检查LTL属性：<>q是否满足。有人知道如何在 promela 中描述这个问题吗？对了，spin中LTL的next算子怎么用？

就复杂性而言，LTL 公式的大小 |p| 通常是什么意思？原子命题的数量，深度还是其他？

提前致谢！！