/**	
 *	Classe Bankcardsecpurse
 *	Creation le 29/01/2007
 *	Derniere modification le 29/01/2007 par <ThM>
 *	@author <ThM>
 *	@version <0.1>
 */
public class Bankcardkernel {
	/* --------- Constantes -------- */
	// custom PIN constants
	public static final int DEFAULT_BPC =         0x00000000;
	public static final short DEFAULT_HPC =       0x0000;
	public static final byte MAX_TRY =            3;
	public static final short MAX_BALANCE =       3000;


	/* --------- Attributs --------- */
	private /*@ spec_public */ byte terminal_;
	private /*@ spec_public */ byte mode_;
	private /*@ spec_public */ boolean isOpenSess_;
	private /*@ spec_public */ int bpc_;
	private /*@ spec_public */ byte bptry_;
	private /*@ spec_public */ boolean isBankAuth_;
	private /*@ spec_public */ short hpc_;
	private /*@ spec_public */ byte hptry_;
	private /*@ spec_public */ boolean isHoldAuth_;
	private /*@ spec_public */ short balance_;
	private /*@ spec_public */ boolean hpcSet_;
	private /*@ spec_public */ boolean bpcSet_;


	/*@ invariant  
	  @   mode_ == Mode.PERSO ==> ((bpcset_ == false || hpcset_ == false) && 
	  @                             isBankAuth_ == false &&
	  @                             isHoldAuth_ == false);
	  @
	  @ invariant 
	  @    mode_ == Mode.INVALID ==> (isHoldAuth_ == false &&  
	  @                               hptry_ == 0 &&
	  @                               bptry_ > 0 && 
	  @                               bpcset_ == true && hpcset_ == false);
	  @
	  @ invariant
	  @    mode_ == Mode.USE ==> (bptry_ > 0 && hptry_ > 0 &&
	  @                           bpcset_ == true && hpcset_ == true);
	  @
	  @ invariant 
	  @    terminal == Terminal.NONE <==> isOpenSess_ == false;
	  @
	  @ invariant 
	  @    isOpenSess_ == false ==> (isBankAuth == false && 
	  @                              isHoldAuth == false);
	  @ 
	  @ invariant 
	  @    bpcset_ == true ==> bptry_ > 0;
	  @
	  @ invariant
	  @    hpcset_ == true ==> hptry_ > 0;
	  @    
	  @*/



	/* --------- Methodes ---------- */
	/**	
	 *	Constructeur
	 *    @param  files  noms des fichiers d'entree [et nom a utiliser pour le fichier de sortie]
	 */	
	/*@ assignable mode_, isOpenSess_, balance_, bpc_, bptry_, isBankAuth_, hpc_, hptry_, isHoldAuth_, balance_, terminal_, hpcSet_, bpcSet_;
	  @ ensures mode_ == Mode.PERSO &&
 	  @         isOpenSess_ == false &&
	  @         balance_ == 0 &&
	  @         bpc_ == DEFAULT_BPC &&
	  @         bptry_ == MAX_TRY &&
	  @         isBankAuth_ == false &&
	  @         hpc_ == DEFAULT_HPC &&
	  @         hptry_ == MAX_TRY &&
	  @         isHoldAuth_ == false &&
	  @         balance_ == 0 &&
	  @         terminal_ == Terminal.NONE && 
	  @         hpcSet_ == false &&
	  @         bpcSet_ == false;
	  @*/ 	  
	public Bankcardkernel(){
		mode_ = Mode.PERSO;
		isOpenSess_ = false;
		balance_ = 0x00000000;
		bpc_ = DEFAULT_BPC;
		bptry_ = MAX_TRY;
		isBankAuth_ = false;
		hpc_ = DEFAULT_HPC;
		hptry_ = MAX_TRY;
		isHoldAuth_ = false;
		balance_ = 0;
		terminal_ = Terminal.NONE;
		hpcSet_ = false;
		bpcSet_ = false;
	}


