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

*To*: PVS Help <pvs-help@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] Weighted graphs and adding vertices*From*: Jerome <jerome@xxxxxxxxxxxxxx>*Date*: Tue, 21 Oct 2008 18:59:32 -0700*In-reply-to*: <20081018011635.GA14637@cs.caltech.edu>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20081018011635.GA14637@cs.caltech.edu>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Mutt/1.5.9i

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

**References**:**[PVS-Help] Weighted graphs and adding vertices***From:*Jerome

- Prev by Date:
**Re: [PVS-Help] Error: "Restarts:"** - Next by Date:
**[PVS-Help] Parametrized type equivalence** - Previous by thread:
**[PVS-Help] Weighted graphs and adding vertices** - Next by thread:
**[PVS-Help] Error: "Restarts:"** - Index(es):