Я хотел бы настроить защиту края следующим образом: (turn % 4) == me где turn — переменная часов, а me — целое число, представляющее процесс. Пожалуйста, дайте мне пример того, как сделать защиту для вышеуказанного предиката. Спасибо,...

Дополнение от этот вопрос ... У меня есть полностью связанный граф, и это здорово. Я также добавил понятие времени. Сейчас я борюсь с концепцией передачи данных по моему графику. Я моделирую систему, задача которой состоит в том, чтобы каждый...

Я хотел бы распечатать все состояния при проверке моей модели. Мы получаем файл следа, когда происходит нарушение утверждения, но я хочу видеть состояния, даже если нарушения утверждения отсутствуют. Как я могу это сделать?

Я использую графический интерфейс для проверки моделей SPIN — iSPIN. Графический интерфейс поставляется с хорошим генератором представления автоматов, однако, чтобы увидеть полный автомат, мне нужно увеличивать/уменьшать масштаб. Также я хотел бы...

Я пытаюсь создать реализацию системы светофора в NuSMV. Прямо сейчас у меня есть 6 логических значений для NS/EW красный, желтый, зеленый. Однако, когда я указываю, что каждое из них всегда истинно в будущем состоянии, оно возвращается ложным. Если...

Мой профессор решил дать нам, студенту-математику, код для изменения в NuSMV, и я не могу найти больше нигде помощи, и я прочитал учебник, всего около 6 страниц, и только описываю, что делает определенное свойство. Модуль main является примером кода...

Я пытаюсь использовать NuSMV в качестве средства проверки модели в java. Однако я не могу найти соответствующую библиотеку JAR в Интернете. Единственное, что я нашел, находится на здесь для которого ссылка на скачивание больше не работает....

В чем разница между символическим выполнением и проверкой модели (например, при преобразовании модели)? Я не понимаю их разницы. Они одинаковы?!

В средствах проверки моделей, таких как CBMC (средство проверки ограниченной модели для C), определяемый пользователем оператор утверждения принимает логическое условие, а средство проверки модели проверяет, является ли условие истинным или ложным для...

Я новичок в SPIN и Promela, и я столкнулся с этой ошибкой, когда пытался проверить свойство живости в своих моделях. Код ошибки: unreached in proctype P (0 of 29 states) unreached in proctype monitor mutex_assert.pml:39, state...

Я пишу два модуля в NuSMV, но получаю сообщение об ошибке «Условия случая не являются исчерпывающими». Эта ошибка указывает на последний оператор случая, который у меня есть в коде. Я не уверен, как это исправить, потому что те случаи, которые у меня...

Я написал следующую модель алгоритма Петерсона: bool want[2], turn ltl { []<>P[0]@cs } active [2] proctype P() { pid me = _pid pid you = 1 - me do :: want[me] = true turn = you !want[you] || turn == me cs:...

Допустим, у нас есть этот фрагмент кода: int x = 3; int y = 5; int z = 0; active proctype P(){ if :: x > y -> z = x :: else -> z = y fi } active proctype Q(){ x++ } active proctype R(){ y = y - x } Я не...

У меня есть модель в muXmv, где я инициализирую диапазон значений, например - VAR x : 0..100; ASSIGN init(x) := 10..50; это отлично работает. Однако, когда я использую переменную вместо значений, ASSIGN init(x) := LB..UB;...