model projet_bataille_navale

enum TypeCase {
  Vide,
  Bateau,
  Touche, 
  Rate
}

enum TypeBateau {
  Torpilleur,
  Contre_Torpilleur,
  Croiseur,
  Porte_Avions
}

enum TypeCoup {
  Rate,
  Touche,
  Touche_Coule
}

enum EtatBateau {
  Operationnel,
  Coule
}

class Jeu
operations
    init(nom1: String, nom2: String)  
    debut()
constraints
    -- Contraintes qui vérifient qu'il y a bien un bateau à un endroit coulé
    inv coule1: joueur1.plateau.cases.forAll(
        c1: Case | 
        c1.type = TypeCase::Touche 
        implies joueur2.plateau.cases->select(
            c2: Case | 
            c2.x = c1.x and c2.y = c1.y)->forAll(
                c3: Case | c3.type = TypeCase::Bateau
            )
    )
    inv coule2: joueur2.plateau.cases.forAll(
        c1: Case | 
        c1.type = TypeCase::Touche 
        implies joueur1.plateau.cases->select(
            c2: Case | 
            c2.x = c1.x and c2.y = c1.y)->forAll(
                c3: Case | c3.type = TypeCase::Bateau
            )
    )
    -- Contraintes qui vérifient qu'il n'y a pas de bateau à un endroit raté
    inv rate1: joueur1.plateau.cases.forAll(
        c1: Case | 
        c1.type = TypeCase::Rate
        implies joueur2.plateau.cases->select(
            c2: Case | 
            c2.x = c1.x and c2.y = c1.y)->forAll(
                c3: Case | c3.type = TypeCase::Vide
            )
    )
    inv rate2: joueur2.plateau.cases.forAll(
        c1: Case | 
        c1.type = TypeCase::Rate 
        implies joueur1.plateau.cases->select(
            c2: Case | 
            c2.x = c1.x and c2.y = c1.y)->forAll(
                c3: Case | c3.type = TypeCase::Vide
            )
    )
    -- Contrainte qui vérifie que les joueurs ont des noms différents
    inv noms: not(joueur1.nom = joueur2.nom)
end

class Joueur
attributes
    nom: String
operations
    tirer(case: String): TypeCoup
    tirerRobot(): TypeCoup
end

class Flotte
operations
    ajouterBateau(bateau: Bateau)
constraints
    -- Contraintes qui vérifient le nombre de bateaux par type
    inv torpilleur: bateaux->select(b: Bateau | b.type = TypeBateau::Torpilleur)->size() = 1
    inv contre_torpilleur: bateaux->select(b: Bateau | b.type = TypeBateau::Contre_Torpilleur)->size() = 2
    inv croiseur: bateaux->select(b: Bateau | b.type = TypeBateau::Croiseur)->size() = 1
    inv porte_avions: bateaux->select(b: Bateau | b.type = TypeBateau::Porte_Avions)->size() = 1
end

class Coup
attributes
    type: TypeCoup
constraints
    inv unicite: joueur.coups.isUnique(c: Coup | c.case = case)
end

class Plateau
operations
    afficherPlateau(CacherBateaux: Boolean)
end

class Case 
attributes
    x: Integer 
    y: Integer
    type: TypeCase
operations
    changerEtat(nouveauEtat: TypeCase)  
    getEtat(): TypeCase
constraints
    -- Contrainte qui vérifie qu'il n'y a pas deux cases au même endroit
    inv unicite: plateau.cases->isUnique(c: Case | c.x = x and c.y = y)
    -- Contrainte qui vérifie que le plateau est de bonne dimensions
    inv dimensions: x <= 10 and x > 0 and y > 0 and y <= 10
end

class Bateau
attributes
    type: TypeBateau
    longueur: Integer
    etat: EtatBateau
    x1: Integer
    y1: Integer
    x2: Integer
    y2: Integer
constraints
    -- Contraintes qui vérifient que les bateaux sont de la bonne taille 
    inv torpilleur1: type = TypeBateau::Torpilleur implies longueur = 2 and cases->size() = 2
    inv contre_torpilleur1: type = TypeBateau::Contre_Torpilleur implies longueur = 3 and cases->size() = 3
    inv croiseur1: type = TypeBateau::Croiseur implies longueur = 4 and cases->size() = 4
    inv porte_avions1: type = TypeBateau::Porte_Avions implies longueur = 5 and cases->size() = 2
    -- Contrainte qui dit que si toutes les cases d'un bateau sont touchées alors le bateau est coulé
    inv coule: cases->forAll(c: Case | c.type = TypeCase::Touche) implies etat = EtatBateau::Coule
    -- Contrainte qui vérifie que le bateau est soit horizontal soit vertical
    inv orientation: x1 = x2 or y1 = y2
    -- Contraintes qui vérifient que les cases du bateau correspondent bien aux coordonnées
    inv horizontal: y1 = y2 implies cases.forAll(c: Case | c.y = y1 and c.x >= x1 and c.x <= x2)
    inv vertical: x1 = x2 implies cases.forAll(c: Case | c.x = x1 and c.y >= y1 and c.y <= y2)
end

association Utilise between
Joueur[1] role joueur
Plateau[1] role plateau
end

composition Joue1 between
Joueur[1] role joueur1
Jeu[1] role jeu1
end

composition Joue2 between
Joueur[1] role joueur2
Jeu[1] role jeu2
end

association Tire between
Joueur[1] role joueur
Coup[0..100] role coups
end

association Appartient between
Joueur[1] role joueur
Flotte[1] role flotte
end

composition Appartient2 between
Flotte[1] role flotte
Bateau[5] role bateaux
end

composition Compose between
Case[100] role cases
Plateau[1] role plateau
end

association Etat between
Case[1] role case
Coup[1] role coup
end 

association Repartit between
Case[2..5] role cases
Bateau[0..1] role bateau
end