Promela/Spin : 'inline text too long' 中包含 C 的 Python 文件

Question

尝试在 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 从所有包含的文件中获取代码并将其内联。这段代码的大小在内联后变得比自旋的大数还大，导致它崩溃。

我这样想对吗？如何解决我的问题，并从我的 Promela 规范中成功调用 Python 代码？

Answer 1

Spin 文档推荐的替代解决方案是替换

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

与

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

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

来自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.

---

示例输出:

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