ソース
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