UPPAAL：检查数组成员

Question

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

如果我有一个整数数组

int ap[1,2];

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

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

另外，UPPAAL中有String类型或者字符类型吗？

提前致谢！

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

UPPAAL：检查数组成员

UPPAAL: Checking member of array

model-checking

uppaal