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

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

0 голосов
/ 02 января 2019

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

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

Код Python в hello.py: 

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

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

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

Ответы [ 2 ]

0 голосов
/ 02 января 2019

Альтернативное решение, которое рекомендуется 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();
        }
...
0 голосов
/ 02 января 2019

По данным сайта spinroot :

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

и

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

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

Поскольку в любом случае код 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 КБ.

...