	/**
	 *  setTerminal command
	 *  @param  t  terminal to set
	 */
	//@ assignable terminal_;
	private void setTerminal(byte t){
		terminal_ = t;
	}


	/**
	 *  beginSession command
	 *  @return value of the mode
	 */
	/*@ normal_behavior
	  @    requires t == Terminal.ADMIN || 
	  @             t == Terminal.BANK || 
	  @             t == Terminal.PDA;    
	  @    requires isOpenSess_ == false;
	  @    assignable isOpenSess_, terminal_;
 	  @    ensures isOpenSess_ == true &&  terminal_ == t;	
	  @ also
	  @  exceptional_behavior 
	  @     requires isOpenSess_ == true;
 	  @     assignable isOpenSess_;
	  @     signals (RfException) \old(isOpenSess_) == isOpenSess_;
	  @ also
	  @  exceptional_behavior
	  @     requires t != Terminal.ADMIN && 
 	  @              t != Terminal.BANK && 
	  @              t != Terminal.PDA;
	  @     assignable isOpenSess_; 
	  @     signals (RsException) isOpenSess_ == \old(isOpenSess_);
	  @*/
	public void beginSession(byte t) throws RsException, RfException{
    	  

		// test si on a la condition de la PS, sinon lève une RsException
		if (!(
			  (t == Terminal.ADMIN) ||
			  (t == Terminal.BANK) ||
			  (t == Terminal.PDA)
			  )
			)
			throw new RsException("terminal = "+Terminal.type(t));
	  
		// test si on a la condition du MF, sinon lève une RfException
		if (!(isOpenSess_ == false))
			throw new RfException("isOpenSess = TRUE");
	  
		isOpenSess_ = true;
		setTerminal(t);
	}
	
	/**
	 *  endSession command
	 */
	/*@ normal_behavior
	  @    requires terminal_ == Terminal.ADMIN || 
	  @             terminal_ == Terminal.BANK || 
	  @             terminal_ == Terminal.PDA;    
	  @    requires isOpenSess_ == true;
	  @    assignable isOpenSess_, isBankAuth_, isHoldAuth_, terminal_;
	  @    ensures isOpenSess_ == false;
	  @    ensures isBankAuth_ == false;
	  @    ensures isHoldAuth_ == false;
	  @    ensures terminal_ == Terminal.NONE;
	  @ also 
	  @  exceptional_behavior
	  @     requires isOpenSess_ == false;
	  @     assignable isOpenSess_, isBankAuth_, isHoldAuth_;
	  @     signals (RfException) \old(isOpenSess_) == isOpenSess_ &&
	  @                           \old(isBankAuth_) == isBankAuth_ &&
	  @                           \old(isHoldAuth_) == isHoldAuth_;
	  @ also 
	  @  exceptional_behavior
	  @     requires terminal_ != Terminal.ADMIN && 
	  @              terminal_ != Terminal.BANK && 
	  @              terminal_ != Terminal.PDA;
	  @     assignable isOpenSess_, isHoldAuth_, isBankAuth_; 
	  @     signals (RsException) isOpenSess_ == \old(isOpenSess_) &&
	  @                           \old(isBankAuth_) == isBankAuth_ &&
	  @                           \old(isHoldAuth_) == isHoldAuth_;
	  @	  
	  @*/
	public void endSession() throws RsException, RfException{
		
		// test si on a la condition de la PS, sinon lève une RsException
		if (!(
			  (terminal_ == Terminal.ADMIN) ||
			  (terminal_ == Terminal.BANK) ||
			  (terminal_ == Terminal.PDA)
			  )
			)
			throw new RsException("terminal = "+Terminal.type(terminal_));
		
		
		// test si on a la condition du MF, sinon lève une RfException
		if (!(isOpenSess_ == true))
			throw new RfException("isOpenSess = FALSE");
		
		isOpenSess_ = false;
		isBankAuth_ = false;
		isHoldAuth_ = false;
		terminal_ = Terminal.NONE;
	}
	
