Spinroot

A forum for Spin users

You are not logged in.

Pages: 1

#1 Re: General » Strange error (inline text too long) » 2013-04-15 16:53:56

HJW

In that case it must be the inline recursively calling itself since the largest definition is only about 1500 characters. Thanks. I'll see if I can find a way around that.

#2 Re: General » Strange error (inline text too long) » 2013-04-15 10:20:14

HJW

Thanks you for the answer.

Is the 64K limit for each single inline, for all inlines in the code, for all inline calls by a process or all calls by all processes?

While I have some rather long inlines, I doubt they exceed that limit (I'll check ith though).
One of them is a recursive depth first search though. I tried to limit the depth of the recursion in praxis, in theory it can go quite deep.

#3 General » Strange error (inline text too long) » 2013-04-14 11:31:26

HJW
Replies: 4

Hi,

I have problems during syntax check.

Output of iSpin is:

"inline text is too long near "connect2.pml" child process ended abnormaly"

What is the maximum length of an inline command? I put most of my models functionality in big in inlines that calls other inlines sinceit is used in several places in the model. Didn't know that would cause a problem

#4 General » Testing graph properties » 2013-03-22 20:03:26

HJW
Replies: 1

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?

#5 General » Error: place initialized var decl of... » 2012-08-08 22:40:40

HJW
Replies: 1

Hi, I keep getting this error message and don't know why or how to solve the problem:

Error: place initialized var decl of 'ia' at start of proctype     saw ';' near 'byte'

The code looks like this:
...
proctype agent (byte index) {
....
}

init{
...
byte ia = 1;
...
atomic {
        run agent(ia);
}
}
ia is a byte value that gives the process an index in a global array. From the error message I get that it is not initialized propperly. But I don't see why. Any idea what I'm doing wrong?

Thanks in advance for any clues

#6 Re: General » Array hidden in parameter » 2012-06-12 18:34:10

HJW

thanks, this helps me a great deal smile

#7 Re: General » Array hidden in parameter » 2012-06-11 19:02:05

HJW

Thank you for your answer. So I can't have an array as an input parameter. Is there a workround for this?

The model I want tow write has several processes communicating with each other. In this array I wanted to store the channels each process knows at initialisation. I could write each one in the input parameters. But that doesn't scale very well when I want to try my model with different numbers of processes.

#8 General » Array hidden in parameter » 2012-06-11 10:21:44

HJW
Replies: 4

Hi,

I want to give a selfdefined datatye to a process. But I keep getting the error message "Error: hidden array in parameter a"

My code looks like this:

typedef Array{
    int el[10]
};

proctype p(Array a){
*code*
};

Any idea why this doesn't work or how I could initialise a process with information stored in an array capsuled in a selfdefined datatype?

#9 General » Setting up flexible communication channels » 2012-03-28 11:55:07

HJW
Replies: 0

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

Pages: 1

Board footer

Powered by FluxBB