UPPAAL: проверка члена массива

Можно ли проверить, является ли объект элементом массива в UPPAAL?

Если у меня есть целочисленный массив

int ap[1,2];

Я хочу сделать запрос в верификаторе, где у меня есть что-то вроде:

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

Кроме того, есть ли в UPPAAL типы строк или символов?

Заранее спасибо!


model-checking uppaal
person tschens    schedule 30.03.2018    source источник
comment
В Uppaal нет текстовых строк.   -  person mariusm    schedule 30.03.2018
comment
окей, это грустно, но ладно :D   -  person tschens    schedule 30.03.2018

Ответы (1)


arrow_upward
1
arrow_downward

Вероятно, вы ищете выражение 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;
}
person mariusm    schedule 30.03.2018
comment
Я видел пользовательские функции, используемые только в части перехода update. Можно ли также использовать их в запросе? Если да, то можете описать как? :) Извините за много вопросов - person tschens; 30.03.2018
comment
Да, они могут, они должны быть без побочных эффектов, т.е. передавать по значению или константной ссылке. - person mariusm; 30.03.2018
comment
Я использовал ваш пример кода, чтобы иметь метод contains, но всегда получаю синтаксические ошибки при их использовании в запросе. Вот пример: E<> P0.a and contains({1},1) неожиданное '{', ожидание ')'... Я поместил метод contains в стандартный путь Project › Declarations. Что мне не хватает? Должен ли я использовать другой синтаксис для типа set_t? - person tschens; 08.04.2018
comment
Uppaal не принимает конструкции на месте. Обходной путь — создать const set_t one = {1,0,0,0,0,0,0,0,0,0}; а затем используйте один в запросе. - person mariusm; 08.04.2018