Я пытаюсь создать допустимое выражение CTL или LTL для проверки модели в NuSMV. У меня есть переменная в игре, где актеры бегают, пытаясь поймать друг друга. Переменная: State_Of_Game: {Победа, Проигрыш, Игра} и я хочу сказать, что из каждого...

Я установил NuSMV с помощью предоставленного файла readme, однако, когда я пытаюсь использовать команду NuSMV, я получаю следующее сообщение: -bash: NuSMV: команда не найдена В интернете мало информации по этому поводу, буду признателен за любую...

Я изучаю проверку моделей и NuSMV для своего образования. Я могу редактировать и запускать код NuSMV, и у меня есть четкое представление о том, что такое UART и что он делает. Моя задача — формально смоделировать UART с помощью NuSMV, но пока я не...

Я новичок в NuSMV и CTL и пробовал простые примеры. У меня есть 3 состояния A, B и C и есть переход из A-> B Я смоделировал его в NuSMV и хочу проверить, есть ли какой-либо путь выполнения из B в A. Несмотря на то, что я не определил такой...

MODULE main VAR x : 0 .. 2; ASSIGN init (x) := 2; next (x) := case x = 2 : x = 10; esac; SPEC AG x = 2 -> AG X x = 20 at token "X": syntax error - Почему синтаксическая ошибка? Я пытаюсь...

Я пытаюсь использовать NuSMV для проверки своей модели, и вот код. Однако, когда я ввожу NuSMV kernel.smv в оболочку, возникает ошибка file kernel.smv: line 16: nested NEXT operators: next(_b) in definition of next(_cond) in definition...

Я хочу исключить возможный следующий случай при определенных условиях. Например, у меня есть: 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;...

У меня есть простая структура крипке, где у меня есть 3 состояния со следующими переходами: s1 --> s2 s2 --> s1 s1 --> s3 s3 --> s3 s1 — единственное начальное состояние. Я не хочу, чтобы цикл от s1 до s2 повторялся более...

Я начал изучать NuSMV в эти дни. У меня есть этот код: MODULE main VAR state: {a,b,c,d,e}; ASSIGN init(state) := a; next(state) := case (state = a) : b; (state = b) : c; (state = c) : d;...

Я хочу сформулировать эту проблему в NuSMv: Пользователь может находиться в одном из этих трех состояний: U-потребность, U-использование, U-грусть (представляющий собой пользователя, который нуждается в услуге, начинает пользоваться и он/она...

Я скачал бинарный файл NuSMV (64-разрядная версия MacOSX Darwin (x86)). После того, как я распаковал его, я отправился в папку bin в терминале. Я пробовал команду NuSMV -int, но получаю сообщение об ошибке: -bash: NuSMV: команда не найдена Я...

Я следую руководству по установке NuSMV в Windows 10. Он загружается нормально, но после извлечения файлов из заархивированной (.tar) папки я не нахожу файл .exe в папке «bin», которая должна быть там (конечно). Я загружаю его с веб-сайта NuSMV....