c - 尝试将 C 库包含到 Promela 模型中

Question

首先，我将总结我正在工作的项目，以便更容易理解问题(我不习惯用英语写作，对于我可能犯的错误感到抱歉)。
我一直在研究 Promela 模型，用于使用 LTL 条件为机器人在自然地形上进行路径规划。总之，模型必须从外部文件中读取 map 信息( map 可以看作包含每个单元格高度的 2D 矩阵)，并且根据相邻单元格之间的斜率，机器人可以导航或不通过某些路径. map 的每个单元格都与一个状态相关联。
我一直在使用一些直接定义到 Promela 模型中的小 map 来测试模型，并且正确生成了路径。为了测试更大更详细的 map (真实的自然地形图)，我需要使用嵌入式 C 代码来预处理文件，生成 bool 值(1 表示允许的运动，0 表示禁止的运动)，以便我可以将它们分配给 Promela 变量并考虑他们进入零担条件。
当我尝试将所需的 C 库(如 math.h )添加到我的嵌入式代码时，问题就会出现。我尝试使用 c_code和 c_decl职能。
(在初始化过程中，初始化我正在工作的 map ):

`...
 c_code{
 #include <math.h>
 }`

当我使用 math.h 库并尝试验证我的模型 (spin -a model_name.pml) 时，出现此错误:

spin: D:/Documentos/TDM-GCC/x86_64-w64-mingw32/include/vadefs.h:14, Error: malformed preprocessor directive - # .lineno near '#pragma'

我也试过使用 \#include ，如 Embedded C code in Promela 的文档中所示，但它似乎效果不佳，因为我在验证后编译 pan.c 时遇到错误，因为“ \”符号。
我尝试将验证后需要的库手动添加到 pan.c 文件中，并且可以正常工作，但对我来说似乎不是一个好的解决方案。我是否以错误的方式使用#include 表达式？我能做些什么来解决这个问题？
如果您对解释有任何疑问，请回答。如有任何意见，我将不胜感激。

Answer 1

最后，我找到了解决方案。我试图在模型的 init 进程中包含 C 库。这样做是错误的方法。正确的方法是在init进程前使用c_code指令:

... // After other proctypes created

c_code{
  \#include <math.h>
}

/* INIT PROCESS */
init{

 // Variables needed in the model:
 int dataPromela;

 // Embedded C code needed:
 c_code{ //C variables declaration, math operations, etc
   ...
 }
...

}

那是我的一个笨拙的错误。我希望这可以随时对某人有所帮助。