Give an example for logical problems farmer, wolf, goat and cabbage. Solving the problems of farmer-wolf -goat cabbafe with spin

Ancient task: The farmer needs to transport through the river of a wolf, a goat and cabbage. The boat contains except the farmer just something one. But without farmer it is impossible to leave a wolf with a goat, and a goat – with cabbage

Though system not discrete, for the solution of a task it is possible to construct abstract model - system of transitions, and to investigate possible ways.

f-Fermerna right the W-wolf on the right the G-goat on right s-Kapusta on the right

Properties of system farmer-wolf-goat-cabbage

1. It is possible to get to a final state

EF fwgc

2. There is such solution of a task at which if the goat moves to that party, it there forever also remains

3. Though on one way conducting to the purpose, restrictions are observed

4. At any version of the solution of a task the farmer will have to come back through the river one

19. Give an example for logical "Chiness Rings". Solving the problems of "Chiness Rings" with spin

The puzzle – to remove all rings from a loop and/or to put on them

1. The first ring can always be removed or put on

2. If all are removed to N-1, and N - No, that can remove or put on N+1

In Spin

bool all_right_side;
active proctype rings() {

bool x1=true, x2=true, x3=true, x4=true, x5=true;
all_right_side = false;
printf("MSC: x1 %d x2 %d x3 %d x4 %d x5 %d \n", x1, x2, x3, x4, x5);
do
:: (x1==false) && (x2==false) && (x3==false) && (x4==false) &&(x5==false)->all_right_side = true;
break;
:: else ->
if
::(x1==true)->x1=false;
::(x1==false)->x1=true;

::(x1==true && x2==true)->x2=false;
::(x1==true && x2==false)->x2=true;

::(x1==false && x2==true && x3==true)->x3=false;
::(x1==false && x2==true && x3==false)->x3=true;

::(x1==false && x2==false && x3==true && x4==true)->x4=false;
::(x1==false && x2==false && x3==true && x4==false)->x4=true;

::(x1==false && x2==false && x3==false && x4==true && x5==true)->x5=false;
::(x1==false && x2==false && x3==false && x4==true && x5==false)->x5=true;

::(x1==false && x2==false)->x2=true;
::(x1==false && x2==true)->x2=false;

::(x1==true && x2==false && x3==false)->x3=true;
::(x1==true && x2==false && x3==true)->x3=false;

::(x1==true && x2==true && x3==false && x4==false)->x4=true;
::(x1==true && x2==false && x3==true && x4==true)->x4=false;

fi;
printf("MSC: x1 %d x2 %d x3 %d x4 %d x5 %d \n", x1, x2, x3, x4, x5);

od; printf("MSC: OK!\n")
}

Date: 2016-01-03; view: 1786