A forum for Spin users
You are not logged in.
Pages: 1
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
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
Thanks for your reply. (_nr_pr == 1); solves my problem. I should have remembered about the process behaviors.
Ayesha
Offline
Pages: 1