	/**
	 *  setBpc command
	 *  @param  pin  value of the pin code to set to bpc
	 */
	/*@ normal_behavior
	  @     requires isOpenSess_ == true &&
	  @              mode_ == Mode.PERSO &&
	  @              terminal_ == Terminal.ADMIN;
	  @     assignable bpc_, bptry_, bpcSet_, mode_;
	  @     ensures bpc_ == pin && 
	  @             bptry_ == MAX_TRY &&
	  @             bpcSet_ == true && 
	  @             (\old(hpcSet_) == true ==> mode_ == Mode.USE) && 
	  @             (\old(hpcSet_) != true ==> mode_ == \old(mode_));
	  @ also 
	  @  exceptional_behavior
	  @     requires isOpenSess_ == false;
	  @     assignable bpc_, bptry_, bpcSet_, mode_;
	  @     signals (RfException) \old(bpc_) == bpc_ && 
	  @                           \old(bptry_) == bptry_ && 
	  @                           \old(bpcSet_) == bpcSet_ && 
	  @                           \old(mode_) == mode_;
	  @ also 
	  @  exceptional_behavior 
	  @     requires terminal_ != Terminal.ADMIN || mode_ != Mode.PERSO;
	  @     assignable bpc_, bptry_, bpcSet_, mode_; 
	  @     signals (RsException) \old(bpc_) == bpc_ && 
	  @                           \old(bptry_) == bptry_ && 
	  @                           \old(bpcSet_) == bpcSet_ && 
	  @                           \old(mode_) == mode_;
	  @*/
	public void setBpc(int pin) throws RsException, RfException{
		
		// test si on a la condition de la PS, sinon lève une RsException
		if (mode_ != Mode.PERSO)
			throw new RsException("mode != PERSO");
		
		if (terminal_ != Terminal.ADMIN)
			throw new RsException("Terminal != ADMIN");
		
		// test si on a la condition du MF, sinon lève une RfException
		if (isOpenSess_ != true || pin < 0)
			throw new RfException("isOpenSess != TRUE");
		
		bpc_ = pin;
		bptry_ = MAX_TRY;
		bpcSet_ = true;
		if (hpcSet_) 
			mode_ = Mode.USE;
	}
	
	/**
	 *  setHpc command
	 *  @param  pin  value of the pin code to set to hpc
	 */
	/*@ normal_behavior
	  @     requires isOpenSess_ == true;
	  @     requires (mode_ == Mode.PERSO && terminal_ == Terminal.ADMIN) ||
	  @              (mode_ == Mode.INVALID && terminal_ == Terminal.BANK && isBankAuth_);
	  @     assignable hpc_, hptry_, hpcSet_, mode_;
	  @     ensures hpc_ == pin && 
	  @             hptry_ == MAX_TRY &&
	  @             hpcSet_ == true && 
	  @             (\old(bpcSet_) == true ==> mode_ == Mode.USE) && 
	  @             (\old(bpcSet_) == false ==> mode_ == \old(mode_));
	  @ also 
	  @   exceptional_behavior 
	  @     requires isOpenSess_ == false;
	  @     assignable  hpc_, hptry_, hpcSet_, mode_;
	  @     signals (RfException) \old(hpc_) == hpc_ && 
	  @                           \old(hptry_) == hptry_ && 
	  @                           \old(hpcSet_) == hpcSet_ && 
	  @                           \old(mode_) == mode_;
	  @ also 
	  @   exceptional_behavior
	  @     requires !(mode_ == Mode.PERSO && terminal_ == Terminal.ADMIN) &&
	  @              !(mode_ == Mode.INVALID && terminal_ == Terminal.BANK && isBankAuth_);
	  @     assignable hpc_, hptry_, hpcSet_, mode_; 
	  @     signals (RsException) \old(hpc_) == hpc_ && 
	  @                           \old(hptry_) == hptry_ && 
	  @                           \old(hpcSet_) == hpcSet_ && 
	  @                           \old(mode_) == mode_;
	  @*/
	public void setHpc(short pin) throws RsException, RfException{
		
		// test si on a la condition de la PS, sinon lève une RsException
		if (!(
			  (
			   (mode_ == Mode.PERSO) &&
			   (terminal_ == Terminal.ADMIN) 
			   )||
			  (
			   (mode_ == Mode.INVALID) &&
			   (terminal_ == Terminal.BANK) &&
			   (isBankAuth_ == true)
			   )
			  ) )
			throw new RsException("RsException");
		
		// test si on a la condition du MF, sinon lève une RfException
		if (isOpenSess_ != true || pin < 0)
			throw new RfException("isOpenSess != TRUE");
		
		hpc_ = pin;
		//hptry_ = MAX_TRY;   // bug potentiel
		hpcSet_ = true;
		isBankAuth_ = false;
		isHoldAuth_ = false;
		if (bpcSet_) {
			mode_ = Mode.USE;
			hptry_ = MAX_TRY;
		}
	}
	
