Spinroot

A forum for Spin users

You are not logged in.

#1 Re: General » Technical info requested » 2012-11-04 10:18:50

Thanks alot for your cooperation and prompt reply. Grateful to you.

#2 Re: General » Technical info requested » 2012-11-03 10:10:32

I don't know whether i am right or wrong but if it reaches the maximum depth first time (doesn't change throughout verification) then why its verification is continued for 50 min or 60 min. Clarify me I dont know.

#4 Re: General » Technical info requested » 2012-11-02 05:47:03

There is another question. I am not feeling well by questioning again and again. Kindly answer.
Q.    In ispin is it possible to verify multiple LTL properties simultaneously. From the warning I have mentioned below, I think that may be this is possible.

warning: only one claim defined, -N ignored


Q.   This is a short part of verification result. The depth doesn't increase, can you tell me the reason. Why it happens like this.
Depth=     301 States=    4e+06 Transitions= 1.35e+07 Memory=    21.150    t=      324 R=   1e+04
Depth=     301 States=    5e+06 Transitions= 1.67e+07 Memory=    21.150    t=      403 R=   1e+04
Depth=     301 States=    6e+06 Transitions= 1.93e+07 Memory=    21.150    t=      467 R=   1e+04
Depth=     301 States=    7e+06 Transitions= 2.28e+07 Memory=    21.150    t=      559 R=   1e+04
Depth=     301 States=    8e+06 Transitions=  2.6e+07 Memory=    21.150    t=      635 R=   1e+04
Depth=     301 States=    9e+06 Transitions= 2.95e+07 Memory=    21.150    t=      795 R=   1e+04
Depth=     301 States=    1e+07 Transitions= 3.23e+07 Memory=    21.150    t=      893 R=   1e+04
Depth=     301 States=  1.1e+07 Transitions= 3.51e+07 Memory=    21.150    t=      977 R=   1e+04
Depth=     301 States=  1.2e+07 Transitions= 3.84e+07 Memory=    21.150    t= 1.07e+03 R=   1e+04

#5 Re: General » Technical info requested » 2012-11-01 18:32:32

Another thing i need to know
I have tried -DHC4 -DBITSTATE and the physical memory available value as 10000 Mbytes. Even in these cases it gives error "pan: out of memory" after a lot of time. What can be done in this case. Kindly guide me on these guidelines. I am getting bored and tired now.
I can send you promela model if required for suggestions. Will be thankful for your cooperation. I have also tried -BITSTATE. Following are some of the lines of verification result.

pan: out of memory

hint: to reduce memory, recompile with -DBITSTATE # supertrace, approximation       


pan. elapsed time 1.92e+03 seconds
No errors found -- did you verify all claims?

#6 Re: General » Technical info requested » 2012-11-01 15:59:55

Two questions are still pending. Kindly answer.

Q.   What things are included in State-vector?

Q.   Can you please tell me some way by which no memory limit is imposed during verification. Also tell me about pan: out of memory. If all memory is consumed and this error happens, then can we say that the property is completely verified.

#7 Re: General » Technical info requested » 2012-10-31 17:13:23

How can we increase -w parameter in ispin. I am a new one. tell me

#8 Re: General » Technical info requested » 2012-10-31 15:05:46

Depth=   15771 States=  5.3e+07 Transitions= 2.48e+08 Memory=  1723.618    t= 2.15e+03 R=   2e+04
Depth=   15771 States=  5.4e+07 Transitions= 2.54e+08 Memory=  1750.512    t=  2.2e+03 R=   2e+04


What about t and R in the above lines of verification result?

State-vector 1772 byte, depth reached 15771, errors: 0
58341410 states, stored
2.17569e+08 states, matched
2.7591041e+08 transitions (= stored+matched)
       35 atomic steps
hash conflicts: 1.0721985e+08 (resolved)

What things are included in State-vector?
There are alot of hash conflicts? Why is this such a great number? Has it any effect on verification? I am new one. so please briefly explain.


