python - Promela/Spin中C随附的Python文件:“内联文本太长”

尝试在Promela中使用Python库并旋转（error message screenshot）时出现以下错误消息：

spin: /usr/include/unistd.h:778, Error: inline text too long near '/usr/include/unistd.h'

我的Promela代码是

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;
}

这是我的demo1.c文件，我将其包含在Promela代码中：

#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;
}

hello.py中的Python代码为：

def Hello():
    a = 5
    b = 2
    print("hello world " + str(a + b))

据我了解，Promela从所有包含的文件中获取代码并将其内联。内联之后，此代码的大小变得大于spin的大数字，并导致崩溃。

我认为正确吗？如何解决我的问题，并成功从Promela规范中调用Python代码？

最佳答案

Spin文档建议的替代解决方案是替换

c_code{
  #include "demo1.c" /* the c code written above */
}

与

c_code{
  \#include "demo1.c" /* the c code written above */
}

这样可以防止在将代码传递给Spin解析器之前将c代码插入模型的文本中。

从docs：


  现在，Spin解析器将简单地将include指令本身复制到生成的C代码中，而无需先对其进行扩展。
  
  反斜杠只能在c_decl和c_code语句中以这种方式使用，并且在这些情况下，建议使用反斜杠来处理包含的文件。




样本输出：

~$ 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();
        }
...