UPPAAL：检查数组成员答案

【问题标题】：UPPAAL: Checking member of arrayUPPAAL：检查数组成员
【发布时间】：2018-03-30 20:35:28
【问题描述】：

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

如果我有一个整数数组

int ap[1,2];

我想在验证器中进行查询，我有类似的东西：

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

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

提前致谢！

【问题讨论】：

Uppaal 中没有文本字符串。
ok，这很可悲，但没关系：D

标签： model-checking uppaal

【解决方案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;
}

【讨论】：

我看到了自定义用户函数只在过渡的 update 部分中使用。是否也可以在查询中使用它们？如果是，你能描述一下如何吗？ :) 很抱歉有很多问题
是的，它们必须是无副作用的，例如按值或常量引用传递。
我使用您的示例代码来创建 contains 方法，但在 Query 中使用它们时总是出现语法错误。这是一个示例：E<> P0.a and contains({1},1) unexpected '{', expecting ')' ... 我将 contains 方法放在标准 Project > Declarations 路径中。我错过了什么？我必须对 set_t 类型使用其他语法吗？
Uppaal 不接受就地结构。一种解决方法是创建“const set_t one = {1,0,0,0,0,0,0,0,0,0}；”然后在查询中使用“one”。