uppaal - 有什么方法可以知道 uppaal 模型是否识别痕迹？

Question

我正在尝试检查 uppaal 模型是否识别出痕迹。

我必须生成随机跟踪并检查另一个类似模型是否可以执行相同的跟踪。我可以通过使用带有查询的verifyta.exe来进行随机生成：

"模拟 [<= n ; 1] {时钟} "

但是，我不知道 Uppaal 或 Tron 或某些扩展是否能够检查模型是否实际上可以达到与输入相同的轨迹。我将不胜感激任何建议，无论是改变我生成痕迹的方式还是我希望模型识别痕迹的方式。

任何帮助将不胜感激：D

Answer 1

首先，您需要定义跟踪的含义。模拟查询给出了一些表达式的轨迹——这很少需要，因为它包含非常精确的信息（在不同的系统中很难重现）。

Uppaal ECDAR 可以检查两个过程之间的模拟细化，并且跟踪是一个定时的动作序列。

Uppaal TRON 关注相对化的定时 i/o 一致性关系，也通过 i/o 操作的定时跟踪定义，除了跟踪是交互式组合的，其中输入由 TRON 生成，输出由被测实现。还可以声明所有可观察的动作都是输出，从而从 IUT 提供跟踪，TRON 将检查跟踪是否可以被模型接受。这就是所谓的监控模式，它可以由一个特殊的“跟踪适配器”执行，该适配器读取一个跟踪并代表 IUT 执行它。TRON 发行版包含一些由trace目录中的脚本驱动的示例，使用TraceAdapter. 适配器在命令行之后接受参数，--并且tron可以通过标准输入流提供跟踪。