uppaal - 晚餐无法核实

Question

为什么在我验证时会发生这种情况。当我验证 test1.P3 和 test.P6 的 sup 时，我得到 gtr < inf。这是什么意思，我该如何解决？我的模型如下：

在此处输入图像描述

在此处输入图像描述

标签： uppaal

Answer 1

The message means that the supremum is infinity, i.e. there is no upper bound for gtr. The reason for this is that the system can stay in the initial state indefinately, thus gtr may get arbitrary large valuation.