several basic questions

Unstoppable · 2011-04-03 11:52:06

Hello everyone! I'm student from Russia and I need to write a graduate work)
I had a model of transactional algorithm based on ABP-protocol model.
This is my first experience of working with PROMELA language and there are several things, that I don't understand )
Honestly, I'm a noob in verfication ))
I'm using jSpin.

Here are my questions:
1)I've got several processes and every process can be activated in a random time, but in every moment of time it should be only one process working. I've tried to add "atomic" strings and set priority levels in each process but it didn't help.
Here is my code:

proctype SUPERProcess () priority 123{
do
::(start<2)->run Transaction();
::(start<2)->run WAL();
::(start<2)->run TrComm()
::(start<2)->run WALComm()
::(start<2)->run Timeout();
::(start<2)->run TrLoseMsg();
::(start<2)->run WALLoseMsg();
::(start ==2) -> break;
od;
}
what should I write to get a program which would start another process after terminating previous process?
hope, that I've explained my problem enough to understand ))

2) how to use "Verify" feature?
when I click on this button, I get this message:
pan:1: VECTORSZ is too small, edit pan.h (at depth 0)
pan: wrote transaction_3.pml.trail
(Spin Version 6.0.0 -- 5 December 2010)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 1632 byte, depth reached 0, ••• errors: 1 •••
0 states, stored
0 states, matched
0 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
0.098 memory usage (Mbyte)
pan: elapsed time 0 seconds
warning: only one claim defined, -N ignored

what' s the problem with VECTORSZ?
I've got the following assertion in my code:

active proctype monitor() priority 2{
do
::(WALDef==1)&&(WALInMsg.msgbit == 1-TrBit)-> assert(TrBit==WALBit);
od;
}

--

thanks a lot in advance for your help!
Max

spinroot · 2011-04-03 21:58:25

Let me start with question 1.
Note that the 'run' operator starts a process, but it does not wait for it to complete executing: the new process will run in parallel with the creating process. (It works much like a 'fork' in Unix).
So to wait for the process to terminate, assuming that no other processes are created by each of the processes you want to run, you could do this:

:: (start < 2) -> cnt = _nr_pr; run Transaction(); (cnt == _nr_pr)

you need to declare a variable called cnt of course, but _nr_pr is predefined.
This simply counts how many processes are active before you execute the run statement, and then it waits until that number goes back to what it was before you created the new process (i.e., until that new process disappears again).

spinroot · 2011-04-03 22:00:37

question 2
the message means that you should compile pan.c with a larger value for the directive VECTORSZ. the default value is 1024, and your model is larger so it requires a larger vector to store each state. you can try 2048 or 4096.
from the command line you would use:
cc -DVECTORSZ=2048 -o pan pan.c
but I'm not sure how you'd specify an extra compiler directive in jSpin -- check with the authors!

Unstoppable · 2011-04-04 18:41:37

Thanks for your answers!
Method of solving first question is quite elegant, I've applied it!)
now average number of steps in program is about 2N instead of N, but there aren't any excessive processes )

as it comes to second question, i've tried to compile pan-file using cmd and usual Spin, not jSpin.
it asks for stdint.h.
where should I add this library?
I've tried to download it and place in the folder with pan.c, but it didn't work

*I'm using gcc compiler.

Unstoppable · 2011-04-04 18:44:25

sorry, after posting this message I've found how to include -DVECTORSZ=2048 into jSpin compiler )
now trying to understand output file ))

spinroot · 2011-04-04 18:57:55

what type of system do you use: Windows or Linux?
(on Windows you need to compile with the directive -DPC added)

Unstoppable · 2011-04-04 21:24:05

forgot to say - Windows XP home )
this is what I get in an output file:
with -DPC

STEP 3 SUPERProcess
state 1 -(tr 54)-> state 2 [id 26 tp 2] [----G] transaction_3.pml:46 => ((start<2))
state 2 -(tr 55)-> state 3 [id 27 tp 2] [----G] transaction_3.pml:46 => cntprc = nr_pr
state 3 -(tr 56)-> state 4 [id 28 tp 2] [----L] transaction_3.pml:46 => (run Transaction())
....
state 34 -(tr 83)-> state 0 [id 59 tp 3500] [--e-L] transaction_3.pml:55 => -end-

without DPC