Can you please tell me some way by which no memory limit is imposed during verification. Also tell me about pan: out of memory. If all memory is consumed and this error happens, then can we say that the property is completely verified.

#9 General » Technical info requested » 2012-10-19 16:02:52

MuhammadIsmail
Replies: 17

Can anyone please tell me the proper way of removing this warning both in ispin and using command line

warning: never claim + accept labels requires -a flag to fully verify
pan: out of memory
error: max search depth too small

#10 Re: General » Information and syntax request » 2012-10-06 11:40:49

Another thing I want to know whether is there any function of finding maximum of different values in spin instead of writing it ourself.

#11 General » Information and syntax request » 2012-10-06 11:38:38

MuhammadIsmail
Replies: 3

Can anyone please tell me about how to send arrays using send/receive in spin. Is this possible.

#12 Re: General » How to deal with exponentials in any model » 2012-09-27 16:37:03

Can you please tell me whether UPPAAL can deal with arrays, exponentials and distributed systems. SPIN also uses C compiler (cygwin). I think then it should support exponentials. Also tell me whether MATLAB can do formal verification (model checking)

#13 Re: General » How to deal with exponentials in any model » 2012-09-27 02:03:44

Then can you please help me in analyzing the correct tool wwhich can handle these calculations and better for distributed systems, have real time. Is there any tool of such kind. I need guidance from you.

#14 General » How to deal with exponentials in any model » 2012-09-26 12:32:40

MuhammadIsmail
Replies: 5

I need some way to use an exponential in my model. Is this possible. Can anyone please tell me. I am new one. If this SPIN doesn't support then please tell me if anyone know about any other model checking tool which can handle it. Without this the model cannot be accurate.

#15 Re: General » Problem with Verification Output » 2012-07-27 05:14:04

I also have the same problem and unable to upload my code

#16 General » How to introduce time in SPIN » 2012-05-29 12:55:00

MuhammadIsmail
Replies: 1

I need to use time as a parameter for analysis. Is there any way to observe the behavior of model with time.  If there is some way then please tell me.
Thanks

#18 Re: General » How to declare a two D array of 12 bits location each » 2012-05-25 06:49:24

[u]Here when I am sending the complete model. It gives me the following errer.[/u]

406 not acceptable
An appropriate representation of the requested resource /fluxbb/post.php could not be found on this server.

Additionally, a 404 Not Found error was encountered while trying to use an ErrorDocument to handle the request.

#19 Re: General » How to declare a two D array of 12 bits location each » 2012-05-24 07:22:10

Is there any way to declare 12 bit array or not.
Is this a problem of state explosion.

#20 Re: General » How to declare a two D array of 12 bits location each » 2012-05-24 06:49:29

When I use byte the complete model is working ok. but when I change it to short it gives the result as mentioned. I need actually 12 bits. I think 12 bits will work in my model.
By 16 bits(short) even the execution cannot proceed from the start.
By 8 bits(byte) everything is ok but there is truncation when I use simulation/run.

Please give me some reason for this. I think it is state explosion. I do not know whether I am right or wrong.
I need a solution for how to make a 12 bit 2-D array to avoid this problem.

#21 General » How to declare a two D array of 12 bits location each » 2012-05-22 15:44:02

MuhammadIsmail
Replies: 8

I need to declare 2D arrays but using "short datatype" the verification is not proceeding and on run following is displayed

State-vector 1028 byte, depth reached 27, errors: 1
        1 states, stored
        0 states, matched
        1 transitions (= stored+matched)
       27 atomic steps
hash conflicts:         0 (resolved)

    2.539	memory usage (Mbyte) 

I can't able to understand this

I am making 2D array as follows

typedef VECTOR1{
		short vector1[c];
		}
	VECTOR free[r];             			
	VECTOR used[r];   

   
  Please have a look at code and propose some solution

Board footer

Powered by FluxBB