A forum for Spin users

You are not logged in.

#1 2012-03-30 08:55:39

Registered: 2012-03-30
Posts: 1

Problem with acceptance checking


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() {
    ::(farmer==goat) -> cross_with(goat)
    ::(farmer==dog) -> cross_with(dog)
    ::(farmer==cabbage) -> cross_with(cabbage)
    ::(farmer && dog && cabbage && goat) -> goto accept
accept: skip

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

init {
    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,



#2 2012-03-30 12:59:50

Registered: 2010-11-24
Posts: 9

Re: Problem with acceptance checking

I'm not sure that I understand your model but there are a few problems:

1. When I tried to run Spin, the preprocessor failed.
I don't know enough C to know why ...
By substituting the "define"s manually,
I received assertion errors.

2. The correct mode for checking assertion errors is "Safety".
"Acceptance" is used when there is a "cycle"
usually within a never-claim or a one derived from an LTL formula.

3. In your monitor, a nondeterministic choice is made between
the two assertions. You probably want to check both of them
so they should be in the same alternative.

I hope this helps,



Board footer

Powered by FluxBB