package batNavale;

/** Representation du jeu.
 * @author M. Nebut
 * @version 05/05
 */
public class Jeu {

    /** le premier Joueur. */
    //@ public model Joueur lejoueur1;
    //@ private represents lejoueur1 <- joueur1; 
    private Joueur joueur1; //@ in lejoueur1;
    /** le second Joueur. */
    //@ public model Joueur lejoueur2;
    //@ private represents lejoueur2 <- joueur2; 
    private Joueur joueur2; //@ in lejoueur2;

    /*@ requires j1 != null;
      @ requires j2 != null;
      @ assignable lejoueur2,lejoueur1;
      @ ensures this.lejoueur1 == j1;
      @ ensures this.lejoueur2 == j2;
      @*/
    public Jeu(Joueur j1, Joueur j2) {
	this.joueur1 = j1;
	this.joueur2 = j2;
    }

    /*@ ensures \result == this.lejoueur1;
      @*/
    public /*@ pure @*/ Joueur getJoueur1() {
	return this.joueur1;
    }

    /*@ ensures \result == this.lejoueur2;
      @*/
    public /*@ pure @*/ Joueur getJoueur2() {
	return this.joueur2;
    }


    /** Methode qui lance le jeu complet. */
    /*@ assignable lejoueur1, lejoueur2;
      @ //ensures lejoueur1.aPerdu() || lejoueur2.aPerdu();
      @*/
    public void jouer() { 
	int nbTour = 1; 
	boolean fini1 = this.joueur1.aPerdu();
	boolean fini2 = this.joueur2.aPerdu();
	boolean fini = fini1 || fini2;
	//@ loop_invariant fini == fini1 || fini2;
	//@ decreases 101 - nbTour; 
	while (! fini) {
	    System.out.println ("Tour " + nbTour);
	    System.out.println ("Au joueur 1 de jouer");
	    joueur1.jouer(joueur2);
	    System.out.println ("Au joueur 2 de jouer");
	    joueur2.jouer(joueur1);
	    fini1 = this.joueur1.aPerdu();
	    fini2 = this.joueur2.aPerdu();
	    fini = fini1 || fini2;
	    nbTour ++;
	}
	if (fini1)
	    System.out.println ("Le joueur 1 a perdu.");
	if (fini2)
	    System.out.println ("Le joueur 2 a perdu."); 
    }
   
}