Spinroot

A forum for Spin users

You are not logged in.

#1 2012-01-27 16:51:28

ayesha
Member
Registered: 2011-11-20
Posts: 2

question about assertion violation

Hi

When I process the following code with spin I get an assertion violation. It seems to me that the send action occurs but not the receive. Can anyone shed some light?

-------------------------------------------------------------------

mtype = { FA2 , FA3 , FA1 , FA4 , FA5 , TEST , SC0 , vector , WayPoint , noValueSpecified } ;

mtype fa = FA1;
mtype linkagenttoPAVfunction_controlAircraftfa = noValueSpecified;

chan faCH = [1] of { mtype } ;

proctype sendfa(){
    faCH!fa ;
}

proctype linkagenttoPAVfunction_controlAircraftGETSfa(){
    faCH?linkagenttoPAVfunction_controlAircraftfa ;
}

init{
         run sendfa() ;
         run linkagenttoPAVfunction_controlAircraftGETSfa() ;

       assert ( linkagenttoPAVfunction_controlAircraftfa != noValueSpecified) ;
}


-------------------------------------------------------

spin -s -t small.pml  gives me the following output:


  3:    proc  1 (sendfa) line   9 "small.pml" Send FA1    -> queue 1 (faCH)
spin: line  20 "small.pml", Error: assertion violated
spin: text of failed assertion: assert((linkagenttoPAVfunction_controlAircraftfa!=noValueSpecified))
spin: trail ends after 4 steps
#processes: 3
        fa = FA1
        linkagenttoPAVfunction_controlAircraftfa = noValueSpecified
        queue 1 (faCH): [FA1]
  4:    proc  2 (linkagenttoPAVfunction_controlAircraftGETSfa) line  13 "small.pml" (state 1)
  4:    proc  1 (sendfa) line  10 "small.pml" (state 2) <valid end state>
  4:    proc  0 (:init:) line  21 "small.pml" (state 4) <valid end state>
3 processes created


-------------------------------------------------


Regards
Ayesha

Offline

#2 2012-01-27 17:59:26

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

Re: question about assertion violation

spin merely reports that there is an execution scenario where the assertion can be reached with the initial value still present
note that a 'run' statement only creates a new process, that can then start executing asynchronously.
after you have executed a run statement and created a new process, there's no guaranteering when that process will start executing its statements -- it can delay to do so -- and that's what happens in the scenario.
so if you want to make sure that both processes completed executing before checking the assertion, you explicitly have to wait for it.  in you example you could do that by adding the wait condition "(_nr_pr == 1);" just before the assertion.
you can also check an ltl formula instead, e.g.: []<> (linkagenttoPAVfunction_controlAircraftfa != noValueSpecified)  which should hold in the example...

Offline

#3 2012-01-27 18:47:40

ayesha
Member
Registered: 2011-11-20
Posts: 2

Re: question about assertion violation

Thanks for your reply. (_nr_pr == 1); solves my problem. I should have remembered about the process behaviors.

Ayesha

Offline

Board footer

Powered by FluxBB