/* -----------------------------------------------
   (c) Projet NaBLa - Fevrier 2001
   Structures de données classiques
   Graphes avec arcs valués (pondérés)
   Version 0
   C. Attiogbe - UFR Sciences Nantes
-------------------------------------------------*/
MACHINE GrapheV
SETS
        NODE   
ABSTRACT_CONSTANTS
        Edges, Weight  /* parametres de la machine */
PROPERTIES
        Edges : NODE <-> NODE
&       Weight : Edges --> NAT
VARIABLES
        graphe         /* etat : un graphe particulier */
,       weight         /* fonction poids de ce graphe */
INVARIANT
        graphe <: Edges 
&       weight <: Weight    /* weight : graphe --> NAT */
&       dom weight = graphe
INITIALISATION
        graphe := {}
||      weight := {}
OPERATIONS
        add_edge (be, ee, ww) = 
                      /* ajoueter un arc, avec son poids au graphe */
        PRE
             be  : NODE 
        &    ee  : NODE
        &    (be, ee) /: graphe
        &    (ee, be) /: graphe
        &    ww : NAT
        THEN
             graphe := graphe \/ {be |-> ee} 
        ||   weight(be, ee) := ww
        END
/* 
;
  +++ les autres operations voulues 
*/

END