I get this error message when trying to use a Python library in Promela and spin (error message screenshot):
spin: /usr/include/unistd.h:778, Error: inline text too long near '/usr/include/unistd.h'
My Promela code is
c_code{
#include "demo1.c" /* the c code written above */
}
bool badstate = false;
active proctype driver()
{
do
:: (1) ->
c_code{
demo_fun();
}
if
:: c_expr{ x == 5 } ->
badstate = true;
:: else ->
skip;
fi;
od;
}
Here is my demo1.c
file, which I am including in my Promela code:
#include "python2.7/Python.h"
void demo_fun(void)
{
Py_Initialize();
PyRun_SimpleString("import sys; sys.path.insert(0, '/home/zeeshan/Documents/Promela')");
PyObject* pModule = NULL;
PyObject* pFunc = NULL;
pModule = PyImport_ImportModule("hello");
if (pModule == NULL) {
printf("Error importing module.");
exit(-1);
}
pFunc = PyObject_GetAttrString(pModule, "Hello");
PyEval_CallObject(pFunc, NULL);
Py_Finalize();
}
int main()
{
demo_fun();
return 0;
}
The Python code in hello.py
is:
def Hello():
a = 5
b = 2
print("hello world " + str(a + b))
From what I understand, Promela takes the code from all included files and inlines it. The size of this code becomes larger than spin's big number after the inline and causes it to crash.
Am I correct in thinking this? How can I fix my issue, and successfully call the Python code from my Promela specification?
An alternative solution, which is recommended by Spin
documentation, is to replace
c_code{
#include "demo1.c" /* the c code written above */
}
with
c_code{
\#include "demo1.c" /* the c code written above */
}
This prevents the c code from being inserted into the text of the model before it is passed to the Spin
parser.
From the docs:
The
Spin
parser will now simply copy theinclude
directive itself into the generatedC
code, without expanding it first.The backslash can only be used in this way inside
c_decl
andc_code
statements, and it is the recommended way to handle included files in these cases.
Sample output:
~$ spin t.pml
spin: warning: c_code fragments remain uninterpreted
in random simulations with spin; use ./pan -r instead
c_code2: {
demo_fun();
}
c_code3: x == 5
c_code2: {
demo_fun();
}
c_code3: x == 5
c_code2: {
demo_fun();
}
c_code3: x == 5
c_code2: {
demo_fun();
}
...