uppaal - 价值通过渠道

Question

根据 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

谢谢

Answer 1

在您的模型中，没有价值传递。实际上，您使用同名通道的同步来模拟值传递：comm[n]！其中 n 实际上是一个变量和 comm[k]？其中 k 是一个选择器，即一个常数值。消费者实际上并没有收到 n 的值；它接收到 comm[n] 已针对某个固定的 n 值发出的信息。