[PVS-Help] Weighted graphs and adding vertices

[Jerome <jerome@xxxxxxxxxxxxxx>]

I have two questions pertaining to the graph library:

 1. Has there been any work done with respect to weighted graphs?
    That is, graphs with a value attached to their edges?

 2. I notice there is a function defined for deleting a vertex and
    edge, but I can't find one for addition - am I missing something?
    I've taken a stab at defining my own:

      add_vert(G: graph, v: T): graph = G WITH [vert := add(v, vert(G))]

      add_vert_to(G: graph, v: T | vert(G)(v), w: T): graph =
        (# vert  := add(w, vert(G)),
           edges := union(edg(v, w), edges(G)) #)

    could someone verify their correctness? Thanks

jerome