MACHINE

    e_purse_kernel

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};
    OKKO = {OK,KO}
    

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

    rs, rf <-- beginSession(su) = 
        PRE
            su : SUBJECT
	THEN
	    IF 
		(su = terminalAdministratif or 
		 su = terminalBancaire or
		 su = pda) 
            THEN
		rs := OK ||
	    	IF 	
		    su /= none & terminal = none
		THEN 
	 	    rf := OK || terminal := su
	        ELSE 
		    rf := KO
		END
	    ELSE 
		rs := KO ||
		IF 
		    su /= none & terminal = none
		THEN 
		    rf := OK
	        ELSE
		    rf := KO
		END
	    END
        END;
    
    
    rs, rf <-- authBank(pin) = 
        PRE
            pin : BPC
	THEN 
	    IF 
		terminal = terminalBancaire & mode = invalid
	    THEN 
		rs := OK ||
		IF 
		    pin /= -1 & (mode = invalid & terminal /= none)
	        THEN
		    rf := OK ||
        	    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
		ELSE
		    rf := KO
		END
	    ELSE 
		rs := KO ||
		IF 
		    mode = invalid & terminal /= none
 	        THEN 
		    rf := OK
		ELSE
		    rf := KO
		END
	    END
        END;
    

    rs, rf <-- checkPin(pin) = 
        PRE
	    pin : HPC
	THEN 
	    IF 
		mode = use & terminal = terminalBancaire
	    THEN 
		rs := OK ||
		IF 
		    pin /= -1 & mode = use & terminal /= none 
		THEN 
		    rf := OK ||
		    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
		ELSE
		    rf := KO
		END
	    ELSE
		rs := KO ||
		IF 
		    mode = use & terminal /= none
		THEN 
		    rf := OK
		ELSE
		    rf := KO
		END
	    END
	END;



    rs, rf <-- setBpc(pin) = 
        PRE
	    pin : BPC
	THEN 
	    IF 
		(mode = perso & terminal = terminalAdministratif)
	    THEN
		rs := OK ||
		IF 
		   pin /= -1 & mode = perso & terminal /= none 
	        THEN
		    rf := OK ||
	            bpc := pin ||
	            bptry := MAXTRIES ||
	            isBankAuth := FALSE ||
	            IF  
			hpc /= -1
	            THEN 
			mode := use	
	            END
		ELSE
		    rf := KO
		END
	    ELSE
		rs := KO ||
		IF 
		    pin /= -1 & mode = perso & terminal /= none
	        THEN 
		    rf := OK 
		ELSE
		    rf := KO
		END
	    END
        END;


    rs, rf <-- setHpc(pin) = 
        PRE	
            pin : HPC
	THEN 
	    IF 
		(terminal = terminalBancaire & mode = invalid & isBankAuth = TRUE) or
		(terminal = terminalAdministratif & mode = perso)
	    THEN 
		rs := OK ||
		IF 
		    (pin /= -1 &        
	            (mode = perso or 
	                 (mode = invalid & isBankAuth = TRUE)) &
	            terminal /= none) 
	        THEN
		    rf := OK ||
	            hpc:= pin ||
        	    isHoldAuth := FALSE ||
		    isBankAuth:= FALSE ||
		    hptry := MAXTRIES ||
	            IF  
		        bpc /= -1
	            THEN  
		 	mode := use
	            END
		ELSE
		    rf := KO
		END
	    ELSE
		rs := KO ||
		IF 
		    (pin /= -1 &        
	            (mode = perso or 
	                 (mode = invalid & isBankAuth = TRUE)) &
	            terminal /= none) 
		THEN 
		    rf := OK 
		ELSE
		    rf := KO
		END
	    END	    
       END;
    
    
    rs, rf <-- endSession = 
        IF 
	    (terminal = terminalBancaire or
	     terminal = terminalAdministratif or
	     terminal = pda)
	THEN 
	    rs := OK ||
	    IF 
		terminal /= none
	    THEN
		rf := OK ||
	        isBankAuth := FALSE ||
	        isHoldAuth := FALSE ||
	  	terminal := none
	    ELSE
	        rf := KO
	    END
	ELSE
	    rs := KO ||
	    IF 
		terminal /= none
	    THEN 
		rf := OK
	    ELSE
		rf := KO
	    END
        END;


    rs, rf, amount <-- getBalance = 
	IF 
	    mode = use & 
	    (terminal = terminalBancaire or terminal = pda)
	THEN 
	    rs := OK ||
	    IF			
                mode = use & 
	        terminal /= none
	    THEN
	        rf := OK ||
                amount := balance
	    ELSE
		rf := KO
	    END
	ELSE
	    rs := KO ||
	    IF 
		mode = use & 
		terminal /= none
	    THEN 
		rf := OK
	    ELSE
		rf := KO
	    END
        END;


    rs, rf <-- debit(amount) = 
        PRE
            amount : 0..MAXBAL 
	THEN 
	    IF 
		mode = use & 
		(terminal = terminalBancaire or
		 terminal = pda)
	    THEN 
		rs := OK ||
		IF 
	            mode = use &
	            terminal /= none & 
	            balance - amount >= 0
		THEN
		    rf := OK ||	
        	    balance := balance - amount		
		ELSE
 		    rf := KO
		END 
	    ELSE 
		rs := KO ||
		IF 
	            mode = use &
	            terminal /= none & 
	            balance - amount >= 0
		THEN
		    rf := OK
		ELSE
 		    rf := KO
		END 
	    END
        END;


    rs, rf <-- credit(amount) = 
        PRE
            amount : 0..MAXBAL
	THEN 		
	    IF 
		mode = use & 
		terminal = terminalBancaire &
		isHoldAuth = TRUE
	    THEN 
		rs := OK ||
		IF
	            mode = use & 
		    terminal /= none &
	            isHoldAuth = TRUE &
	            balance + amount <= MAXBAL
		THEN 
		    rf := OK ||
	            balance := balance + amount
		ELSE
		    rf := KO
		END
	    ELSE
		rs := KO ||
		IF
	            mode = use & 
		    terminal /= none &
	            isHoldAuth = TRUE &
	            balance + amount <= MAXBAL
		THEN 
		    rf := OK 
		ELSE
		    rf := KO
		END
	    END
        END

END