SPIN:1信号(赤青黃)の遷移サンプル
「SPINによる設計モデル検証」のNever Claimの2信号サンプルがあるのですが、自身の勉強としてもっと簡単なサンプルから作成してみました。モデルとしては、赤から青になり、青から黄、黄から赤になる信号のモデルと、Never Claimを記述します。
記述したファイルは以下となります。
signal3.pml
/* 信号の色 */ mtype = { BLUE, YELLOW, RED } mtype light = RED; active proctype signal() { do :: atomic { light == RED -> if :: light = BLUE; :: light = RED; fi } :: atomic { light == BLUE -> if :: light = YELLOW; :: light = BLUE; /* バグを仕込むと検出される。*/ //:: light = RED; fi } :: atomic { light == YELLOW -> if :: light = RED :: light = YELLOW; fi } od } never n01 { /* 信号:赤からの遷移 */ LIGHT_RED: if :: light == RED -> goto LIGHT_RED :: light == BLUE -> goto LIGHT_BLUE :: else -> goto accept fi /* 信号:青からの遷移 */ LIGHT_BLUE: if :: light == BLUE -> goto LIGHT_BLUE :: light == YELLOW -> goto LIGHT_YELLOW :: else -> goto accept fi /* 信号:黃からの遷移 */ LIGHT_YELLOW: if :: light == YELLOW -> goto LIGHT_YELLOW :: light == RED -> goto LIGHT_RED :: else -> goto accept fi accept: skip; goto accept }
検証器の作成と実行
$ spin -a -run -a signal3.pml
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
(Spin Version 6.5.0 -- 17 July 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (n01)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 20 byte, depth reached 11, errors: 0
6 states, stored
7 states, matched
13 transitions (= stored+matched)
6 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.287 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype signal
signal3.pml:32, state 22, "-end-"
(1 of 22 states)
unreached in claim n01
signal3.pml:63, state 27, "-end-"
(1 of 27 states)
pan: elapsed time 0 seconds
バグを仕込む
signal3.pmlのコメントアウトしている「//:: light = RED;」をコメント解除すると、エラーが検出されてきます。
$ spin -a -run -a signal3.pml
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: acceptance cycle (at depth 12)
pan: wrote signal3.pml.trail
(Spin Version 6.5.0 -- 17 July 2019)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (n01)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 20 byte, depth reached 20, errors: 1
10 states, stored
6 states, matched
16 transitions (= stored+matched)
10 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.286 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
pan: elapsed time 0 seconds
trailの確認
信号が赤(初期値)から青、赤と遷移した際にNever claimのaccetpにジャンプすることになり、最終的にエラーとして検出されています。
$ spin -t -p -g signal3.pml starting claim 1 Never claim moves to line 39 [((light==RED))] 2: proc 0 (signal:1) signal3.pml:9 (state 1) [((light==RED))] 3: proc 0 (signal:1) signal3.pml:11 (state 2) [light = BLUE] light = BLUE Never claim moves to line 40 [((light==BLUE))] 5: proc 0 (signal:1) signal3.pml:16 (state 7) [((light==BLUE))] 6: proc 0 (signal:1) signal3.pml:19 (state 9) [light = BLUE] Never claim moves to line 47 [((light==BLUE))] 8: proc 0 (signal:1) signal3.pml:16 (state 7) [((light==BLUE))] 9: proc 0 (signal:1) signal3.pml:21 (state 10) [light = RED] light = RED Never claim moves to line 49 [else] 11: proc 0 (signal:1) signal3.pml:9 (state 1) [((light==RED))] 12: proc 0 (signal:1) signal3.pml:11 (state 2) [light = BLUE] light = BLUE <<<<<START OF CYCLE>>>>> Never claim moves to line 61 [(1)] 14: proc 0 (signal:1) signal3.pml:16 (state 7) [((light==BLUE))] 15: proc 0 (signal:1) signal3.pml:18 (state 8) [light = YELLOW] light = YELLOW 17: proc 0 (signal:1) signal3.pml:25 (state 14) [((light==YELLOW))] 18: proc 0 (signal:1) signal3.pml:27 (state 15) [light = RED] light = RED 20: proc 0 (signal:1) signal3.pml:9 (state 1) [((light==RED))] 21: proc 0 (signal:1) signal3.pml:11 (state 2) [light = BLUE] light = BLUE spin: trail ends after 21 steps #processes: 1 light = BLUE 21: proc 0 (signal:1) signal3.pml:7 (state 20) 21: proc - (n01:1) signal3.pml:61 (state 25) 1 processes created
