Event-B Rodin platform, Modelling Sub-Sets relation

Question

I'm a beginner on Event-B and I'm trying to model a machine where the set PERSONNE includes the set CLIENT which includes the set RESIDENT... I've searched on Rodin's documentation but I haven't found anything... Here is the context

context contexteHumain

sets PERSONNE CLIENT RESIDENT

axioms
  @axm1; finite(PERSONNE)
  @axm2; finite(CLIENT)
  @axm3; finite(RESIDENT) // Definition of three possible sets

and here is the machine

machine machineFunKeyHotel sees contexteHumain

variables
    pers
    reserv
    cli
    resid
    chkin
    chkout

invariants
    @inv1: pers ⊆ PERSONNE
    @inv2: cli ⊆ CLIENT
    @inv3: resid ⊆ RESIDENT
// Définis les 3 variables d'ensemble de Personnes, Clients et Résidents
    @inv4: reserv ∈ BOOL
    @inv5: chkin ∈ BOOL
    @inv6: chkout ∈ BOOL
// Les paramètres booléens si la ⦂personne a réservé, check-in ou check-out.
    @inv7: CLIENT ⊆ PERSONNE
    @inv8: RESIDENT ⊆ CLIENT
// Et les relations entre les différnets ensembles d'humains·

events
  event INITIALISATION
  begin
    @act1: reserv ≔ FALSE
    @act2: chkin ≔ FALSE
    @act3: chkout ≔ FALSE
// Ces valeurs sont à faux, en effet, au début personne n'a ni réservé ni check-in
// Encore moins check out.
    @act4: resid ≔ ∅
    @act5: cli ≔ ∅
// Au début le nombre de client et de résidents sont zéro
    @act6: pers ≔ ∅ //???
// Définir un nombre de personne presqu'infini (Personnes sur terre estimé à
// 7 290 477 807 personnes le vendredi 3 avril 2015 à 9 h 07 min et 24 s (GTM +1)
  end

  event réserver
// Lorsqu'une personne quelconque a réservé ça implique quelle soit ajoutée
// à l'ensemble clients.
    any potentiel_client
    where
      @gr1: potentiel_client ∈ PERSONNE
      @gr2: reserv = TRUE
    then
      @act1: cli ≔ cli ∪ {potentiel_client}
  end

  event checkerin
// Lorsqu'un client a passé l'étape de check-in, cela implique qu'il est ajouté
// à l'ensemble résident
    any futur_resident
    where
      @gr1: futur_resident ∈ CLIENT
      @gr2: chkin = TRUE
    then
      @act1: resid ≔ resid ∪ {futur_resident}
  end

  event checkerout
// Lorsqu'un résident a procédé au check out cela implique qu'il est retiré
// et de l'ensemble client et de l'ensemble résident.
    any resident_actuel
    where
      @gr1: resident_actuel ∈ RESIDENT
      @gr2: chkout = TRUE
    then
      @act1: resid ≔ resid ∖ {resident_actuel}
      @act2: cli ≔ cli ∖ {resident_actuel}
  end
end

I think I've got the idea but I cannot manage how to solve the various errors I get: Types CLIENT and PERSONNE do not match (3 times) Types RESIDENT and CLIENT do not match (2 times)...

Answer 1

There is a problem in your specification that is very common for beginners in Event-B. :)

You have introduced three deferred sets PERSONNE, CLIENT and RESIDENT. But I think a client or a resident are persons, too. And all deferred sets are constants, so with this construction, you're not able to modify your set of clients or residents.

I think the basic problem is the keyword SETS. You do not have to specify all sets of your machine there. Think TYPES! You just introduce a new type (I think you need only PERSONNE here) and have a constant for all elements.

context contexteHumain
sets PERSONNE

So remove the sets CLIENT and RESIDENT. I would suggest to remove all axioms, too. Do you really have to assume that the set of possible persons is finite?

Adapt your invariants:

invariants
  @inv1: pers ⊆ PERSONNE
  @inv2: cli ⊆ pers
  @inv3: resid ⊆ cli

Remove inv7 and inv8. You probably want to add an invariant that the set of persons in your system is finite (in contrast to all possible persons in PERSONNE):

@inv9: finite(pers)

Accordingly, you would adapt your guards:

@gr1: futur_resident ∈ cli

resp.

@gr1: resident_actuel ∈ res