Spinroot

HJW

Member

Registered: 2012-03-28

Posts: 9

Setting up flexible communication channels

Hi everyone,
I'm a student new to model checking and very new to SPIN so bear with me, even if the solution should be simple. At my current project I've run into a problem where I'm kind of stuck. At the moment all I have for references is the book "The Spin Model Checker" by G.J.Holzmann.

What I want to do:
I want to model a distributed multi agent system. The idea behind the system is, that each agent only has limited knowledge of global system but through communication with each other they can find agents with similar properties to form clusters.

My solution was like this:
Have a single proctype Agent that consists of an ID (its pid), an int X to form clusters (agents with a similar X try to form a cluster) and a channel cnl communication (and some other stuff that is important for the clustering algorithm but not for communication).
Further each process knows n other processes.

Now I wanted to instantiate n processes, each with a random X and a random set of other processes this one knows.

From what I understand each channel has a unique name, even if they are defined locally. So sending

cnl!message

would be recived not by a specific process but by all processes listening on cnl could get it. Further multiple processes sending on the cnl channel would create a message queue each process can see.

What I want though is that each process only can send messages to processes it knows and that these messages are speciffically directed to a single process and no other can see it.
So either I need to name the channels dynamically, preferable naming them after the pid of the process they belong to or I need to build each agent by hand (which is a lot of work with more than 100 agents) or something completely different that I simply don't see

Thanks in advance for any suggestions,
HJW