promela

-2热度

1回答

我在查看如何在Windows 10命令行上使用Spin分析train.pml的输出。任何帮助，使文件给出正确的输出将不胜感激。

1热度

1回答

我正在研究一个相当简单的promela模型。使用两个不同的模块，它充当人行横道/交通灯。第一个模块是输出当前信号的交通灯（绿色，红色，黄色，待定）。该模块还接收作为输入的称为“行人”的信号，该信号用作行人想穿过的指示器。第二个模块充当人行横道。它接收来自交通灯模块的输出信号（绿色，黄色，绿色）。它将行人信号输出到交通灯模块。这个模块简单地定义行人是否在穿越，等待或不在场。我的问题是，在Spin中运

1热度

1回答

Promela使用Spin建模

1热度

2回答

参考Promela LTL声明中的以前状态

我开始使用Promela，并且在表达一些LTL公式时遇到问题。一个示例是以下sequence值，我想断言是单调增加。直觉上我想在下一个状态中写，顺序是> =其前值，但是通过查看文档，我没有看到一种方式来表达这一点。有没有一种方法来表达这种类型的公式？ byte sequence = 0; ltl p0 { [] sequence >= prev(sequence) } ... process

2热度

1回答

使用SPIN进行LTL模型检查

我正在查看SPIN软件。我想用它来找到LTL理论的模型。所有的手册和教程讨论验证算法的属性，但我根本不感兴趣。我只想找到LTL公式的模型（我猜想是相应的Büchi自动机），就像mace4或paradox模型检测器可以找到FOL公式的模型。我相信SPIN应该能够做到这一点，但我无法在文档中找到它。有人能指出任何有用的资源吗？

2热度

1回答

自旋验证，验证变量达到一定的数值

这是我在Stack Exchange上的第一个问题，所以如果有任何违规指标，请告诉我。我有一个用Promela编写的大学OS和并发系统课程。有两个进程正在运行，增加一个变量n。我们的任务是编写这些流程，然后使用Spin中的验证工具来证明n有可能获得值4.我已经通读了所有的命令行参数，但是没有任何结果对我来说，“插入这个修饰符后跟一个变量名来检查所有可能的值。” byte n; proctyp

1热度

1回答

Spin的“深度达到”考虑什么样的状态和转换？

对于使用从未声称验证（带ispin），我得到depth reached产出比 Full statespace search for: never claim + (REQ5) assertion violations + (if within scope of claim) cycle checks - (disabled by -DSAFETY)

1热度

1回答

使用SPIN测试多个LTL公式

我有很多LTL公式，我试图在同一.pml文件上进行测试。我的问题是，当在任何单个公式中发现错误时，跟踪文件被写入（或覆盖）到相同的跟踪文件名。我一直无法找到写入我选择的跟踪文件名的方法。有谁知道这个选项是否存在？如果不是，我可以使用什么策略同时测试同一.pml文件中的多个ltl公式，而不必每次都覆盖相同的跟踪文件？我知道SPIN运行时-x选项，但这只是防止覆盖的跟踪文件。它不会生成具有不同名称

1热度

1回答

如何在promela中实现重复直到（条件）循环？

这将是正确的方法做： repeat{ ... } until(<condition>) 在PROMELA ？我曾尝试： do:: //.. (condition) -> break; od 和 do :: //.. if::(condition) -> break; else fi; od

2热度

1回答

在SPIN公式中使用（U）ntil运算符公式

我想了解如何在ltl公式中正确使用Until运算符。我发现this定义（见下文）是明确的： ù NTIL 甲û B：如果存在真实我使得：中的B是真[s i，s i + 1，s i + 2，... ] 对于所有的j，使得0≤Ĵ< I，式A是真[秒Ĵ，S J + 1，S J + 2， ...] 含义： B是在时间真我为0和i-1之间的时间中，式A为真仍在使用的形式化 “真实在时间i” 示例代码与