A forum for Spin users
You are not logged in.
Pages: 1
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.
Offline
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,
Moti
Offline
Pages: 1