uppaal - 无限延迟但没有正率

Question

我创建了这个 UPPAAL 规范：https ://pastebin.com/v4AkYUuy

但是在运行查询时：

simulate 100 [<=500] { time }

我得到错误：

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

我已经搜索了几个小时，但 UPPAAL 没有很好的文档。

人 汽车 火车

标签： uppaal

Answer 1

只需将指数速率添加到该位置即可。当没有延迟上限时，Uppaal 尝试使用指数分布，但它不知道速率，因此会出现错误消息。另请参阅 Uppaal SMC 教程。