Promela中的浮点计算

Question

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

解决这个问题的办法是什么？我们如何在Promela建立这样的系统模型？

Answer 1

在Promela/SPIN中，您可以嵌入任意的C代码，包括说明哪些C内存应该被视为被彻底探索的状态空间的一部分。查看语言结构：c_code、c_decl、c_state、c_track和c_expr。

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

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

注意:在您的例子中，您可能有一些输入参数和一个“命中目标”的输出参数。然后，所有浮点计算都是中间的，您的正确性声明发现，例如，导致错过目标的参数组合。