我正在尝试检查uppaal模型是否识别跟踪。
我必须生成随机跟踪，并检查另一个类似的模型是否可以进行相同的跟踪。我可以使用verifyta.exe和查询进行随机生成：
">模拟[lt；=n；1]{时钟}"；
然而，我不知道Uppaal、Tron或某个扩展是否能够检查模型是否真的可以到达与输入相同的跟踪。我将感谢任何建议，无论是改变我生成痕迹的方式，还是我希望模型识别痕迹的方式。
任何帮助都将不胜感激：D
首先，您需要定义跟踪的含义。模拟查询给出了一些表达式的轨迹——这是很少需要的，因为它包含非常精确的信息(在不同的系统中很难再现)。
Uppaal ECDAR可以检查两个过程之间的模拟细化，跟踪是一个定时的动作序列。
Uppaal TRON涉及相对化的定时i/o一致性关系，也通过i/o操作的定时跟踪来定义，但跟踪是交互式组成的，其中输入由TRON生成，输出由测试中的实现生成。还可以声明所有可观察的动作都是输出，从而从IUT提供跟踪，TRON将检查跟踪是否可以被模型接受。这就是所谓的监视模式，它可以由一个特殊的"监视器"来执行；跟踪适配器"；其读取跟踪并代表IUT执行该跟踪。TRON发行版包含一些由trace目录中使用TraceAdapter的脚本驱动的示例。适配器在--到tron命令行之后接受参数，并且可以通过标准输入流提供跟踪。