问题标签 [model-checking]

检查我的模型时，我想打印所有状态。当发生断言违规时，我们确实会得到一个跟踪文件，但即使没有断言违规，我也想查看状态。我怎样才能做到这一点？

在我的模型检查代码中，我只对找到某个变量的最大值感兴趣。我现在采用的过程是有一个 assert 语句assert( var < MAX_VALUE )，并以二进制搜索方式不断更改 MAX_VALUE。但是，如果 SPIN 真的有办法在一次运行中给出变量的最大可能值，那就更好了。我知道 UPPAAL 有一个sup运营商。SPIN 中是否有任何等价物？

是否有任何操作可以返回 Alloy 中关系的范围和域。

假设我在 Alloy 中定义了一个 sig，如下所示：

我正在寻找要在 r 上应用的操作并给我 B（可能类似于返回 B 的 r[B]）

上面的情况可能看起来很愚蠢，因为 r[B] 会返回 B，所以为什么我一开始不使用 B！实际上，我发现范围和域操作（如果它们存在的话）对于编写事实（约束）非常有用。例如：

任何想法？:)

我想对 HTTP 交互进行建模，即一系列 HTTPRequest/HTTPResponse，并且我试图将其建模为转换系统。我使用以下方法在类 State 上定义了一个排序：

其中状态只是一组消息：

每对 (HTTPRequest->HTTPResponse) 和 (HTTPResponse->HTTPRequest) 在我的转换系统中都表示为一条规则。这些规则在 Alloy 中表示为谓词，可以让一个状态从一种状态移动到另一种状态。

例如，这是在收到特定 HTTPRequest 后生成 HTTPResponse 的规则：

不幸的是，创建的模型似乎太复杂了：我们有十几个规则（比上面的更复杂，但遵循相同的模式）并且执行速度非常慢。

编辑：特别是，CNF 生成非常慢，而求解需要相当长的时间。

您对如何模拟类似的过渡系统有什么建议吗？

非常感谢！

我必须在 NuSMV 中创建 Kripke 的结构，并且我必须检查一些属性。

有人帮我吗？结构和特性（LTL、CTL 和 CTL*）在图片中。

这里有一个结构和性质：

http://cl.ly/image/1x0b1v3E0P0D/Screen%20Shot%202014-10-16%20at%2016.52.34.png

基本上，模型检查处理模型“m”（系统的行为描述）和系统应满足的属性“p”。对于这两个工件，模型检查器确定模型是否满足属性。

我的问题是是否可以将模型“m”指定为 LTL 公式并检查模型作为 LTL“m”是否满足属性“p”。

从理论上讲，我相信这种方法应该有效，因为我们可以生成两个 Büchi 自动机，一个用于 LTL 公式“p”，另一个用于描述模型“m”的 LTL 属性。如果两个非确定性自动机的交集为空，则作为 LTL 的模型“m”满足该性质。

有人可以给我一个提示吗？可能吗？

我想在 Promela 中对物体的弹道轨迹进行建模，并验证模型的一些属性。但是，Promela 没有浮点数据类型。因此，它不能例如计算弹丸运动参数。例如，它无法计算正弦/余弦等三角函数，因此我无法模拟射弹运动。

解决方法是什么？我们如何在 Promela 中对此类系统进行建模？

根据秒。SMT-LIBv2 Language and Tools: A Tutorial 的3.9.3 可以在 SMT-LIBv2中声明这样的复合排序：

我正在使用 CVC4，它似乎接受这种语法。但是我如何访问这些元素？我尝试了以下方法（以及我在网上找到的各种变体）：

但看起来这些运算符只适用于向量和数组。我找不到任何使用这种复合排序的示例，也找不到有关在教程或语言标准中访问这些元素的任何内容。它是如何完成的？还是我完全误解了这个功能的用途？

我的应用程序：我想对一个时间问题进行编码，并希望以将旧状态转换为新状态的状态转换函数的形式进行编码，因此我可以在试验系统时编写如下内容：

我需要使用 UPPAAL 将系统建模为定时自动机，我对 UPPAAL 根据经过时间管理时钟和守卫的方式感到非常困惑：看起来 UPPAAL 只是忽略了时钟守卫！我想我的问题是我正在从一种非常“物理”的方法进行建模，所以我面临着这种问题。

所以这里出现了一个微不足道的自动机。在 UPPAAL 模拟上运行时，我希望它在初始位置和 A 位置之间永远循环，永远不会到 B。但事实并非如此：它在 A 和 B 之间随机交替（至少使用最新的 UPPAAL 快照；我不能尝试版本，因为没有 Linux 64 版本）。

那么我缺少什么？UPPAAL 真的如何对待时钟守卫？

当我第一次遇到这个问题时，我试图做的是模拟超时，所以如果在 30 秒之前没有满足标称行为的保护，自动机就会采取不同的优势。

十分感谢

我想要一些关于我的编码方法的反馈（即，它是否合适，或者我所做的是否可以以更好的方式完成）：

我想创建一个接口来记录构造函数应该具有特定格式。当然，如果接口只包含一个构造函数（我什至惊讶于 PHP 允许您在接口中放置一个构造函数），该接口将不起作用（除了可能的文档）。此外，PHP 不强制任何可调用的参数匹配，无论是数量还是类型，函数、方法和构造函数都是如此。

如果你看到我是如何命名我的类的，你就会意识到我正在尝试做什么（：记录构造函数参数必须是一个消息器实例，太糟糕了，我无法做更多的事情来强制执行）。请让我知道我的方法是否可行以及我是否可以改进它。

考虑到上面的简单类，我想创建一个如下所示的接口，但是由于我们正在处理 PHP 构造函数，这应该没用吗？

然后我想在一个名为Runner如下的类中强制执行我的接口：

最后运行这段代码：

输出：