Установить реализацию в UPPAAL
У меня есть модель, в которой процесс должен выбрать элемент s
случайно из набора S
, Выбор части является одной операцией. Единственная похожая структура данных, которую я знаю в UPPAAL, это массивы.
Существует ли заданная структура данных в UPPAAL? Если нет, то как я могу его создать?
2 ответа
Если ваше множество S конечно и счетно, то попробуйте использовать ограниченный целочисленный тип. Например:
const int N = 10; // size of the whole domain
typedef int[1,N] range_t; // range of possible elements: indexed 1..N
typedef int[0,N-1] crange_t; // C-programmers may prefer indexed 0..N-1
bool S[range_t]; // boolean array encoding of membership
тогда вы можете сделать ребро, выбрав любой элемент из S, например:
select: e:range_t
guard: S[e]
sync: hey[e]!
update: chosen_one=e
Если только недавно не была добавлена заданная структура данных (как за последние 10 лет или около того), в языке нет такой вещи.
Я бы смоделировал выбор как процесс с одним местоположением и |S| ребра, каждый из которых устанавливает общую переменную (выбор) на значение, отличное от S. Для запуска выбора я бы использовал синхронизацию по срочному каналу.