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

Я скачал исходный код NuSMV для Mac и начал установку с помощью README. Тем не менее, есть шаг, который просит меня выполнить сборку с использованием «cmake..», когда я запускаю эту проблему. Исходный каталог не содержит CMakeLists.txt. Любая...

Я использую NuSMV для проверки алгоритма Деккера, и мой код выглядит следующим образом: MODULE main VAR b1 : {true, false}; b2 : {true, false}; k : {1, 2}; pr1 : process proc(k, b1, b2, 1); pr2 : process proc(k, b2, b1, 2); ASSIGN init(b1) :=...

Я не знаю, как объявить глобальные константы в NuSMV таким же образом, как #define n 5 in C . Как я могу сделать это в NuSMV?

Я проверяю 8-битный сумматор с помощью этого кода. Когда я печатаю, число доступных состояний равно 1, если основной модуль пуст, и 2^32, если включен весь основной модуль. Что делает эту разницу в сообщаемом количестве достижимых состояний? Для...

Я не могу установить NuSMV-2.6.0-win64 в ОС Windows 10. Я успешно загрузил это, но не могу установить из папки «bin», которая была извлечена.

Я пытаюсь запустить «случайное» или недетерминированное моделирование модели NuSMV, которую я создал. Однако между последующими запусками трассировка, которая создается, точно такая же. Вот модель: MODULE main VAR x : 0..4; VAR clk : 0..10;...

Мне нужно установить NuSMV на свой Mac, и я точно не знаю, как его установить. На веб-сайте NuSMV доступны два файла: исходный код и двоичный код. Какой из них я должен установить? И после выбора, что я должен делать, например, я должен следовать...

Я пытаюсь создать реализацию 4 в ряд в NuSMV. К сожалению, я новичок в NuSMV, и мне трудно его создать. Я попытался определить все случаи выигрыша для игрока 1 и использовал 2D-массив для представления сетки. Теперь я получаю сообщение об ошибке от...

Я написал следующий код: MODULE main VAR status:{empty, no_empty}; x : 0..3; ASSIGN init(status):= empty; init(x):=0; next(status):= case (status = empty): no_empty; (status = no_empty) & (x=0): empty;...