Файл Python, включенный в C в Promela/Spin: «слишком длинный встроенный текст»

Я получаю это сообщение об ошибке при попытке использовать библиотеку Python в Promela и вращаться (скриншот сообщения об ошибке):

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

Мой код Промела

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

Код Python в hello.py:

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

Насколько я понимаю, Promela берет код из всех включенных файлов и встраивает его. Размер этого кода становится больше, чем большое число спина после встроенного кода, что приводит к сбою.

Правильно ли я думаю об этом? Как исправить мою проблему и успешно вызвать код Python из моей спецификации Promela?


python c promela spin
person Tania Saleem    schedule 02.01.2019    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Альтернативное решение, рекомендованное Spin документацией, заключается в замене

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

с

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

Это предотвращает вставку кода c в текст модели до того, как он будет передан синтаксическому анализатору Spin.

Из документов:

Синтаксический анализатор 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();
        }
...
person Patrick Trentin    schedule 02.01.2019

arrow_upward
1
arrow_downward

Согласно веб-сайту spinroot:

Максимальная длина строки — 64 КБ (65536 символов).

а также

ограничение на встроенное определение

"python2.7/Python.h" и некоторые из его собственных включений имеют размер более 64 КБ, поэтому вы получаете эту ошибку. Вы не можете просто включить всю библиотеку Python в свою спецификацию Promela (по крайней мере, со спином, как это реализовано в настоящее время).

Поскольку код C в любом случае должен быть связан с библиотеками Python, вы можете предоставить extern определений или даже собственный заголовочный файл для элементов, которые нужны вашему коду C для вызова вашего кода Python.

Итак, в вашем случае в minimal_python.h (я предполагаю, что возвращаемые типы void не используются):

#ifndef MINIMAL_PYTHON_H
#define MINIMAL_PYTHON_H

void Py_Initialize(void); 
void Py_Finalize(void);

void PyRun_SimpleString(const char *);

PyObject * PyImport_ImportModule(const char *);

void PyEval_CallObject(PyObject *, void *); 
PyObject * PyObject_GetAttrString(PyObject *, const char *); 

#endif

И тогда demo1.c включает minimal_python.h вместо python2.7/Python.h.

В случае с вашим кодом вам также потребуется определение для printf и любой другой стандартной библиотеки или функций Python, так как они превышают ограничение в 64 КБ.

person Billy Brown    schedule 02.01.2019
comment
Проголосовал за, так как вы меня опередили, и это работает, но есть и альтернативное решение;) - person Patrick Trentin; 02.01.2019
comment
@PatrickTrentin Альтернативное решение, но ваше решение правильное. - person Billy Brown; 02.01.2019