Spinroot

Hello,

I'm kind of new with Spin, and facing a problem I don't get. I am using the spin version 6.1.0, with the GUI jspin.
I am working on the classical problem of the farmer which wants to cross the river with a goat, a dog and a cabbage. To modelize it in Promela, I use this code :

#define cross_alone farmer=!farmer;
#define cross_with(x) atomic{farmer=!farmer; x=!x;}
bool goat;
bool dog;
bool cabbage;
bool farmer;

proctype A() {
do
    ::cross_alone
    ::(farmer==goat) -> cross_with(goat)
    ::(farmer==dog) -> cross_with(dog)
    ::(farmer==cabbage) -> cross_with(cabbage)
    ::(farmer && dog && cabbage && goat) -> goto accept
od;
accept: skip
}

proctype monitor() {
do
    ::assert (!((goat==cabbage) && !(goat==farmer)));
    ::assert (!((goat==dog) && !(goat==farmer)));
od;
}

init {
    goat=false;dog=false;cabbage=false;farmer=false;
    run monitor(); run A();
}

The idea is to have a process which non-deterministicaly cross the river alone/with an animal/vegetable which is with me, and can jump to my acceptance state as soon as everyone has crossed. And a monitor which check that the dog is not alone with the goat, and the goat is not alone with the cabbage.

It seemed ok to me, so I launch "Verify", under the option "Acceptance", and he answer me there's an assertion fault, despite, if I make my run manually, checking the assertions at each step, I'm able to reach the acceptance state.

Am I doing something wrong with the acceptance checking process ?

Thank you for your time,

Yaya.