uppaal - Uppaal 模拟错误：状态定义不明确

Question

我是uppaal的新手。我有一个由不同模型组成的系统。我还声明了一个时钟和一个双变量。

对于我的不变量和守卫，我需要检查这两个值（时钟 t；双 y；不变量：t<=y 或守卫 t==y 或 ty）。

现在在模拟的时候，我有这个错误

这个州的继任者没有很好的定义。SymbolicState:clock: Model.t -> double

我不知道我做错了什么。