spin - Promela中的浮点计算

Question

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

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

Answer 1

在 Promela/SPIN 中，您可以嵌入任意 C 代码，包括指定应将哪些 C 内存视为详尽探索的状态空间的一部分。查看语言结构：c_code、c_decl、c_state和.c_trackc_expr

请注意，包含浮点数通常很麻烦；甚至一个，但肯定不止一个。您要么需要找到一种方法使浮点值不属于状态空间，在这种情况下它们是中间计算值，要么您需要离散化您的问题空间。这是一个重要的模型检查概念的具体示例 - 在精确但计算上不可能的模式和近乎无内容的高级模型之间找到适当的抽象级别。

鉴于此，在最初的 PROMELA/SPIN 设计中省略浮点数是一个非常有意识的设计决定。

注意：在您的情况下，也许您有一些输入参数和一个“命中目标”的输出参数。然后，所有浮点计算都是中间的，并且您的正确性声明会找到例如导致错过目标的参数组合。