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