Установить реализацию в 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. Для запуска выбора я бы использовал синхронизацию по срочному каналу.

Другие вопросы по тегам