Spinroot

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