First, I'll summarize the project where I'm working so it's easier to understand the problem (I'm not use to write in English, sorry for the mistakes I could commit).
I've been working on a Promela model for path planning on natural terrain for a robot using LTL conditions. In summary, the model have to read the map information from an extern file (maps can be seen as a 2D matrix containing the height of each cell), and depending on the slope between adjacent cells, the robot could navegate through some path or not. Each cell of the map is associated with one state.
I've been testing the model with some tiny maps defined directly into the Promela model, and the path is correctly generated. To test bigger and more detailed maps (real natural terrain maps), I need to use embedded C code to preprocess the file, generating boolean values (1 for allowed movements and 0 for prohibited movements) so I could assign them to Promela variables and consider them into the LTL condition.
The problem appears when I try to add needed C libraries (like math.h) to my embedded code. I tried using c_code and c_decl functions.
(in Init proccess, to initialize the map where I'm working):
`...
c_code{
#include <math.h>
}`
When I use math.h library and try to verify my model (spin -a model_name.pml), I get this error:
spin: D:/Documentos/TDM-GCC/x86_64-w64-mingw32/include/vadefs.h:14, Error: malformed preprocessor directive - # .lineno near '#pragma'
I've also tried using \#include, as it appears in the documentation for Embedded C code in Promela, but it doesn't seems to work well, as I get errors during compilation of pan.c after verification because of the " \ " sign.
I tried to add the libraries I need after verification into the pan.c file manually and it works, but it doesn't looks like a good solution to me. Am I using at a bad way the #include expression? What I could do to fix the problem?
If you have any doubt about the explanation, please answer. I'll be very greatful for any comments.
Finally, I found the solution. I was trying to include C libraries inside the init process of the model. It's a wrong way to do this. The correct way is using the c_code instruction before init process:
... // 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
...
}
...
}
That was a clumsy mistake on my part. I hope that could be helpful for someone anytime.