Type abstrait Sommet
AXIOMES

	Préconditions
		---
	Postconditions
	
		creerSommet(nom).recNom().estEgal(a)
		Sommet s => s.affNom(nom2).recNom().estEgal(nom2)
		
FIN
	
	
Type abstrait Produit hérite Sommet
AXIOMES

	// Remarque à ajouter dans le rapport : le constructeur creerProduit surcharge creerSommet => pas besoin des réécrire les opérations
	
	Préconditions Produit p
	
		définie(p.recNumWagon()) <=> p.estAffecte()
	
	Postconditions Produit p
	
		NON creerProduit(nom).estAffecte()
		p.affNumWagon(i).estAffecte()
		p.affNumWagon(i).recNumWagon().estEgal(i)
		
FIN 


Type abstrait Ville hérite Sommet
AXIOMES
	
	// Remarque à ajouter dans le rapport : le constructeur creerVille surcharge creerSommet => pas besoin des réécrire les opérations
	
	Préconditions Ville v
		---
	Postconditions Ville v
	
		creerVille(nom,n).recIndice().estEgal(n)
		NON creerVille(nom,n).estMarque()
		v.marquer().estMarque()
		NON v.demarquer().estMarque()
		
FIN 


Type abstrait Arete
AXIOMES
	
	Préconditions Arete a
	
		définie(creerArete(sA,sB)) <=> NON sA.estEgal(sB)
		
	Postconditions Arete a
	
		creerArete(sA,sB).recS1().estEgal(sA)
		creerArete(sA,sB).recS2().estEgal(sB)
		
FIN


Type abstrait Liaison hérite Arete 
AXIOMES
	
	// Remarque à ajouter dans le rapport : le constructeur creerLiaison surcharge creerSommet => pas besoin des réécrire les opérations
	
	Préconditions Liaison l
	
		définie(creerLiaison(sA,sB,temps)) <=> (NON sA.estEgal(sB)) ET (temps >= 0)
		
	Postconditions Liaison l
	
		creerLiaison(sA,sB,temps).recS1().estEgal(sA)
		creerLiaison(sA,sB,temps).recS2().estEgal(sB)
		creerLiaison(sA,sB,temps).recTemps().estEgal(temps)
		
FIN


