[SOLVED] Event-B, formal modelling : How to affect all the elements of a set to a relation

Event-B, formal modelling : How to affect all the elements of a set to a relation

I'm having quite a lot of troubles with Event-B..

I'd like to make a relation from a group of client to a client number each

I have a relation of that type :

cli(PERSON) = NAT1 (Person is a finite set)

and in an event I have a subset of person

where group <: PERSON

and I'd like to affect to the cli relation what I'd write intuitively :

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

Am I modelling it the right way? Is there any method to get the affectation I'd like to get?

Solution

I'm a little bit guessing what you want to achieve: cli maps a person to a number:

VARIABLES
  cli
INVARIANTS
  cli : PERSON +-> NAT1

You want an event (let's call it ev) that assigns to a group of persons (called group) the same number:

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

group ** {numcli} is a set of pairs (a relation) where the first element is an element of group and the second is numcli. The operator <+ (relational override) removes all elements from cli where the first element if one of its right operand and adds the right operand. I.e. mappings of group in cli are replaced or added to a mapping to numcli.