uppaal - Uppaal时钟是如何演变的？我有两个位置 1 和 2 没有不变量。什么是时钟值？

TLDR；回答。 如果自动机从没有不变量的位置开始x==0并移动，那么自动机可能会延迟，比如5时间单位，然后移动到另一个位置x==5，然后再次延迟，比如3.141时间单位，移动x到值8.141，等等。请注意，时钟x可以通过延迟和进行转换来获得任意实际值（因此我是任意选择），这意味着需要分析所有这些可能性。Uppaal 以约束的形式捕获所有这些可能的值（或者在没有不变量或守卫的情况下缺少它们，模拟器可能会显示只是x==y因为所有时钟都是同步的）。

一些上下文。 Uppaal 使用时钟变量实现定时自动机，其值以 . 的速率（时间导数）连续变化1。因此，如果时钟重置为0并且自动机到达没有不变量的位置（也不是紧急的，也不是提交的），那么时钟可以自由演化，因此可以具有从0到的任意值infinity。Uppaal使用打包到差分绑定矩阵(DBM)中的约束（区间）象征性地表示此类估值。如果自动机进行转换，则 Uppaal 将立即分析满足约束的所有可能转换。例如，如果一个位置有一个不变量，而边有一个守卫，那么转换是可用的x<=5x>=2x2在和之间的任意位置5，因此 Uppaal 将采用带约束的符号转换，2<=x && x<=5该转换一次捕获所有可能的转换。这允许在有限的数据结构和有限的时间内分析无限多的转换。

一些常见的情况可能会让新手感到困惑。 如果系统中有多个自动机，则全局分析时间的流逝，即一个自动机中的不变量将对其他自动机中的其他时钟产生影响，因为所有时钟通过全局时间同步。

定时自动机在守卫和不变量中只允许整数，原则上可以缩放以适应具有有理数的模型。Uppaal 还通过紧急、已提交的位置、选择语句、广播同步、整数变量、函数调用等扩展了定时自动机，这些在相同的定时自动机理论下仍然可以分析，但使建模更具表现力和简洁。

您可以在http://uppaal.org的文档部分下的 Uppaal 教程中阅读更多内容： http ://www.it.uu.se/research/group/darts/uppaal/documentation.shtml#tutorials

uppaal - Uppaal时钟是如何演变的？我有两个位置 1 和 2 没有不变量。什么是时钟值？

问题描述

解决方案

推荐阅读