问题标签 [promela]

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

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

本文在结论部分明确指出

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

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

结构如下

PS 我无法使用，例如：

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

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

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

理想情况下，我会喜欢这样的东西：

但据我所知，这是行不通的。有没有办法做到这一点，而不是这样？

我目前正在学习 Promela/Spin。我遇到的问题是我无法验证我的程序。

我创建我的平移文件： spin_64bits.exe -a x.pr --- 一切都很好，直到这里。

现在，当我尝试通过gcc pan.c (gcc -o pan pan.c, 不管) 编译 pan.c 时，我收到一个错误，即存在对随机和随机的未定义引用。

注意：当我分别用 srand() 和 rand() 交换它们时它确实有效，但老实说，我不想在每次想要运行验证时打开 pan.c 并对其进行编辑。

我是否必须使用另一个编译器？我正在使用 MinGW。

我创建了多个进程，这些进程又产生了其他进程。因此，SPIN 模型不断打印“进程过多（最多 255）”。但是，它仍然给了我最终的输出。如果它不能处理超过 255 个进程，它如何仍然设法给我最终输出？

我有以下类型定义。Pub 类型保留两个整数，而 pub_table 保留一个发布者数组和一个整数。

然后在网上pt.table[pt.last] = p;我收到一个错误说

“错误：不完整的结构参考‘表’看到‘操作员：=’”

不幸的是，我看不出那条线上有什么问题？

我正在使用 ispin 并收到错误说明 spin: trails end after 10 steps and transition failed.

如何防止此错误发生？

有什么方法可以指定消息的大小吗？例如，如果我想通过通道 AB 发送消息数据，那么如何在 PROMELA 语言中指定数据的大小？

我正在使用 SPIN 模型检查器 GUI - iSPIN。GUI 带有一个不错的自动机视图生成器，但是为了看到完整的自动机，我需要放大/缩小。如果可能的话，我还想将该自动机保存在一个漂亮的图像中（避免使用打印屏幕）。有没有办法从 SPIN 或其他可以基于 Promela 模型生成自动机的工具中保存生成的自动机图像？

PS 下面是一张图片，显示了我想保存的生成的 Automaton 图像。显然，我无法仅通过打印屏幕重新创建它。

我已经用 Promela 建模语言准备了一个 ABP 模型。但是我需要一些帮助来用另一种建模语言 - mCRL 重写它。我没有任何经验。有人可以告诉我一个开始的方法，或者给我指出 mCRL 的好教程吗？无论如何， mCRL 和 mCRL2 之间的代码有区别吗？

我在 promela 中的代码：