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

RE: [PVS-Help] Graph library

t: THEORY
BEGIN
 
    IMPORTING graphs@graphs[nat]

    R: graph = (# vert := singleton[nat](0),
                  edges := emptyset[doubleton[nat]]
               #)

END t  

-----Original Message-----
From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx
[mailto:pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx] On Behalf
Of Jerome
Sent: Monday, September 15, 2008 7:15 PM
To: PVS Help
Subject: [PVS-Help] Graph library

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