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

ソース

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
}

一番難しかったのがLTL式

(((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