model-checking - UPPAAL：检查数组成员

Question

是否可以检查对象是否是 UPPAAL 中数组的元素？

如果我有一个整数数组

int ap[1,2];

我想在验证器中做一个查询，我有类似的东西：

E<> 1 \in Process.ap[1]

此外，UPPAAL 中是否有字符串类型或字符类型？

提前致谢！

Answer 1

您可能正在寻找exists表达。

这是一个例子：

const int size=5;
typedef int[0,size-1] range_t;
typedef int set_t[range_t];

bool contains(const set_t& s, int el)
{
  return exists(i:range_t) s[i]==el;
}