问题标签 [spin]

I'm pretty new at spin model checking and wanted to know what this error means:

here is my code:

It actually doesn't have to end, it is a mutual exclusion program that checks if the two processes aren't at the critical section together. Does the error means that the program doesn't end? Thanks!

我正在使用如下代码在验证模式下运行旋转。名为“从不”的函数出现问题。在执行时它给了我一个错误，函数 inc()、dec() 和 reset() 从未完成。但是如果我添加一个循环，它会很好用。根据文档，“从不”检查每一步的变量。那么，为什么没有循环就不行呢？

“从不”阻止，这给了我一个警告

实际上，这不是错误，这是一种警告，在 proctype Inc、Dec、Reset、Init 中显示 unreached。完整的警告日志如下。

我在我教授的课程中使用 Promela 和 Spin 对并发进行建模。我也一直在使用 jspin 前端。我有学生试图在 Windows 8 上安装这些工具，但他们遇到了困难——我不知道这是 64 位还是 32 位的问题，还是他们正在使用的 gcc 版本或其他完全不同的问题。

因此，我正在寻找在 Windows 8 下具有这些工具的工作配置的任何人，他们可以在使用工具链的方式等方面提供一些帮助。

好吧，我有这个（它是代码的一部分）：

在 //////////// 上它卡住了（写入超时），并且没有前进的路，例如到第 40 步。

它是 Ricart-Agrawala 算法的一部分，这里是 et al：

我做错了什么？先感谢您

PS 关键 - 是一个关键部分“模拟器”，因为这个算法适用于分布式系统......

比方说，例如，我有以下

我明白了

我的理解是因为底层变量是 char 类型。但是，我想获得那个 char 的 mtype，有没有办法将一个 char 交叉引用回它的 mtype？

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

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

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

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

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

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

我正在使用 Promela 评估 Spin 进行模型检查，但处理时间对我来说是个问题。我已经看到我可以使用多核来改进计算但是 GPU/Cuda 支持来加速计算呢？我可以这样做吗？

问候阿德里安

在我的设计中，我有N个全局变量和一个方法，该方法将一些提到的参数作为参数，具体取决于状态。

我可以通过引用将全局变量作为参数传递吗？

本文在结论部分明确指出

“Spin 不支持的特殊形式的引用调用参数传递”

还有其他方法可以做到这一点吗？（即传递变量名）

结构如下

PS 我无法使用，例如：

然后检查传递了哪个变量，因为AProcess 无法知道其他变量的存在