[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
preweight: TYPE = pregraph WITH [# weight: [doubleton -> R] #]
weighted_graph: TYPE = 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