Неограниченная задержка, но нет положительной скорости

Я создал эту спецификацию UPPAAL: https://pastebin.com/v4AkYUuy

Но при выполнении запроса:

simulate 100 [<=500] { time }

Я получаю сообщение об ошибке:

Location Person.Rijssen has unbounded delay but no positive rate.

Я искал часы, но у UPPAAL нет хорошей документации.

Лицо Автомобиль Поезд


person Mathay Kahraman    schedule 11.11.2018    source источник


Ответы (1)


Просто добавьте экспоненциальную скорость к этому местоположению. Uppaal пытается использовать экспоненциальное распределение, когда нет верхней границы задержки, но скорость неизвестна, поэтому появляется сообщение об ошибке. См. также учебник Uppaal SMC.

person mariusm    schedule 12.11.2018