Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
Pages: 1
#1 Re: General » several basic questions » 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 }
#2 Re: General » several basic questions » 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!)
#3 Re: General » several basic questions » 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.
#4 Re: General » several basic questions » 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 ))
#5 Re: General » several basic questions » 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.
#6 General » several basic questions » 2011-04-03 11:52:06
- Unstoppable
- Replies: 16
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
Pages: 1