	/**
	 *  authBank command
	 *  @param  pin  value of the pin code to check for bpc
	 */
	/*@ normal_behavior
	  @     requires isOpenSess_ == true;
	  @     requires (mode_ == Mode.INVALID);
	  @     requires terminal_ == Terminal.BANK;
	  @		requires bptry_ > 0;
	  @     requires pin == bpc_;
	  @     assignable bptry_, isBankAuth_;
	  @     ensures bptry_ == MAX_TRY && isBankAuth_ == true;
	  @ also
	  @     requires isOpenSess_ == true;
	  @     requires (mode_ == Mode.INVALID);
	  @     requires terminal_ == Terminal.BANK;
	  @		requires bptry_ > 0;
	  @     requires pin != bpc_;
	  @     assignable bptry_, isBankAuth_, isHoldAuth_, mode_, hpcSet_, bpcSet_;
	  @     ensures (bptry_ == \old(bptry_) - 1) &&
	  @             isBankAuth_ == false && 
	  @             (bptry_ == 0 ==> 
	  @                     (mode_ == Mode.PERSO && 
	  @                      hpcSet_ == false && 
	  @                      bpcSet_ == false));
	  @      ensures (bptry_ > 0 ==> 
	  @                     (mode_ == \old(mode_) && 
	  @                      isBankAuth_ == \old(isBankAuth_) && 
	  @                      isHoldAuth_ == \old(isHoldAuth_) && 
	  @                      hpcSet_ == \old(hpcSet_) && 
	  @                      bpcSet_ == \old(bpcSet_)));
	  @ also 
	  @  exceptional_behavior 
	  @     requires (mode_ != Mode.INVALID) || 
	  @              (terminal_ != Terminal.BANK);	  
	  @     assignable mode_;
	  @     signals (RsException) mode_ == \old(mode_);
	  @ also 
	  @  exceptional_behavior
	  @     requires (isOpenSess_ == false);
	  @     assignable mode_; 
	  @     signals (RsException) mode_ == \old(mode_);
	  @	  
	  @*/
	public void authBank(int pin) throws RsException, RfException{
			
		// test si on a la condition de la PS, sinon lève une RsException
		if (mode_ != Mode.INVALID)
			throw new RsException("mode = PERSO");
		
		if (terminal_ != Terminal.BANK)
			throw new RsException("Terminal != BANK");
		
		// test si on a la condition du MF, sinon lève une RfException
		if (isOpenSess_ != true)
			throw new RfException("isOpenSess != TRUE");
		
		
		if (bptry_ > 0){
			if (pin == bpc_) {
				isBankAuth_ = true;
				bptry_ = 3;
			}
			else{
				bptry_ --;
				if (bptry_ == 0){
					mode_ = Mode.PERSO;
					isBankAuth_ = false;
					isHoldAuth_ = false;
					hpcSet_ = false;
					bpcSet_ = false;
					//hptry_ = 3;
				}
			}
		}
	}
	
