问题标签 [uppaal]

问问题

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

73 问题

0 投票

2 回答

5068 浏览

random - Uppaal中的随机数

在 Uppaal 程序中定义全局声明时，如何创建随机数？

我想要一个包含随机数的变量，就像在 C 程序中一样：

0 投票

1 回答

929 浏览

model-checking - UPPAAL：是什么导致时钟停止运行

我目前正在运行我的 UPPAAL 模拟器。我的模拟器在某个时间点后停止运行代码。这一点取决于我提供的声明。但我想知道时钟什么时候停止运行？有什么东西会触发这个吗？

model-checking uppaal

0 投票

2 回答

416 浏览

modeling - 在 UPPAAL 中设置实现

我有一个模型，其中一个进程需要s从集合中随机选择一个元素S。选择部分是一个单一的操作。我在 UPPAAL 中知道的唯一类似的数据结构是数组。

UPPAAL 中是否存在集合数据结构？如果没有，那么我该如何创建一个？

modeling verification promela uppaal

0 投票

0 回答

268 浏览

oop - uppaal 上的领导人选举过程

我的拓扑中有这样的连接：

https://courses.cs.ttu.ee/w/images/e/e5/ITI0130_Lab3_IEEE1394.pdf

我写了这样一个声明来在 uppaal 上运行模拟：

该数组指定节点与索引的连接。例如，节点“0”没有与任何节点连接，因此它在所有索引中都为 0。但是节点“1”与节点“2、4、5”相连。所以它在那个索引中有 1。

现在，当我运行模拟时，我得到了两个领导者。

当我运行模拟时，我必须将节点“0”连接到拓扑以获得一个领导者。

我尝试将节点“0”连接到某些节点，但没有成功。

这是我的模型：

在此处输入图像描述

我怎样才能做到这一点？

oop leader uppaal

0 投票

1 回答

2425 浏览

random - 在 Uppaal 中生成随机数

我的问题是我可以在 Uppaal 中生成一个随机数吗？

我想从一系列值中生成一个数字。更重要的是，我想生成的不仅仅是整数，我还想生成双精度值。

例如：双 [7.25,18.3]

我发现这个问题在谈论同样的问题。我尝试过这个。但是，我收到此错误：语法错误意外 T_SELECT。

它不起作用。我是 Uppaal 世界的新手，如果您能提供任何帮助，我将不胜感激。

问候，

random numbers uppaal

0 投票

0 回答

534 浏览

deadlock - UPPAAL：违反了不变量，但没有明确设置 - 如何解决死锁？

我想了解更多关于定时自动机来验证实时系统的信息。目前，我正在尝试熟悉一个名为 UPPAAL 的工具。

我画了一些简单的图表并添加了不同的属性。整个模型应该代表一个生产单元系统，其中不同的机械单元相互传递一个块。

我已经模拟了块（BlockCycle）、2 个机械单元（Feeder、FeederBelt）和 2 个感应块到达的传感器。

尽管我认为我的系统会有意义，但它还是陷入了僵局：

这个转换的目标状态违反了不变量。这不是问题，只要您希望您的模型表现得像这样。

（不，我没有。;P）

不过，我似乎无法找到导致僵局的原因。该工具将我指向BlockCycle模型，但我没有在那里指定任何不变量。事实上，所有的转换要求都已满足，因此绝对应该进行转换（从Pos7到Pos8 ）。

下面您将看到系统如何演变并最终陷入困境（弹出错误消息）。

标签：

绿色：属性检查（例如FB_Running表示FB_Running == true）
深蓝色：属性更新/分配
深红色：位置（例如Pos7或Pos8）

具有相关转换的BlockCycle模型：

我的问题：为什么系统会死锁，即使仍然有可以采取的交易。

Edit1：当我删除 Sensor7 的位置Active（称为BlockAtPos[7]）的不变属性时，死锁就解决了。所以我猜，由于Sensor7和BlockCycle在死锁之前的最后一个转换之间没有同步，这会导致矛盾（BlockAtPos[7]在传感器还没有机会进行InActive转换时变为假），因此违反不变量。

注意：您可以在此处找到我的 UPPAAL 代码/文件：pcs.xml。

deadlock modeling verification invariants uppaal

0 投票

1 回答

729 浏览