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

[PVS-Help] Graph library

To: PVS Help <pvs-help@xxxxxxxxxxx>
Subject: [PVS-Help] Graph library
From: Jerome <jerome@xxxxxxxxxxxxxx>
Date: Mon, 15 Sep 2008 16:15:24 -0700
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>
Sender: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx
User-agent: Thunderbird 2.0.0.16 (X11/20080724)

I'm wondering how to specify conditions of a graph (graphs@graphs[nat]). For example, I'd like to say the graph R initially has 1 node, the root R(0), and no edges. How can this be done? Thanks

jerome

Follow-Ups:
- RE: [PVS-Help] Graph library
  - From: Butler, Ricky W. (LARC-D320)

Prev by Date: Re: [PVS-Help] How to use PVSio for prove formulas?
Next by Date: RE: [PVS-Help] Graph library
Previous by thread: [PVS-Help] How to use PVSio for prove formulas?
Next by thread: RE: [PVS-Help] Graph library
Index(es):
- Date
- Thread