Событие B, формальное моделирование: как повлиять на все элементы набора в отношении

Question

У меня довольно много проблем с Event-B..

Я хотел бы установить связь между группой клиентов и номером клиента каждый

У меня есть отношение этого типа:

cli(PERSON) = NAT1 (Персона - это конечное множество)

и в случае, если у меня есть подмножество человека

where group <: PERSON

и я хотел бы коснуться отношения с клиентом, что я бы написал интуитивно:

! x . x : group | cli(x) = numcli

Я моделирую это правильно? Есть какой-нибудь способ получить аффект, который я хотел бы получить?

Answer 1

Я немного догадываюсь, чего вы хотите достичь: cli сопоставляет человека с номером:

VARIABLES
  cli
INVARIANTS
  cli : PERSON +-> NAT1

Вы хотите событие (давайте назовем это ev), который присваивает группе лиц (называется group) тот же номер:

ev = ANY
  group, numcli
WHERE
  group <: PERSON
  numcli : NAT1
THEN
  cli := cli <+ (group**{numcli})
END

group ** {numcli} является набором пар (отношение), где первый элемент является элементом group а второй numcli, Оператор <+ (реляционное переопределение) удаляет все элементы из cli где первый элемент, если один из его правого операнда и добавляет правый операнд. Т.е. отображения group в cli заменены или добавлены в отображение numcli,