Spinroot

A forum for Spin users

You are not logged in.

#1 2013-03-22 20:03:26

HJW
Member
Registered: 2012-03-28
Posts: 9

Testing graph properties

Hi,

I'm trying verify properties of an undirected graph in my current project. But I get my head around how to do it.
Basically I have n running processes which are nodes in the graph.
The edges are channels the processes know. Each process has a set of such edges >1.

For example process0 is connected to process4; this means that process0 knows the channel asigned to process4 and so can send messages to process4.
This also means that there is an undirected edge between process0 and process4 (even though the channel is directional)

Now I want to verify that from every process I can reach every other process using those edges (number of steps it takes doesn't matter).

The graph starts in that state. But the edges can change over time. While the edges are changed this condition doesn't have to be fullfilled.
edges are represented by this selfdefined type:

typedef Link{
    pid from;
    pid to;
    chan source;
    chan target;
};

To test this I thought of making a []<>p statement where p means that I can reach the every node.
But I have no idea how to check for p.

Can anyone help me?

Offline

#2 2013-03-22 23:06:05

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Testing graph properties

How about defining an internal variable, say "bool reached", in each process?  The initial value of reached is false.  At the begining of the propagation, assign true to the starting process and check if all these variables reached can be eventually true.

Offline

Board footer

Powered by FluxBB