问题标签 [spin]

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

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

我查看了 SPIN 模型检查器。但是，它没有动态分配的功能。是否有任何其他模型检查器可用于动态分配？

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

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

我目前正在学习 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;我收到一个错误说

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

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

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

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

我想知道如何编写代表 proctype 的所有实例的 never 声明。例如，如果我有以下命题：

现在，如果我实例化 5 个实例，camera_node我如何创建一个原子命题检查start_publishing所有这 5 个实例是否等于零？

我想在 windows7-64 上使用 SPIN 模型检查器，并且我已经安装了它的所有先决条件。以下是我如何做到的程序

1. 我用 cygwin 安装了 gcc 编译器 .. 用命令提示符检查了更新的路径，它显示版本 4.9.2
2. 安装 Active Tcl .. 更新路径 .. 当我打开 ispin 时工作正常。
3. 更新了 ispin 目录的路径。
4. 只是一点技巧，还可以通过在 ispin 文件中给出 gcc.exe 的确切路径来检查。但是错误仍然相同。

但是当我尝试编译预先包含的示例文件（例如leader.pml）时，它给了我错误

有人可以告诉我我做错了什么和/或错过了什么吗？我该如何解决这个问题？

谢谢。

我正在尝试习惯 iSpin/Promela。我在用：

Spin 版本 6.4.3——2014 年 12 月 16 日，iSpin 版本 1.1.4——2014 年 11 月 27 日，TclTk 版本 8.6/8.6，Windows 8.1。

这是我尝试使用 LTL 的示例。如果 for 循环中的两个步骤不是原子的，则 LTL 属性的验证会产生错误：

在验证点击中，我只想测试 LTL 属性，所以我禁用所有安全属性并激活“使用声明”。声明名称为“alwaysten”。

但是，如果我激活“断言违规”，似乎只是评估了 LTL 属性。为什么？一位同事正在使用 iSpin v1.1.0，他不需要激活它？我究竟做错了什么？我想独立地证明断言和 LTL 属性......

这是跟踪：