Как выполнить файл .smv из блокнота++

В настоящее время я изучаю NuSMV для проверки моделей LTL и CTL.

Я использую notepad++ для своей деятельности по кодированию — в основном на python — и я знаю, что мы можем запустить скрипт python (файлы .py) с помощью notepad++.

Я новичок в NuSMV, и мне интересно, есть ли способ выполнить скрипт .smv в notepad++.

Вот пример кода .smv, который я собираюсь запустить.

MODULE main
 VAR
  variable : boolean;
 ASSIGN
  init(variable) := true;
  next(variable) := !variable;
 LTLSPEC
  G (variable & X !variable)
 CTLSPEC
  EF (!variable & AX variable)

Однако у меня также есть некоторые трудности с запуском вышеуказанного сценария SMV с использованием интерактивной оболочки NuSMV. Предположим, имя приведенного выше сценария — test.smv. Как мне запустить его с помощью интерактивной оболочки NuSMV?


notepad++ nusmv
person Iqazra    schedule 04.04.2014    source источник
comment
Вы пробовали плагин NppExec?   -  person user694733    schedule 04.04.2014
comment
Согласно руководству NppExec, SMV не поддерживается. Я ожидаю что-то вроде run C:\Program Files\NuSMV\2.5.4\bin\NuSMV.exe -i ($(FULL_CURRENT_PATH). Это работает для python, но проблема возникает для SMV. Подсказка NuSMV › отсутствует. .   -  person Iqazra    schedule 04.04.2014

Ответы (1)


arrow_upward
1
arrow_downward

Если вы можете понять командную строку для запуска вашего кода, то решение таково:

  1. Установить плагин NPPExec
  2. Выясните командную строку, которую вы хотите выполнить, и протестируйте ее.
  3. В N++ нажмите F6 или используйте эквивалентный пункт меню из меню плагина NPPExec.
  4. Заполните необходимую командную строку
  5. Замените имя файла в вашей командной строке на токен "$(FULL_CURRENT_PATH)" - N++ поместит здесь имя файла вашего текущего файла
  6. [необязательно] Нажмите кнопку Сохранить... и сохраните команду.
  7. Нажмите кнопку OK, чтобы выполнить команду.
  8. Для повторного запуска одной и той же команды просто нажмите Ctrl+F6

Чтобы отобразить вывод команды на консоль, нажмите Ctrl+` (клавиша слева от 1234567890).

NuSMV поддерживает запуск из командной строки и имеет множество параметров командной строки, описанных в главе 4 документации (текущая версия на сегодняшний день). Однако, если они по-прежнему не соответствуют вашим требованиям и нет возможности запустить ваш код из командной строки, вам может потребоваться рассмотреть собственное программное решение (если у вас достаточно времени и навыков) — рассмотрите возможность написания собственного плагина N++. Или напишите небольшой инструмент, управляемый из командной строки, который вызывает все необходимые методы NuSMV, используя свой API. Возможно, это также можно сделать в Python. Затем вы просто вызываете свой инструмент из NPPExec.

person miroxlav    schedule 04.04.2014