Я настроил модель с помощью UPPAAL и использовал верификатор для проверки взаимоблокировки. Ответ: Имущество не устраивает. Таким образом, существует тупик.
Есть ли способ в UPPAAL сообщить более подробную информацию о взаимоблокировке, такую как состояние и текущие значения всех переменных в конкретной ситуации?
да. мы можем отследить тупик в UPPAAL, т. е. мы можем найти состояния или путь, который вызывает тупик. Перейдите к опции --> диагностическая трассировка --> самая быстрая. вы можете выбрать любой из этих вариантов: какой-то/самый быстрый/кратчайший в диагностической трассировке. После выбора самого быстрого. Перейдите к верификатору и проверьте свойство блокировки взаимоблокировки. Сохраните новую трассировку в моделировании, выбрав «да» после этого перейдите в симулятор, он покажет вам новую трассировку хранилища, которая делает свойство неудовлетворительным. Надеюсь, это будет полезно
