Python file included with C in Promela/Spin: 'inline text too long'

Question

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?

Answer 1

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 the include directive itself into the generated C code, without expanding it first.

The backslash can only be used in this way inside c_decl and c_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();
        }
...