/* AnnuaireBis
 * Author: e174584q
 * Creation date: 16/01/19
 */
MACHINE
    AnnuaireBis

SETS
    PERSONNES;
    NUMEROS

VARIABLES
    annuaire,
    personnes

INVARIANT
    personnes : FIN(PERSONNES)
  & annuaire : personnes <-> NUMEROS // une personne peut avoir deux numéros

INITIALISATION
    personnes := {}
 || annuaire := {}

OPERATIONS
    ajoutMembre(pers) = //ajout d'un personne dans le club
    PRE
        pers : PERSONNES
      & pers /: personnes
    THEN
        personnes := personnes \/ {pers}
    END;

    ajoutNumMembre(pers, num) = //ajout d'un num à un membre du club
    PRE
        pers : personnes
      & num : NUMEROS
      & pers |-> num /: annuaire
    THEN
        annuaire := annuaire \/ {pers|->num}
    END;

    rr<--consultNum(pers) =  //retourne le num d'une personne
    PRE
        pers : personnes
      & pers: dom(annuaire) //la personnes a un numero
    THEN
        rr := annuaire[{pers}]
    END;

    rr<--consultNom(num) = //retourne la ou les personnes
    PRE
        num : NUMEROS
    THEN
        rr :=  num |-> annuaire~[{num}] //antécédent
    END;

    supprMembreAnnuaire(pers,num) =  //supprimer un membre de l'annuaire
    PRE
        pers : personnes
      & pers : dom(annuaire)
      & pers |-> num : annuaire
    THEN
        annuaire := annuaire - {pers |-> num}
    END;

    modifNum(pers,num, nouveau)= //modifier le numéro d'une personne
    PRE
        pers : personnes
        & num : NUMEROS
        & nouveau : NUMEROS
        & pers |-> num : annuaire
        & pers |-> nouveau /: annuaire
    THEN
        annuaire := (annuaire - {pers|->num}) \/ {pers|->nouveau}
    END

END