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;
}