added preconditions for boat type limits and updated state change operation

This commit is contained in:
Lukian 2025-01-18 18:23:55 +01:00
parent 22408c8fec
commit 4b2c5d16f2
2 changed files with 133 additions and 127 deletions

View file

@ -77,12 +77,17 @@ attributes
nom: String
operations
tirer(case: String): TypeCoup
-- pre libre: plateau.cases.
tirerRobot(): TypeCoup
end
class Flotte
operations
ajouterBateau(bateau: Bateau)
pre torpilleur: bateau.type = TypeBateau::Torpilleur implies bateaux->select(b: Bateau | b.type = TypeBateau::Torpilleur)->size() < 1
pre contre_torpilleur: bateau.type = TypeBateau::Contre_Torpilleur implies bateaux->select(b: Bateau | b.type = TypeBateau::Contre_Torpilleur)->size() < 2
pre croiseur: bateau.type = TypeBateau::Croiseur implies bateaux->select(b: Bateau | b.type = TypeBateau::Croiseur)->size() < 1
pre porte_avions: bateau.type = TypeBateau::Porte_Avions implies bateaux->select(b: Bateau | b.type = TypeBateau::Porte_Avions)->size() < 1
constraints
-- Contraintes qui vérifient le nombre de bateaux par type
inv torpilleur: bateaux->select(b: Bateau | b.type = TypeBateau::Torpilleur)->size() = 1
@ -109,7 +114,9 @@ attributes
y: Integer
type: TypeCase
operations
changerEtat(nouveauEtat: TypeCase)
changerEtat(nouveauEtat: TypeCase)
pre different: not(nouveauEtat = type)
post change: type = nouveauEtat
getEtat(): TypeCase
constraints
-- Contrainte qui vérifie qu'il n'y a pas deux cases au même endroit