# 例題:うさぎとおおかみ解いてみた

#### ソース

```mtype = {A, AtoB, B, BtoA};
int RbA, RbB, RbS, WoA, WoB, WoS;
mtype Splace;

inline toBank(RbX, WoX){
atomic{
RbX=RbX+RbS;RbS=0;
WoX=WoX+WoS;WoS=0;
}
}
inline fromBank(RbX, WoX){
atomic{
if
::(RbX>=2) -> RbX = RbX-2; RbS = RbS+2;
::(RbX>=1) -> RbX = RbX-1; RbS = RbS+1;
::(RbX>=0) -> skip;
fi;
if
::(WoX>=2) -> WoX = WoX-2; WoS = WoS+2;
::(WoX>=1) -> WoX = WoX-1; WoS = WoS+1;
::(WoX>=0) -> skip;
fi;
}
}

active proctype ship(){
RbA=3;
RbB=0;
RbS=0;
WoA=3;
WoB=0;
WoS=0;
Splace=A;

fromBank(RbA, WoA);
Splace = AtoB;

do
::true->
if
::(Splace==AtoB)->printf("(%d %d) -(%d %d)->(%d %d)\n", RbA, WoA, RbS, WoS, RbB, WoB);
::(Splace==BtoA)->printf("(%d %d)<-(%d %d)- (%d %d)\n", RbA, WoA, RbS, WoS, RbB, WoB);
::else->skip;
fi;
if
::(Splace==A) -> toBank(RbA, WoA);fromBank(RbA, WoA);Splace=AtoB;
::(Splace==AtoB) -> Splace=B;
::(Splace==B) -> toBank(RbB, WoB);fromBank(RbB, WoB);Splace=BtoA;
::(Splace==BtoA) -> Splace=A;
fi
od
}

never  {    /* (((RbA==0)||(RbA>=WoA))&&((RbB==0)||(RbB>=WoB))&&((RbS==0)||(RbS>=WoS))&&(!((Splace==AtoB)||(Splace==BtoA))||((RbS+WoS==1)||(RbS+WoS==2))))U(RbB+WoB==6) */
T0_init:
if
:: ((RbB+WoB==6)) -> goto accept_all
:: ((((RbA==0)||(RbA>=WoA))&&((RbB==0)||(RbB>=WoB))&&((RbS==0)||(RbS>=WoS))&&(!((Splace==AtoB)||(Splace==BtoA))||((RbS+WoS==1)||(RbS+WoS==2))))) -> goto T0_init
fi;
accept_all:
skip
}```

`(((RbA==0)||(RbA>=WoA))&&((RbB==0)||(RbB>=WoB))&&((RbS==0)||(RbS>=WoS))&&(!((Splace==AtoB)||(Splace==BtoA))||((RbS+WoS==1)||(RbS+WoS==2))))U(RbB+WoB==6)`

をちゃんと書くところだった

#### 実行結果

```\$ spin -a rabit_wolf.pml
\$ gcc pan.c
\$ ./a.out -a
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan:1: end state in claim reached (at depth 352)
pan: wrote rabit_wolf.pml.trail

(Spin Version 6.1.0 -- 4 May 2011)
Warning: Search not completed
+ Partial Order Reduction

Full statespace search for:
never claim         	+ (never_0)
assertion violations	+ (if within scope of claim)
acceptance   cycles 	+ (fairness disabled)
invalid end states	- (disabled by never claim)

State-vector 52 byte, depth reached 352, errors: 1
303 states, stored
8 states, matched
311 transitions (= stored+matched)
41 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
0.023	equivalent memory usage for states (stored*(State-vector + overhead))
0.278	actual memory usage for states (unsuccessful compression: 1202.08%)
state-vector as stored = 934 byte + 28 byte overhead
4.000	memory used for hash table (-w19)
0.534	memory used for DFS stack (-m10000)
4.730	total actual memory usage

pan: elapsed time 0 seconds

\$ spin -t -s rabit_wolf.pml
Never claim moves to line 58	[((((((RbA==0)||(RbA>=WoA))&&((RbB==0)||(RbB>=WoB)))&&((RbS==0)||(RbS>=WoS)))&&(!(((Splace==AtoB)||(Splace==BtoA)))||(((RbS+WoS)==1)||((RbS+WoS)==2)))))]
(2 2) -(1 1)->(0 0)
(2 2)<-(1 1)- (0 0)
(3 1) -(0 2)->(0 0)
(3 1)<-(0 1)- (0 1)
(3 0) -(0 2)->(0 1)
(3 0)<-(0 1)- (0 2)
(1 1) -(2 0)->(0 2)
(1 1)<-(1 1)- (1 1)
(0 2) -(2 0)->(1 1)
(0 2)<-(0 1)- (3 0)
(0 1) -(0 2)->(3 0)
(0 1)<-(1 0)- (2 2)
(0 0) -(1 1)->(2 2)
Never claim moves to line 57	[(((RbB+WoB)==6))]
Never claim moves to line 61	[(1)]
spin: trail ends after 352 steps
#processes: 1
RbA = 0
RbB = 1
RbS = 2
WoA = 0
WoB = 1
WoS = 2
Splace = B
352:	proc  0 (ship) rabit_wolf.pml:48 (state 101)
352:	proc  - (never_0) rabit_wolf.pml:62 (state 8) <valid end state>
1 processes created```