Type abstrait Graphe // A Vérifier
AXIOMES
	
	Préconditions Graphe g ; Sommet s ; Arete a
	
		définie(g.ajouterSommet(s)) <=> NON (g.sommetAppartient(s))
		définie(g.ajouterArete(a)) <=> NON (g.areteAppartient(a))
											ET g.sommetAppartient(a.recS1())
											ET g.sommetAppartient(a.recS2())
		définie(g.recSommetsVoisins(s)) <=> g.sommetAppartient(s)
		
	Postconditions Graphe g ; Sommet s,s1,s2 ; Arete a,a1,a2
		// On gere les aretes
		NON creerGraphe().areteAppartient(a)
		a1.estEgal(a2) => g.ajouterArete(a1).areteAppartient(a2)
		NON a1.estEgal(a2) =>g.ajouterArete(a1).areteAppartient(a2) = g.areteAppartient(a2)
		// On gere les sommets
		NON creerGraphe().sommetAppartient(s)
		s1.estEgal(s2) => g.ajouterSommet(s1).sommetAppartient(s2)
		NON s1.estEgal(s2) =>g.ajouterSommet(s1).sommetAppartient(s2) = g.sommetAppartient(s2)
		//  On gere le nbre de sommets
		creerGraphe().recNombreSommets() = 0
		g.ajouterSommet(s).recNombreSommets() = 1 + g.recNombreSommets()
		// On gere le nbre d'aretes
		creerGraphe().recNombreAretes() = 0
		g.ajouterArete(a).recNombreAretes() = 1 + g.recNombreAretes()
		// On gere le recSommets
		g.recSommets().borneInf() = 1
		g.recSommets().borneSup() = g.recNombreSommets()
		g1.egalA(g.ajouterSommet(s)) => g1.recSommets().recVal(g1.recNombreSommets()).estEgal(s)
		// On gere le recAretes
		g.recAretes().borneInf() = 1
		g.recAretes().borneSup() = g.recNombreAretes()
			*{ Autre idée : ajouter un observateur qui récupère la 'position' d'un sommet qui est egale à son ordre d'ajout;
			le premier ajouté a pour position 1, et le dernier le nouveau nombre d'aretes }*
		g1.egalA(g.ajouterArete(a)) => g1.recAretes().recVal(g1.recNombreAretes()).estEgal(a)
		
	Opérations d'extension recSommetsVoisins(Sommet s) : vecteur de sommets
		références locales
			vectArete,vectSommetsVoisins : Graphe
			nbVoisins : Entier
		DEBUT
			vectArete <-- g.recAretes()
			nbVoisins <-- 0
			Pour i <-- vectArete.borneInf() à vectArete.borneSup() pas 1 Faire
				Si (vectArete.recVal(i).recS1().estEgal(s)) OU (vectArete.recVal(i).recS2().estEgal(s)) Alors
					nbVoisins <-- nbVoisins + 1
				FinSi
			FinPour
			vectSommetsVoisins <-- creerVecteur(1,nbVoisins)
			nbVoisins <-- 1
			Pour i <-- vectArete.borneInf() à vectArete.borneSup() pas 1 Faire
				// Si le premier sommet est s 
				Si (vectArete.recVal(i).recS1().estEgal(s)) Alors
					// alors le second sommet est son voisin
					vectSommetsVoisins.affVal(nbVoisins , vect.Arete.recVal(i).recS2())
					nbVoisins <-- nbVoisins + 1
				Sinon
					// Si le second sommet est s 
					Si (vectArete.recVal(i).recS2().estEgal(s)) Alors
						// alors le premier sommet est son voisin
						vectSommetsVoisins.affVal(nbVoisins , vect.Arete.recVal(i).recS1())
						nbVoisins <-- nbVoisins + 1
					FinSi
				FinSi
			FinPour
			retourner vectSommetsVoisins
		FIN
FIN


Type abstrait ReseauTransport hérite Graphe // TODO : A VERIFIER
AXIOMES

	// Remarque à ajouter dans le rapport : 
	// le constructeur creerReseauTransport surcharge creerGraphe => pas besoin des réécrire les opérations
	// le transformateur ajouterVille surcharge ajouterSommet ~~~~HUM HUM HUM pas sur du tout. Dire que l'indice d'un ville est egal à sa position dans le vecteur ...
	// le transformateur ajouterLiaison surcharge ajouterArete
	
	Préconditions ReseauTransport rt
		LINCIDE DUNE VILLE CORRESPOND A SA POSITION DAJOUT
	Postconditions ReseauTransport rt
		---
	Opérations d'extension calculerChemin(Ville origine,Ville Destination)
		références locales
			vectSommet : vecteur
			vectDist : vecteur
			vectPred : vecteur
		DEBUT
		// Création des vecteurs
		vectSommet <-- rt.recSommets()
		vectDist <-- creerVecteur( 1 , rt.recNombreSommets() )
		vectPred <-- creerVecteur( 1 , rt.recNombreSommets() )
		
		// Initialisation des distances
		Pour i <-- vectDist.recBorneInf() à vectDist.recBorneSup() pas 1 Faire
			vectDist.affVal(i,-1)
		FinPour
		vectDist.affVal( origine.recIndice() , 0 ) // L'INDICE D'UNE VILLE EST SA POSITION DANS LE VECTEUR --> LE DIRE
		
		
		TousLesSommetsMarques <-- FAUX
		TantQue NON TousLesSommetsMarques Faire
			// On récupère le sommet non marqué le moins cher
			pos_min <-- -1
			Pour i <-- vectSommet.recBorneInf() à vectSommet.recBorneSup() pas 1 Faire
				Si NON vectSommet.recVal(i).estMarque Alors
					Si pos_min = -1 Alors
						pos_min <-- i
					Sinon
						Si	vectDist.recVal(i) < vectDist.recVal(pos_min) Alors
							pos_min <-- i
						FinSi
					FinSi
				FinSi
			FinPour
			sommetTmp <-- vectSommet.reecVal(pos_min)
			// On récupère les voisins du sommet en question
			vectTmp <-- rt.recSommetsVoisins(sommetTmp)
			// On fait les MAJ éventuelles
			Pour i <-- vectTmp.recBorneInf() à vectTmp.recBorneSup() pas 1 Faire
				Si NON vectTmp.recVal(i).estMarque() Alors
					// On récupère l'arete concernée
					Pour vectArete.recBorneInf() à vectArete.recBorneSup() pas 1 Faire
						Si ( ( vectArete.recVal(i).recS1().estEgal(sommetTmp) ET  vectArete.recVal(i).recS2().estEgal(vectTmp.recVal(i)) ) 
						OU ( vectArete.recVal(i).recS1(vectTmp.recVal(i)).estEgal() ET vectArete.recVal(i).recS2().estEgal(sommetTmp) ) ) Alors
							areteTmp <-- vectArete.recVal(i)
						FinSi
					FinPour
					// On verifie que le nouveau chemin est plus court
					Si vectDist( vectTmp.recVal(i).recIndice() ) > vectDist(vectTmp.recIndice()) + areteTmp.recTemps() Alors
						vectDist( vectTmp.recVal(i).recIndice() ) <-- vectDist(vectTmp.recIndice()) + areteTmp.recTemps()
						vectPre ( vectTmp.recVal(i).recIndice() ) <-- sommetTmp
					FinSi
				FinSi
			FinPour
			// On marque le sommet courant
			sommetTmp.marquer()
			// On vérifie s'il reste des sommets non marqués	
			TousLesSommetsMarques	<-- VRAI		
			Pour i <-- vectSommet.recBorneInf() à vectSommet.recBorneSup() pas 1 Faire
				Si (NON vectSommet.recVal(i).estMarque) Alors
					TousLesSommetsMarques <-- FAUX
					break
				FinSi
			FinPour
			
		FinTantQue
		FIN
		
FIN


Type abstrait ListeProduits hérite Graphe // A VERIFIER
AXIOMES
	
	// Remarque à ajouter dans le rapport : 
	// le constructeur creerReseauTransport surcharge creerGraphe => pas besoin des réécrire les opérations
	// le transformateur ajouterVille surcharge ajouterSommet
	// le transformateur ajouterLiaison surcharge ajouterArete
	
	Préconditions ListeProduits lp
		---
	Postconditions ListeProduits lp
		---
	Opérations d'extension affecterNumeroWagon()
		références locales
	DEBUT
		vectDeg = creerVecteur(1,g.recNombreSommets())
		// On initialise le degré de chaque sommet à 0
		Pour i <-- 1 à g.recNombreSommets() pas 1 Faire
			vectDeg.affVal(i,0);
		FinPour
		// On va remplir le tableau des degrés
		tmp = lp.recAretes()
		Pour j <-- tmp.recBorneInf() à tmp.recBorneSup() pas 1 Faire
			vectDeg.affVal( tmp.recVal(i).recS1() , vectDeg.recVal(tmp.recVal(i).recS1()) + 1 )
			vectDeg.affVal( tmp.recVal(i).recS2() , vectDeg.recVal(tmp.recVal(i).recS2()) + 1 )
		FinPour
		
		couleur <-- 1
		cpt <-- vectBorneInf()
		TantQue ( cpt < vectDeg.recBorneSup() ) Faire			
			// On récupère le max
			pos <-- vectDeg.recBorneInf()
			Pour i <-- vectDeg.recBorneInf() à vectDeg.recBorneSup() pas 1 Faire
				Si( vectDeg.recVal(i) vect.recVal(pos) )Alors
					pos <-- i 
				FinSi
			FinPour
			// On lui affete la nouvelle couleur
			lp.recAretes().recVal(pos).affNumWagon(couleur)
			// On incremente les compteurs
			cpt <-- cpt + 1
			// On met à jour le vectDeg
			vectDeg.affVal(pos,-1)
			// On essaie les autres
			Pour i <-- lp.recSommets().recBorneInf() à lp.recSommets().recBorneSup() pas 1 Faire
				Si ( NON lp.recSommets().recVal(i).estAffecte() ) Alors
					tmp <-- lp.recSommetsVoisins( lp.recSommets().recVal(i) )
					affectable <-- VRAI
					Pour j <-- tmp.recBorneInf() à tmp.recBorneSup() pas 1 Faire
						Si ( tmp.recVal(j).estAffecte() )
						Si ( tmp.recVal(j).recNumWagon().estEgal(couleur) ) Alors
							affectable <-- FAUX
						FinSi
					FinPour
					Si affectable Alors
						lp.recSommets().recVal(i).affNumWagon(couleur)
						cpt <-- cpt + 1
						vectDeg.affVal(i,-1)
					FinSi
				FinSi
			FinPour
			// On change la couleur			
			couleur <-- couleur + 1
		FinTantQue	
	FIN
	
FIN


Type abstrait Wagon // A Vérifier
// Besoin d'un nouvel observateur :
Observateur recNombreProduits() : Entier
AXIOMES
	
	Préconditions Wagon w
	
		définie(creerWagon(n)) <=> n >= 0
		définie(w.ajouterProduit(p)) <=> NON (w.produitAppartient(p))
		
	Postconditions Wagon w
		
		// On gere le numero du wagon
		creerWagon(n).recNumero().estEgal(n)
		// On gere l'appartenance d'un produit
		NON creerWagon(n).produitAppartient(p)
		p1.estEgal(p2) => w.ajouterProduit(p1).produitAppartent(p2)
		NON p1.estEgal(p2) => w.ajouterProduit(p1).produitAppartient(p2) = w.produitAppartient(p2)
		// On gere le nombre de produits
		creerWagon(n).recNombreProduits() = 0
		w.ajouterProduit(p).recNombreProduits() = 1 + w.recNombreProduits()
		// On gere le recProduits
		w.recProduits().borneInf() = 1
		w.recProduits().borneSup() = w.recNombreProduits()
		w1.egalA(w.ajouterProduit(p)) => w1.recProduits().recVal(w1.recNombreProduits()).estEgal(p)
FIN


Type abstrait Train // A Vérifier
// Besoin d'un nouvel observateur :
Observateur recNombreWagons() : Entier
AXIOMES
	
	Préconditions Train t
	
		définie(t.ajouterWagon(w)) <=> NON (t.wagonAppartient(w.recNumero()))
		
	Postconditions Train t
	
		NON creerWagon().wagonAppartient(w)
		w1.estEgal(w2) => t.ajouterWagon(w1).produitWagon(w2)
		NON w1.estEgal(w2) => t.ajouterWagon(w1).wagonAppartient(w2) = t.wagonAppartient(w2)
		// On gere le nombre de wagons
		creerTrain().recNombreWagons() = 0
		t.ajouterWagon(w).recNombreWagons() = 1 + g.recNombreWagons()
		// On gere le recWagons
		t.recWagons().borneInf() = 1
		t.recWagons().borneSup() = w.recNombreWagons()
		t1.egalA(t.ajouterWagon(w)) => t1.recWagons().recVal(t1.recNombreWagons()).estEgal(w)
FIN