	/**
	 *  checkPin command
	 *  @param  pin  value of the pin code to check for hpc
	 */
	/*@ normal_behavior
	  @     requires isOpenSess_ == true;
	  @     requires mode_ == Mode.USE;
	  @     requires (terminal_ == Terminal.BANK);
	  @		requires hptry_ > 0;
	  @     requires pin ==  hpc_;
	  @     assignable hptry_, isHoldAuth_, mode_;
	  @     ensures hptry_ == MAX_TRY && isHoldAuth_ == true && mode_ == \old(mode_);
	  @ also
	  @     requires isOpenSess_ == true;
	  @     requires mode_ == Mode.USE;
	  @     requires (terminal_ == Terminal.BANK);
	  @		requires hptry_ > 0;
	  @     requires pin != hpc_;
	  @     assignable hptry_, isHoldAuth_, mode_;
	  @     ensures hptry_ == \old(hptry_ - 1) && isHoldAuth_ == false;
	  @     ensures ((hptry_ == 0) ==> (mode_ == Mode.INVALID)) && 
	  @             ((hptry_ > 0) ==> (mode_ == \old(mode_)));
	  @ also 
	  @  exceptional_behavior
	  @     requires (mode_ != Mode.USE) || 
	  @              (terminal_ != Terminal.BANK);	  
	  @     assignable hptry_, isHoldAuth_, mode_;
	  @     signals (RsException) hptry_ == \old(hptry_) && 
	  @                           isHoldAuth_ == \old(isHoldAuth_) &&
	  @                           mode_ == \old(mode_);
	  @ also 
	  @  exceptional_behavior
	  @     requires (isOpenSess_ == false);
	  @     assignable hptry_, isHoldAuth_, mode_;
	  @     signals (RsException) hptry_ == \old(hptry_) && 
	  @                           isHoldAuth_ == \old(isHoldAuth_) &&
	  @                           mode_ == \old(mode_);
	  @	  
	  @*/
	public void checkPin(short pin) throws RsException, RfException{
		
		// test si on a la condition de la PS, sinon lève une RsException
		if (mode_ != Mode.USE)
			throw new RsException("mode != USE");
		
		if (terminal_ != Terminal.BANK)
			throw new RsException("Terminal != BANK");
		
		// test si on a la condition du MF, sinon lève une RfException
		if (isOpenSess_ != true)
			throw new RfException("isOpenSess != TRUE");
		
		if (hptry_ > 0){
			if (pin == hpc_) {
				isHoldAuth_ = true;
				hptry_ = MAX_TRY;
			}
			else{
				hptry_ --;
				isHoldAuth_ = false;
				if (hptry_ == 0){
					mode_ = Mode.INVALID;
				}
			}
		}
	}



	/*@ normal_behavior
	  @    requires isOpenSess_ == true;
	  @    requires mode_ == Mode.USE &&
	  @             isHoldAuth_ == true &&
	  @             terminal_ == Terminal.BANK;
	  @    requires a >= 0 && 
	  @             (short)(balance_ + a) <= MAX_BALANCE;
	  @    assignable balance_;
	  @    ensures balance_ == \old(balance_) + a;
	  @ also 
	  @  exceptional_behavior
	  @    requires isOpenSess_ != true || 
	  @             a < 0 || 
	  @             (short)(balance_ + a) > MAX_BALANCE;
	  @    assignable balance_;
	  @    signals (RfException) \old(balance_) == balance_;
	  @ also 
	  @  exceptional_behavior 
	  @    requires mode_ != Mode.USE || isHoldAuth_ == false || terminal_ != Terminal.BANK;
	  @    assignable balance_;
	  @    signals (RsException) \old(balance_) == balance_;
	  @*/
	public void credit(short a) throws RsException, RfException {
		
		// test Rs
		if (mode_ != Mode.USE || isHoldAuth_ == false || terminal_ != Terminal.BANK) 
			throw new RsException("mode_ != Mode.USE || isHoldAuth_ == false || terminal_ != Terminal.BANK");
		
		// test Rf
		if (isOpenSess_ != true || a < 0 || (short)(balance_ + a) > MAX_BALANCE) {
			throw new RfException("isOpenSess_ != true || a > MAX_BALANCE || a < 0");
		}
		
		balance_ = (short) (balance_ + a);

	}


