UPPAAL中的Set实现

Question

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

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

Answer 1

除非最近添加了一套数据结构(如过去10年左右的数据结构)，否则语言中就没有这样的东西。

我会将选择建模为一个进程，其中有一个位置，每个边都设置一个共享变量(选择)到与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