MACHINE

    e_purse_func

DEFINITIONS

    TRYLEFT == 0..3 ; 
    BPC == -1..9999 ;    /* ensemble des codes PIN banque ; -1 code non initialise */
    HPC == -1..9999      /* ensemble des codes PIN porteurs ; -1 code non initialise */

CONSTANTS

    MAXBAL, MAXTRIES

PROPERTIES

    MAXBAL = 3000        /* solde maximal, en centimes */
	& 
    MAXTRIES = 3         /* nombre maximal d'essais pour les authentifications */

SETS

    SUBJECT = {pda, terminalBancaire, terminalAdministratif, none} ;
    MODE = {perso, invalid, use}
    

ABSTRACT_VARIABLES

    mode, hptry, bpc, hpc, bptry, isBankAuth, isHoldAuth, balance, terminal

INVARIANT

    balance : 0..MAXBAL &    /* solde du porte-monnaie */
    mode : MODE &            /* cycle de vie de la carte PERSO --> USE --> INVALID */
    hptry : 0..MAXTRIES &    /* nb essais verification code PIN porteur */
    bptry : 0..MAXTRIES &    /* nb essais verification code PIN banque  */
    isBankAuth : BOOL &      /* indicateur : la banque est-elle authentifiee ? */
    isHoldAuth : BOOL &      /* indicateur : le porteur est-il authentifié ? */
    bpc : BPC &              /* code PIN banque */
    hpc : HPC &              /* code PIN porteur */
    terminal : SUBJECT &     /* terminal ayant ouvert une session ; none = pas de session ouverte */
    /*? En mode perso, personne n'est authentifié et il reste un code à installer ?*/
    (mode = perso => ( bpc = -1 or hpc = -1 )) &
    (mode = perso => isBankAuth = FALSE) &
    (mode = perso => isHoldAuth = FALSE) &
    /*? En mode invalid, le hpc est bloqué et bpc n'est pas bloqué ?*/
    (mode = invalid => isHoldAuth = FALSE) &
    (mode = invalid => hptry = 0) &
    (mode = invalid => bptry > 0) &
    (mode = invalid => (bpc /= -1 & hpc = -1)) &
     /*? En mode use, ni bpc, ni hpc ne sont bloqués ?*/
    (mode = use => bptry > 0) &
    (mode = use => hptry > 0) &
    (mode = use => bpc /= -1 & hpc /= -1) &
    /*? Hors d'une session, personne n'est authentifié et on n'a pas de terminal ?*/
    (terminal = none => isBankAuth = FALSE) &
    (terminal = none => isHoldAuth = FALSE) &
    (bpc /= -1 => bptry > 0) &
    (hpc /= -1 => hptry > 0)


INITIALISATION
    
    hptry := MAXTRIES ||
    bptry := MAXTRIES ||
    isBankAuth := FALSE ||
    isHoldAuth := FALSE ||
    mode := perso ||
    hpc := -1 ||
    bpc := -1 ||
    balance := 0 ||
    terminal := none


OPERATIONS

    beginSession(su) = 
        PRE
            su : SUBJECT & su /= none & terminal = none
        THEN
 	    terminal := su
        END;
    
    
    authBank(pin) = 
        PRE
            pin : BPC
	    & pin /= -1
            & mode = invalid  
            & terminal /= none 
        THEN
            IF 
                pin = bpc
            THEN
                isBankAuth := TRUE ||
                bptry := MAXTRIES
            ELSE
                bptry := bptry - 1 ||
                isBankAuth := FALSE ||
                IF 
                    bptry -1  = 0
                THEN
                    mode := perso ||
                    hpc := -1 ||
                    bpc := -1
                END
            END
        END;
    

    checkPin(pin) = 
        PRE
	    pin : HPC & 
	    pin /= -1 &
	    mode = use &
            terminal /= none 
        THEN
	    IF 
		pin = hpc
            THEN
                isHoldAuth := TRUE ||
                hptry  := MAXTRIES
            ELSE
                 hptry := hptry - 1 ||
                 isHoldAuth := FALSE ||
                 IF
                     hptry - 1 = 0
                 THEN
                     mode := invalid ||
                     hpc := -1
                 END 
            END
	END;

    setBpc(pin) = 
        PRE
	    pin : BPC & pin /= -1 & 
            mode = perso & 
            terminal /= none 
        THEN
            bpc := pin ||
            bptry := MAXTRIES ||
            isBankAuth := FALSE ||
            IF  
		hpc /= -1
            THEN 
		mode := use
            END
        END;

    setHpc(pin) = 
        PRE
            pin : HPC & pin /= -1 &        
            (mode = perso or 
                 (mode = invalid & isBankAuth = TRUE)) &
            terminal /= none 
        THEN
            hpc:= pin ||
            isHoldAuth := FALSE ||
            isBankAuth:= FALSE ||
	    hptry := MAXTRIES ||
            IF  
	        bpc /= -1
            THEN  
	 	mode := use
            END
        END;
    
    
    endSession = 
        PRE
            terminal /= none
        THEN
            isBankAuth := FALSE ||
            isHoldAuth := FALSE ||
	    terminal := none
        END;


    amount <-- getBalance = 
        PRE
            mode = use & 
            terminal /= none
	THEN
            amount := balance
        END;


    debit(amount) = 
        PRE
            amount : 0..MAXBAL &
            mode = use &
            terminal /= none & 
            balance - amount >= 0
        THEN
            balance := balance - amount
        END;


    credit(amount) = 
        PRE
            amount : 0..MAXBAL &
            mode = use & 
	    terminal /= none &
            isHoldAuth = TRUE &
            balance + amount <= MAXBAL
        THEN
            balance := balance + amount
        END

END