Spinroot

A forum for Spin users

You are not logged in.

#1 2012-10-19 16:02:52

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Technical info requested

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

Last edited by MuhammadIsmail (2012-10-19 17:48:16)

Offline

#2 2012-10-21 05:29:15

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Technical info requested

To remove the warning, you'll need to enable a search for acceptance cycles.
From the command line you do that by adding runtime flag -a to ./pan
To resolve the out of memory problem you can try to compile with -DHC4
To avoid hitting the search depth limit, just specify a larger search depth with -m
For instance:
./pan -a -m100000

Offline

#3 2012-10-31 15:05:46

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Re: Technical info requested

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.

Last edited by MuhammadIsmail (2012-10-31 15:11:41)

Offline

#4 2012-10-31 16:05:57

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Technical info requested

t is the time that has elapsed since the start of the run
R is the rate of verification: the number of new states explored per second
The number of hash conflicts is high, but that does not affect the correctness of the verification, just the speed
(more conflicts = slower, because they need to be resolved in the hash-table)
you can reduce the number by picking a  larger value for the -w parameter

when the run runs out of memory, and it has not found errors up to that point, there is no guarantee that there will be no errors if the search could continue up till the end; so in that case the search remains incomplete
there are a number of strategies that you can explore in that case to reduce memory use.
for instance, try compiling with -DCOLLAPSE, or -DHC4, or -DBITSTATE

Offline

#5 2012-10-31 17:13:23

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Re: Technical info requested

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

Offline

#6 2012-10-31 18:09:55

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Technical info requested

use ./pan -w28
(every increment in the value of -w will double the size of the hash-table.
if you pick a value that is too large, ./pan will fail because it will not be able to allocate the required memory.
if you pick a value that is too small, you incur more hash collisions)

Offline

#7 2012-11-01 15:59:55

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Re: Technical info requested

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.

Offline

#8 2012-11-01 16:34:20

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Technical info requested

The memory limit is ultimately imposed by the machine you are using: it only has a finite amount of RAM memory and that sets the memory limit...
I've answered the other question earlier: when the verification stops when you are out of memory, the verification is not complete, and therefore the model is also not completely verified.
The state vector defines the complete state of the system.

Offline

#9 2012-11-01 18:32:32

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Re: Technical info requested

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?

Last edited by MuhammadIsmail (2012-11-01 18:33:43)

Offline

#10 2012-11-01 19:07:29

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Technical info requested

if you add both HC4 *and* BITSTATE, I'm not sure which of these is going to win, or if pan.c will compile at all.
you'll have to choose one or the other, but you cannot use both simultaneously...

BITSTATE will never run out of memory
HC4 can, but only for very large problem sizes
if you still see an out of memory error then you'll have to reduce the complexity of the model -- use abstraction etc.

If you want to learn how to use the model checker well your best bet is to read one of the books that teach you how to do that, or to read through the tutorials that are online...

Offline

#11 2012-11-02 05:47:03

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Re: Technical info requested

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

Last edited by MuhammadIsmail (2012-11-02 06:07:04)

Offline

#12 2012-11-02 05:48:58

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Technical info requested

you can convert multiple claims into one, but that is almost never a smart thing to do.
spin only verifies one claim at a time
you can select which one with the -N parameter -- and if there's just one claims, that's the one you get of course

Offline

#13 2012-11-02 06:23:25

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Re: Technical info requested

what abt my second question

Offline

#14 2012-11-02 19:47:43

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Technical info requested

re Q2: why would you expect the search depth to increase?

Offline

#15 2012-11-03 10:10:32

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Re: Technical info requested

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.

Offline

#16 2012-11-03 22:31:32

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Technical info requested

There are simply a lot of reachable states that must be explored.

Offline

#17 2012-11-04 10:18:50

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Re: Technical info requested

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

Offline

#18 2013-01-19 07:43:50

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Technical info requested

all state information is included in the global state-vector:
global variables, channel contents, process states

Offline

Board footer

Powered by FluxBB