package crous;


/** Machine servant a payer un repas dans les points de restauration
 * Crous. 
 * @author M. Nebut
 * @version 11/06
 */
public class MachineCrous {
    private /*@ spec_public @*/ /*@ nullable @*/ CarteCrous carte;

    /** Constructeur */
    /*@ ensures this.carte == null;
      @*/
    public MachineCrous() {
	this.carte = null;
    }

    /** retourne vrai si la machine a une carte associee. */
    public /*@ pure @*/ boolean aCarte() {
	return this.carte != null;
    }

    /** Retourne la carte associee a la machine.
     *	@throws CarteNonPresente
     */
    /*@ signals_only CarteNonPresente;
      @
      @ signals (CarteNonPresente) ! aCarte();
      @
      @ ensures \result != null;
      @*/
    public /*@ pure @*/ CarteCrous getCarte() 
	throws CarteNonPresente
    {
	if ( this.carte == null )
	    throw new CarteNonPresente();

	return this.carte;
    }


    /** Positionne a la carte passee en parametre la carte associee a
     * cette machine. 
     * @param c la carte associee a la machine
     * @throws CarteDejaPresente
     */
    /*@ requires c != null;
      @
      @ signals_only CarteDejaPresente;
      @
      @ signals (CarteDejaPresente) aCarte();
      @ 
      @ assignable this.carte;
      @
      @ ensures this.carte == c;
      @*/
    public void setCarte(CarteCrous c) 
	throws CarteDejaPresente
    {
	if ( aCarte() )
	    throw new CarteDejaPresente();
	else
	    this.carte = c;
    }
    
    /** La machine n'a plus de carte associee.
     * @throws CarteNonPresente
     */
    /*@ assignable this.carte;
      @
      @ signals_only CarteNonPresente;
      @
      @ signals (CarteNonPresente) ! aCarte();
      @
      @ ensures this.carte == null;
      @*/
    public void unsetCarte() 
	throws CarteNonPresente
    {
	if ( ! aCarte() )
	    throw new CarteNonPresente();
	else
	    this.carte = null;
    }
    
    /** Retourne le prix d'un repas pour la categorie passee en
     * parametre.
     * @param c la categorie dont on veut le prix d'un repas
     * @throws CategorieInconnue s'il n'y a pas de categorie correspondante
     * @return le prix d'un repas pour la categorie <tt>c</tt>
     */
    /*@ requires c != null;
      @
      @ signals_only CategorieInconnue;
      @
      @ signals (CategorieInconnue) c != Categorie.P1 && c != Categorie.passager;
      @
      @ ensures \result > 0;
      @*/
    public /*@ pure @*/ float prixRepas(Categorie c) 
	throws CategorieInconnue
    {
	if ( c == Categorie.P1 )
	    return DonneesCrous.prixRepasP1;
	else if ( c == Categorie.passager )
	    return DonneesCrous.prixRepasPassager;
	else
	    throw new CategorieInconnue();
    }


    /** Debite un repas sur la carte associee a la machine. Credite la
     * carte du nombre de points correspondants, dans la limite du
     * plafond.
     * @throws CarteNonPresente
     */
    /*@ signals_only CarteNonPresente, CreditInsuffisant, CategorieInconnue;
      @
      @ signals (CarteNonPresente) ! aCarte();
      @ signals (CreditInsuffisant) carte.getMontant() - prixRepas(carte.getCategorie()) < 0;
      @
      @*/
    public void payerRepas() 
	throws CarteNonPresente, CreditInsuffisant, CategorieInconnue
    {
	if ( ! aCarte() )
	    throw new CarteNonPresente();

	if ( carte.getMontant() - prixRepas(carte.getCategorie()) < 0 )
	    throw new CreditInsuffisant();

	/* debiter le montant */
	carte.debiterMontant(prixRepas(carte.getCategorie()));

	/* Eventuellement crediter les points */
	if ( carte.getPoints() + DonneesCrous.pointsRepas <= DonneesCrous.maxPoints )
	    carte.crediterPoints(DonneesCrous.pointsRepas);
    }

    /** Effectue un paiement de repas gratuit sur la carte posee sur
     * le capteur. 
     * @throws CarteNonPresente
     */
    /*@ signals_only CarteNonPresente, CreditInsuffisant;
      @
      @ signals (CarteNonPresente) ! aCarte();
      @ signals (CreditInsuffisant) (carte.getPoints() - DonneesCrous.pointsRepasGratuit) < 0;
      @
      @*/
    public void payerRepasGratuit() 
	throws CarteNonPresente, CreditInsuffisant
    {
	if ( ! aCarte() )
	    throw new CarteNonPresente();

	if ( carte.getPoints() - DonneesCrous.pointsRepasGratuit < 0 )
	    throw new CreditInsuffisant();

	/* Effectuer le debit */
	carte.debiterPoints(DonneesCrous.pointsRepasGratuit);
    }

    /*@ also
      @ ensures \result != null;
      @*/
    public String toString() {
	if ( aCarte() )
	    return carte.toString();
	else
	    return "Aucune carte";
    }


    public static void main(String args[])
    {
	MachineCrous m = new MachineCrous();

	CarteCrous c = new CarteCrous("foobar", Categorie.passager);
	CarteCrous d = new CarteCrous("coin42", Categorie.passager);

	try {
	    System.out.println("Pose une carte...");
	    m.setCarte(c);
	    System.out.println("Pose une carte...");
	    m.setCarte(d);
	} catch ( CarteDejaPresente e ) {
	    System.out.println("Carte deja presente");
	}

	try {
	    System.out.println("Prix passager : " + m.prixRepas(c.getCategorie()));

	    System.out.println("Payer repas...");
	    m.payerRepas();

	    System.out.println("Payer repas gratuit...");
	    m.payerRepasGratuit();

	} catch ( CarteNonPresente e) {
	    System.out.println("Carte non presente");
	} catch ( CreditInsuffisant e) {
	    System.out.println("Pas assez de credit");
	} catch ( CategorieInconnue e) {
	    System.out.println("Categorie Inconnue");
	}
	
	try {
	    System.out.println("Retire carte...");
	    m.unsetCarte();
	    System.out.println("Retire carte...");
	    m.unsetCarte();
	} catch ( CarteNonPresente e ) {
	    System.out.println("Carte non presente");
	}
	
    }

}