Описание тега nusmv

Описание тега Вопросы с тегом
NuSMV - это программное обеспечение для проверки моделей, бесплатное для некоммерческих и академических целей. Он используется для проверки и подтверждения оборудования и программного обеспечения.
1 ответ

Построить формальную модель UART в NuSMV?

Я изучаю проверку моделей и NuSMV для моего образования. Я могу редактировать и запускать код NuSMV, и у меня есть четкое представление о том, что такое UART и что делает. Моя задача - формально смоделировать UART с NuSMV, но в настоящее время я не …
26 фев '17 в 15:27
1 ответ

Как я могу изменить псевдо-код на код NuSMV?

Мой профессор решил дать нам студент-математик код для преобразования в NuSMV, и я не могу найти помощь где-либо еще, и я читаю учебник, он всего 6 страниц и описывает только то, что делает определенное свойство. Модуль main является примером кода N…
27 май '16 в 18:59
2 ответа

Пакетный файл не выполняется полностью после выполнения другого.exe

Я пытаюсь создать командный файл, который должен иметь следующие команды: cd "c:\Program files\NuSMV\2.5.2\bin\" NuSMV -int short.smv go pick_state -r print_current_state -v simulate -r 3 show_traces -t show_traces -v Проблема, с которой я сталкиваю…
14 апр '11 в 21:53
1 ответ

Причина различий в количестве достижимых состояний

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

NuSMV на Mac - опция команды ввода -int не найдена

Я пытаюсь запустить NuSMV на Mac, и я могу запустить его нормально, но когда мне нужно использовать интерактивный режим, опция -int выдает ошибку - Параметр командной строки "–int" неизвестен. У кого-нибудь еще была эта проблема?
19 фев '19 в 15:35
0 ответов

Как решить проблему с ошибкой IVAR в NuSMV

Функциональный модуль в NuSMV не может использовать входные переменные в качестве параметров, Как решить эту проблему, не меняя IVAR на VAR. Например, следующий код: MODULE main IVAR p1 : boolean; p2 : boolean; VAR x : boolean; f1:Fun(p1,p2); INIT x…
02 дек '18 в 15:52
1 ответ

NuSMV: как исключить возможное следующее состояние

Я хочу исключить возможный следующий случай при определенных условиях. Например, у меня есть: token : array 1..2 of {0, 1, 2, 3, 4, 5, 6}; next(token[1]) := case x : {1, 2, 3, 4, 5, 6}; TRUE : 0; esac; next(token[2]) := case x : {1, 2, 3, 4, 5, 6}; …
12 окт '18 в 12:05
1 ответ

Использование NuSMV в качестве модели проверки в Java

Я пытаюсь использовать NuSMV в качестве проверки модели в Java. Однако я не могу найти соответствующую библиотеку JAR онлайн. Единственное, что я нашел, предоставлено здесь, для которого ссылка для скачивания больше не работает. Очевидно, библиотека…
30 май '16 в 18:14
1 ответ

Как использовать NuSMV, чтобы засвидетельствовать атаку "человек посередине" (протокол Нидхэма-Шредера)?

У меня есть следующий упрощенный протокол Нидхэма-Шредера с открытым ключом: A → B: {Na, A} Kb B → A: {Na, Nb} Ka A → B: {Nb} Kb где Na, Nb одноразовые A, B, а также Ka, Kb являются открытыми ключами A, B соответственно. Сообщения, зашифрованные отк…
08 дек '17 в 08:10
2 ответа

Как узнать всевозможные встречные примеры Nusmv

У меня есть модель в NuSMV и после проверки спецификации ltl NuSMV дает мне контрольный пример Можно ли найти все пути, которые содержат контрольный пример, не один из них?
30 янв '18 в 11:04
0 ответов

Исследование государственного пространства в источнике NuSMV

Я работаю над программой коррекции / синтеза проекта. Моя задача - получить трассировку ошибок (контрпример), найти ее в полном пространстве состояний и восстановить модель в этом месте. Я хочу реализовать это как расширение NuSMV. Я отлаживал NuSMV…
11 дек '17 в 06:22
1 ответ

Проверьте алгоритм взаимного исключения Деккера по NuSMV

Я использую 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) := false; init(b2) := false; i…
09 май '16 в 18:04
1 ответ

Понимание рекурсивно определенной ошибки в NuSMV

У меня есть кусок кода в NuSMV, который вызвал ошибку. Код: - MODULE main VAR x1: {a,b,c,d,e}; x2: {a,b,c,d,e}; ASSIGN next(x1) := case x1=a & x2=c: e; x1=d & next(x2)=c : a; TRUE : x1; esac; next(x2) := case x1=b & x2=b: c; x2=d & n…
31 авг '18 в 22:47
1 ответ

Проверка модели с помощью NuSMV

Правда ли, что в NuSMV нет таких значений, как NULL, nil, None? И что мы не должны делать модель для процесса, потому что модели должны отражать электронные схемы? Мой сценарий состоит в том, что у меня есть один разъем UART, основная память и проце…
08 апр '17 в 10:55
1 ответ

Модель NuSMV - AND

Я пытаюсь написать следующую модель в NuSMV Другими словами, z становится плохим только тогда, когда x и y также находятся в плохом состоянии. Это код, который я написал MODULE singleton VAR state: {good, bad}; INIT state = good TRANS (state = good)…
25 сен '17 в 16:00
0 ответов

Как найти память и время выполнения, используемые моделью NuSMV

Учитывая модель NuSMV, как найти ее время выполнения и сколько памяти она потребляет? Таким образом, время выполнения можно найти с помощью этой команды в системном приглашении: /usr/bin/time -f "time %e s" NuSMV filename.smv Вышесказанное дает врем…
30 ноя '18 в 22:08
1 ответ

Присвоить случайное значение переменным в NuSMV

У меня есть следующий код в NuSMV. MODULE main VAR x : 0..5 Таким образом, x является переменной, которая может принимать целочисленные значения 0,1,2,3,4,5. Затем я инициализирую его и устанавливаю правила перехода. ASSIGN init(x):=1; next(x) := ca…
21 авг '18 в 22:55
0 ответов

NuSMV:: Неправильные контрпримеры для свойства

Я хочу смоделировать симметричный распределенный четырехпроцессорный трехцветный протокол с помощью nuSMV. Моя спецификация, в которой я уверен в ее правильности, должна быть истинной, но когда я использую ключевое слово "F" для свойства "Наконец", …
04 фев '17 в 18:27
0 ответов

Прочитать файл в NuSMV

Я хочу реализовать систему перехода в NuSMV, которая указана в файле.txt, который я хочу, чтобы инструмент прочитал, а затем создал TS из него. Формат файла: 6 1 2 2 3 3 4 4 5 5 6 Это конкретный пример, где 6 - это общее количество вершин / узлов, з…
23 окт '18 в 06:01
1 ответ

Удовлетворяющий формуле LTL в модели

Является AG(~q ∨ Fp) LTL формула удовлетворяет в модели ниже? Почему или почему нет? модель?
11 июн '16 в 17:16