问题标签 [promela]

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!

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

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

我不太确定这个词是什么意思。我在我们学习并发的课程中看到了它。我已经看到了很多数据交错的定义，但我可以找到有关进程交错的任何信息。

当看到这个术语时，我的直觉告诉我它是使用线程同时运行多个进程，对吗？

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

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

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

我做错了什么？先感谢您

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

比方说，例如，我有以下

我明白了

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

我有一个模型，其中一个进程需要s从集合中随机选择一个元素S。选择部分是一个单一的操作。我在 UPPAAL 中知道的唯一类似的数据结构是数组。

UPPAAL 中是否存在集合数据结构？如果没有，那么我该如何创建一个？

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

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

我有非常简单的发送方-接收方协议：

它发送四个数据包，然后接收它们。然后我尝试证明属性：总是发送意味着最终接收：

ltl pr { [] ( (sent == 1) -> (<> (received == 1)) ) }

...并且什么也没有发生：SPIN 没有找到这个属性证明和它的否定。

为什么？

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

问候阿德里安