added constraints and comments

This commit is contained in:
Lukian 2025-01-18 15:31:50 +01:00
parent a4fc5e5fe8
commit 064e0aba80
2 changed files with 483 additions and 334 deletions

View file

@ -29,11 +29,52 @@ class Jeu
operations operations
init(nom1: String,nom2: String) init(nom1: String,nom2: String)
debut() 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 end
class Joueur class Joueur
attributes attributes
Nom: String nom: String
operations operations
tirer(case: String): TypeCoup tirer(case: String): TypeCoup
tirerRobot(): TypeCoup tirerRobot(): TypeCoup
@ -43,10 +84,11 @@ class Flotte
operations operations
ajouterBateau(bateau: Bateau) ajouterBateau(bateau: Bateau)
constraints constraints
inv: bateaux->select(b: Bateau | b.type = TypeBateau::Torpilleur)->size() = 1 -- Contraintes qui vérifient que les bateaux sont de la bonne taille
inv: bateaux->select(b: Bateau | b.type = TypeBateau::Contre_Torpilleur)->size() = 2 inv torpilleur: bateaux->select(b: Bateau | b.type = TypeBateau::Torpilleur)->size() = 1
inv: bateaux->select(b: Bateau | b.type = TypeBateau::Croiseur)->size() = 1 inv contre_torpilleur: bateaux->select(b: Bateau | b.type = TypeBateau::Contre_Torpilleur)->size() = 2
inv: bateaux->select(b: Bateau | b.type = TypeBateau::Porte_Avions)->size() = 1 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 end
class Coup class Coup
@ -68,20 +110,25 @@ operations
changerEtat(nouveauEtat: TypeCase) changerEtat(nouveauEtat: TypeCase)
getEtat(): TypeCase getEtat(): TypeCase
constraints constraints
inv: plateau.cases->select(c: Case | c.x = x and c.y = y)->size() = 1 -- Contrainte qui vérifie qu'il n'y a pas deux cases au même endroit
inv: x <= 10 and x > 0 and y > 0 and y <= 10 inv unicite: plateau.cases->select(c: Case | c.x = x and c.y = y)->size() = 1
-- 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 end
class Bateau class Bateau
attributes attributes
type: TypeBateau type: TypeBateau
longueur: Integer longueur: Integer
Etat: EtatBateau etat: EtatBateau
constraints constraints
inv: type = TypeBateau::Torpilleur implies longueur = 2 -- Contraintes qui vérifient que les bateaux sont de la bonne taille
inv: type = TypeBateau::Contre_Torpilleur implies longueur = 3 inv torpilleur: type = TypeBateau::Torpilleur implies longueur = 2
inv: type = TypeBateau::Croiseur implies longueur = 4 inv contre_torpilleur: type = TypeBateau::Contre_Torpilleur implies longueur = 3
inv: type = TypeBateau::Porte_Avions implies longueur = 5 inv croiseur: type = TypeBateau::Croiseur implies longueur = 4
inv porte_avions: type = TypeBateau::Porte_Avions implies longueur = 5
-- 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
end end
association Utilise between association Utilise between
@ -91,12 +138,12 @@ end
composition Joue1 between composition Joue1 between
Joueur[1] role joueur1 Joueur[1] role joueur1
Jeu[1] role jeu2 Jeu[1] role jeu1
end end
composition Joue2 between composition Joue2 between
Joueur[1] role joueur2 Joueur[1] role joueur2
Jeu[1] role jeu1 Jeu[1] role jeu2
end end
association Tire between association Tire between
@ -111,7 +158,7 @@ end
composition Appartient2 between composition Appartient2 between
Flotte[1] role flotte Flotte[1] role flotte
Bateau[*] role bateaux Bateau[5] role bateaux
end end
composition Compose between composition Compose between
@ -125,7 +172,7 @@ Coup[1] role coup
end end
association Repartit between association Repartit between
Case[0..1] role cases Case[2..5] role cases
Bateau[2..5] role bateau Bateau[0..1] role bateau
end end

File diff suppressed because it is too large Load diff