在 UPPAAL 中设置实现答案

【问题标题】：Set implementation in UPPAAL在 UPPAAL 中设置实现
【发布时间】：2014-05-20 05:43:37
【问题描述】：

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

UPPAAL 中是否存在 set 数据结构？如果没有，那我该如何创建呢？

【问题讨论】：

标签： modeling verification promela uppaal

【解决方案1】：

除非最近（如过去 10 年左右）最近添加了一个集合数据结构，否则该语言中没有这样的东西。

我会将选择建模为一个具有一个位置和 |S| 的过程。边缘，每个都将共享变量（选择）设置为与 S 不同的值。为了触发选择，我会在紧急通道上使用同步。

【讨论】：

【解决方案2】：

如果您的集合 S 是有限且可数的，请尝试使用有界整数类型。例如：

const int N = 10; // size of the whole domain
typedef int[1,N] range_t; // range of possible elements: indexed 1..N
typedef int[0,N-1] crange_t; // C-programmers may prefer indexed 0..N-1
bool S[range_t]; // boolean array encoding of membership

然后你可以像这样从 S 中选择任何元素来创建一条边：

select: e:range_t
guard: S[e]
sync:  hey[e]!
update: chosen_one=e

【讨论】：

如果成员是对称的，则通过声明对称范围类型来应用对称减少（产生指数加速）：typedef scalar[N] symrange_t。