问题标签 [uppaal]

我有一个有 5 个进程的系统。其中一个进程发送信号1！到3个进程（即3个进程接收信号1？）。但是当我只模拟 3 个接收进程中的一个接收到 signal1 时。如何让所有 3 个同时接收到这个信号 1？

我正在尝试使用 UPPAAL SMC 查询更大的系统，结果显示“内存已耗尽”错误消息。从本质上讲，UPPAAL SMC 不应该导致状态空间爆炸，这就是为什么我问是否可以在不发生状态空间爆炸的情况下使用 SMC 进行查询。

如果我尝试在很多状态下执行以下操作：

我收到以下错误消息：

是否可以在不调用内存密集型的情况下查询 Uppaal SMC engine.getSystem()？

这是我的“设备”模板的 uppaal 模型

Uppaal时钟是如何演变的？我有两个没有不变量的位置 1 和 2，在转换到位置 1 时时钟重置为零 (0)。在位置 1 和 2 之间的边缘，我如何知道此时时钟的值？（即位置 2 之前两个位置之间的时钟值）。时钟是否继续从位置 1 演变到位置 2 及以后，或者在新位置的入口处发生自动重置？

我有三个自动机（见下文），单个全局声明urgent chan u;和系统声明system UrgentChannel, P1, P2;。我的理解是，通过建立u一个紧急通道，必须start进行从到的过渡。goal

我想了解为什么物业P1.start --> P1.goal不满意。模拟器中的反例在这里似乎没有帮助。

下载模型在这里。谢谢阅读！

• P1：
• P2：
• 紧急频道：

我希望这里有人可以给我你的建议或知识。

我已经在 Uppaal 和 Spin 中阅读了有关火车门的示例。我还尝试使用 Uppaal 来验证我的计划，结果非常好。然而。我想稍微扩展我的计划。因此，我尝试使用 Spin 来验证一些与时间无关的属性。

我的问题是：我是否可以理解，如果我删除相对时间（时钟），Uppaal 可以处理相同的旋转。如果没有，你能给我一个例子或财产来证明吗？

任何信息或建议对我都有帮助。非常感谢您的阅读。

我正在尝试使用类似 CSP 的同步机制，但我不明白为什么以下模型的初始状态是死锁：

在我看来，这两个进程在通道“a”上是同步的，应该至少迈出一步，不是吗？

根据 http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf 没有通过通道传递的值，但这很容易由共享变量编码：全局定义一个变量 x，并使用它用于阅读和写作。"

Uppaal 附带的 Train-Gate 示例似乎通过通道执行值的通信。我还创建了一个小示例，其中生产者在从 1 到 6 的循环中计数并comm[getN()]!在通道通信上进行通信（getN()只需检索局部变量）。消费者与此通信同步comm[n]?并将传递的整数值存储在局部变量中。

这似乎与上述说法相矛盾。我在这里错过了一些微妙的东西吗？这不是通过渠道传递价值吗？还是这个说法不再正确？

我通过 Pastebin 包含了我的完整示例（producer-consumer.xml）：https ://pastebin.com/ZTL46Wr8

谢谢

我有以下结构：

我初始化这个数组如下：

但是对于第一个元素，会出现以下错误：

无效的初始化程序

对于第二个元素：

初始化程序中的元素太多

我应该提到我使用的 Uppaal 版本是4.1.19. 那么问题来了，问题出在哪里？

如何在 Uppaal 中将一些数据作为日志或一些统计信息写入文件？是否有任何fprintf功能或一些FILE*我们有C或没有的功能？从文件中读取同样的问题。

我想了解 [1] 中讨论的 UPPAAL SMC 示例。

这是 UPPAAL-SMC 示例：

三个定时自动机应该可视化 UPPAAL SMC 中的概率分布。在论文中指出，三个 TA 的 END 位置可以在时间间隔 [6,12]、[4,12] 和 [0,+∞) 内到达。我在 UPPAAL 中对 A1 TA 进行了建模，并且由于更新 X=0 并且边缘中的防护 x >= 2，因此不可能到达 END 位置。如何详细计算时间间隔？

[1] http://people.cs.aau.dk/~kgl/SSFT2015/SMC%20tutorial.pdf