igraph p_SUPERProcess {
size="8,10";
GT [shape=box,style=dotted,label="SUPERProcess"];
S31 -> S2 [c_olor=black,style=bold,label="((start<2))"];
S31 -> S6 [c_olor=black,style=bold,label="((start<2))"];
S31 -> S10 [c_olor=black,style=bold,label="((start<2))"];.
...
and so on

it's a kind of graph, I understand )
it shows me, how we move inside the process.
but how it helps me to say that algorithm is correct?

for example, I have an assertion, I want to check that this assertion never fails.
when I perform "random" execution - it's ok, but there is no guarantee that assertion is always true.

spinroot · 2011-04-04 22:27:04

I'm only familiar with the use of iSpin -- if you use this GUI then you'd simply select the verification tab and press the run button
There's likely a similar option for jSpin.
From the command line, you'd just run the ./pan executable to get the verification result.

Unstoppable · 2011-04-09 21:48:12

hello again!)
it was easier for me to download and install jSpin version, but today I've figured out how to install iSpin.
I think, it's more powerful tool and in some aspects it is more comfortable to use.
Although, I still can't run verify process.

gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
pan.c:7667: stdint.h: No such file or directory
pan.c:7720: stdint.h: No such file or directory

I wrote about this problem several messages earlier, and it is still unsolved )

Also iSpin writes that "cannot find a dot" when I press on an Automata view button.
What should I do with it?
UPD: ah, I should just read the spin verifier's roadmap ))

Thanks in advance for your answers!)

Last edited by Unstoppable (2011-04-09 21:49:59)

spinroot · 2011-04-09 21:54:06

if you're on a Windows XP system -- just install cygwin with the gcc compiler
it includes /usr/include/stdint.h by default
if you use a different compiler setup, then you may not get this standard include file.
you could of course add it by hand, but it may be simpler to get a standard cygwin setup

Unstoppable · 2011-04-09 22:31:31

thanks!
I had a standart setup, I thought.
May be a mistake occured during installation.
So I've just added this stdint.h manually in /include directory.

ok, I've run the verifier )
It reports an error because my program ends with timeout.
I'll try to explain what I mean.

It's the end of report:
374: proc 2 (SUPERProcess) transaction_3.pml:54 (state 29) [((start==2))]
375: proc 2 terminates
spin: trail ends after 375 steps
#processes: 2
375: proc 1 (monitor) transaction_3.pml:37 (state 4)
375: proc 0 (:init:) transaction_3.pml:33 (state 19)

Init process fills in start values and runs SUPERprocess.
monitor process is an active process with assertions.
Logically program is over after SUPERprocess finishing.
but these two process (monitor and init) are still working and spin terminates with timeout signal.
how to correct this?

please refer to the code below, if you need more details )

24 init {
25 int i=0;
26 do
27 ::i==0 ->{TrFile[0]=0;i++;}
28 ::i>0&&i<Size-1 -> {TrFile[ i] = i+1;i++;}
29 ::i==Size-1 -> {TrFile[ i]=1;i++;}
30 ::i==Size -> break;
31 od;
32 run SUPERProcess();
33 }
34
35
36 active proctype monitor() priority 2{
37 do
38 /* ::atomic{(WALDef==1)&&(WALInMsg.msgbit == 1-TrBit)-> assert(TrBit==WALBit);}*/
39 /*::atomic{(WALDef==1)&&(WALInMsg.msgbit == TrBit) ->assert (TrBit==WALBit);}*/
40 ::atomic{(TrDef==1)&&(TrInMsg.msgbit == TrBit) ->assert (TrBit==1-WALBit);}
41
42 od;
43 }
44
45 proctype SUPERProcess () priority 123{
46 do
47 ::(start<2)->cntprc=_nr_pr;run Transaction();(cntprc == _nr_pr)
48 ::(start<2)->cntprc=_nr_pr;run WAL();(cntprc==_nr_pr)
49 ::(start<2)->cntprc=_nr_pr;run TrComm();(cntprc==_nr_pr)
50 ::(start<2)->cntprc=_nr_pr;run WALComm();(cntprc==_nr_pr)
51 ::(start<2)->cntprc=_nr_pr;run Timeout();(cntprc==_nr_pr)
52 ::(start<2)->cntprc=_nr_pr;run TrLoseMsg();(cntprc==_nr_pr)
53 ::(start<2)->cntprc=_nr_pr;run WALLoseMsg(); (cntprc==_nr_pr)
54 ::(start ==2) -> break;
55 od;
56 }

spinroot · 2011-04-09 23:09:46

the timeout simply says that execution has come to a halt and nothing more can happen, but the final state was not labeled (by you) as a valid endstate.
so the solution is to add the endstate labels at the start of each do loop (assuming that it is okay for the process to stop there of course)

