Spinroot

I'm using SPIN to verify a firmware of an embedded xxx and
I can't show my model.
So, I made a small model which has the same error with SPIN6.0.0.
-----------------------------
chan c1 = [10] of { int };
chan c2 = [10] of { int };

active proctype proc1()
{
    int msg;
    do
    ::c1?msg->
        if
        ::msg == 1->
            c2!3;
        ::msg == 2->
            c2!4;
        fi;
    od;
}

active proctype proc2()
{
    int msg;
   
    c1!1;
    do
    ::c2?msg->
        if
        ::msg == 3->
            c1!1;
        ::msg == 4->
            c1!2;
        fi;
    od;
}
-----------------------------

>You'll be interested to hear that this particular line has been in the code since version 3.2.4 from 10 January 1999 (almost 12 years).
With SPIN5.2.2, verification of the model was successfull and pan.h doesn't look wrong.
So, I think changes at 6.0.0 affects the generation rules of pan.h.