	/*@ normal_behavior
	  @    requires isOpenSess_ == true;
	  @    requires mode_ == Mode.USE &&
	  @             (terminal_ == Terminal.BANK || terminal_ == Terminal.PDA);
	  @    requires a >= 0 && a <= balance_ ;
	  @    assignable balance_;
	  @    ensures balance_ == \old(balance_) - a;
	  @ also 
	  @  exceptional_behavior 
	  @    requires isOpenSess_ != true || 
	  @             a < 0 || a > balance_;
	  @    assignable balance_;
	  @    signals (RfException) \old(balance_) == balance_;
	  @ also 
	  @  exceptional_behavior 
	  @    requires mode_ != Mode.USE ||  (terminal_ != Terminal.BANK && terminal_ != Terminal.PDA) ;
	  @    assignable balance_;
	  @    signals (RsException) \old(balance_) == balance_;
	  @*/	
	public void debit(short a) throws RsException, RfException {

		// test Rs
		if (mode_ != Mode.USE) {
			throw new RsException("mode != USE");
		}
		if (terminal_ != Terminal.BANK && terminal_ != Terminal.PDA) {
			throw new RsException("terminal != Terminal.BANK && terminal_ != Terminal.PDA");
		}

		// test Rf
		if (a < 0 || a > balance_ || isOpenSess_ != true) {
			throw new RfException("a < 0 || a > balance_ || isOpenSess_ != true");
		}

		balance_ -= a;
	}

	
	/*@ normal_behavior
	  @    requires isOpenSess_ == true;
	  @    requires mode_ == Mode.USE && 
	  @             (terminal_ == Terminal.BANK || terminal_ == Terminal.PDA);
	  @    assignable \nothing;
	  @    ensures \result == \old(balance_);
	  @ also 
	  @  exceptional_behavior 
	  @    requires isOpenSess_ != true;
	  @    assignable balance_;
	  @    signals (RfException) \old(balance_) == balance_;
	  @ also 
	  @  exceptional_behavior
	  @    requires mode_ != Mode.USE || 
	  @             (terminal_ != Terminal.BANK && 
	  @              terminal_ != Terminal.PDA) ;
	  @    assignable balance_;
	  @    signals (RsException) \old(balance_) == balance_;
	  @*/		
	public short getBalance() throws RsException, RfException {
		// test Rs
		if (mode_ != Mode.USE) {
			throw new RsException("mode != USE");
		}
		if (terminal_ != Terminal.BANK && terminal_ != Terminal.PDA) {
			throw new RsException("terminal_ != Terminal.BANK && terminal_ != Terminal.PDA");
		}

		// test Rf
		if (isOpenSess_ != true) {
			throw new RfException("isOpenSess != true");
		}

		return balance_;
	}


}



class Terminal {

	public final static byte NONE = 0;
	public final static byte ADMIN = 1;
	public final static byte BANK = 2;
	public final static byte PDA = 3;


	public static String type(byte t)
	{
		String ret = "NONE";
		switch (t) {
		case ADMIN: ret = "ADMIN"; break;
		case BANK: ret = "BANK"; break;
		case PDA: ret = "PDA"; 
		}
		return ret;
	}


}


class RfException extends Exception { 
	
	public RfException(String s) {
		super(s);
	}

}

class RsException extends Exception { 

	public RsException(String s) {
		super(s);
	}

}

class Mode {

	public final static byte PERSO = 0;
	public final static byte USE = 1;
	public final static byte INVALID = 2;

}