modeling - 在 UPPAAL 中设置实现

Question

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

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

Answer 1

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

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

Answer 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