[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Weighted graphs and adding vertices
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