sylvy · 2011-11-06 11:22:18

Hi! I read this interesting topic because I had a similar problem with VECTORSZ.
I use Win7. In command line I submitted : gcc -DSAFETY -DVECTORSZ=4096 -o pan pan.c
but JSpin always returns : pan:1: VECTORSZ is too small, edit pan.h (at depth 0) with 1 error
so I tried with : gcc -DSAFETY -DVECTORSZ=8192 -o pan pan.c
but it returns :

pan: out of memory
hint: to reduce memory, recompile with
-DCOLLAPSE # good, fast compression, or
-DMA=5916 # better/slower compression, or
-DHC # hash-compaction, approximation
-DBITSTATE # supertrace, approximation

(Spin Version 6.0.0 -- 5 December 2010)
Warning: Search not completed
+ Partial Order Reduction

Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +

State-vector 5916 byte, depth reached 159, errors: 0
359829 states, stored
1163880 states, matched
1523709 transitions (= stored+matched)
74554 atomic steps
hash conflicts: 135148 (resolved)

1935.594 memory usage (Mbyte)

pan: elapsed time 24.4 seconds
pan: rate 14724.762 states/second

How can I resolve this trouble?
Thanks!

Last edited by sylvy (2011-11-06 12:19:06)

theo.ruys · 2011-11-06 12:22:43

What are you doing is OK.
Due to the rather large state vector of the model (5916 bytes), VECTORSZ should be set to a value higher than 5916.

SPIN reports what is happening: the pan verifier is running "out of memory".
Given the large state vector (5916 bytes) and the number of states stored (359829) this is not surprising.
Without any compression, SPIN would have needed more than 2GB (i.e., 359829 * 5916 bytes) to store these states.

SPIN also proposes some fixes to tackle the verification more effictively.
You could first try the -DCOLLAPSE option which offers good compression with a bearable verification time penalty.
Additionally you could reserve more memory for SPIN (e.g., -DMEMLIM=4096 to give SPIN 4GB of memory).

Personally, I would first try some bitstate runs with -DBITSTATE.
Although this verification mode may not be exhaustive, it is very fast and has a more than reasonable coverage.

sylvy · 2011-11-06 16:56:16

Ok, so with:

gcc -DSAFETY -DCOLLAPSE -DVECTORSZ=6144 -o pan pan.c
the results are:

Depth= 159 States= 1e+006 Transitions= 4.96e+006 Memory= 138.757 t= 179 R= 6e+003
Depth= 159 States= 2e+006 Transitions= 1e+007 Memory= 244.615 t= 363 R= 6e+003
pan: resizing hashtable to -w21.. done

gcc -DSAFETY -DMEMLIM=4096 -DVECTORSZ=6144 -o pan pan.c
the results are:

pan: out of memory
1.9353e+009 bytes used
600000 bytes more needed
4.29497e+009 bytes limit
with 0 errors

Finally with: gcc -DSAFETY -DBITSTATE -DVECTORSZ=6144 -o pan pan.c
each proctype is unreached.

Maybe there are other type of errors in my Promela code.

Last edited by sylvy (2011-11-06 16:57:12)

dmwj80 · 2011-11-24 21:26:27

I've trouble installing Spin Version 6.0.0 on MAC where can i find the best guide for that.

spinroot · 2011-11-25 03:47:07

search for the keyword MAC on this forum

Spinroot

#1 2011-04-03 11:52:06

several basic questions

#2 2011-04-03 21:58:25

Re: several basic questions

#3 2011-04-03 22:00:37

Re: several basic questions

#4 2011-04-04 18:41:37

Re: several basic questions

#5 2011-04-04 18:44:25

Re: several basic questions

#6 2011-04-04 18:57:55

Re: several basic questions

#7 2011-04-04 21:24:05

Re: several basic questions

#8 2011-04-04 22:27:04

Re: several basic questions

#9 2011-04-09 21:48:12

Re: several basic questions

#10 2011-04-09 21:54:06

Re: several basic questions

#11 2011-04-09 22:31:31

Re: several basic questions

#12 2011-04-09 23:09:46

Re: several basic questions

#13 2011-11-06 11:22:18

Re: several basic questions

#14 2011-11-06 12:22:43

Re: several basic questions

#15 2011-11-06 16:56:16

Re: several basic questions

#16 2011-11-24 21:26:27

Re: several basic questions

#17 2011-11-25 03:47:07

Re: several basic questions

Board footer