[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Weighted graphs and adding vertices

On Fri, Oct 17, 2008 at 06:16:35PM -0700, Jerome wrote:
> 1. Has there been any work done with respect to weighted graphs?
>    That is, graphs with a value attached to their edges?

How does this look?

  weighted_graph[T: TYPE, R: TYPE FROM number]: THEORY
  BEGIN
    IMPORTING graphs@graphs[T]

    preweight: TYPE = pregraph WITH [# weight: [doubleton -> R] #]

    weighted_graph: TYPE = graph % ???

  END weighted_graph

A weighted graph is just a graph with an additional weight value
attached; where the edges map to the weight. Ideally, a weighted graph
can be used anywhere a graph is accepted. However, I'm not quite sure
how to properly PVS-define it? Any thoughts would be
appreciated. Thanks

jerome