SPIN:-o2オプションを使用して書き込みだけの変数も検証させる

spinのヘルプを見ているときに-o2オプションが気になりました。

-o2オプションのヘルプの説明を読むと書き込みだけの変数も隠さずに検証するような記述になっています。このオプションの説明から、もしかすると「SPINモデル検査入門」で紹介されている8クイーン問題の解を書き込み用のダミー変数(_)を使うことなく全て列挙できるのではないかと思い試してみました。

-o2オプションを試した結果、ダミー変数(_)を使用せずに状態で全ての解である92個が列挙されました。

ソース 8qeen.pml

使用したソースは「SPINモデル検査入門」のp.192(ソースコード 11.5)のものとなります。

-o2オプション無しでの実行

本のとおり86個の解が検出されます。

$ spin -run -E -c0 8qeen.pml
pan:1: assertion violated 0 (at depth 104)

(Spin Version 6.4.9 -- 17 December 2018)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	- (disabled by -E flag)

State-vector 56 byte, depth reached 106, errors: 86
    39249 states, stored
      788 states, matched
    40037 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    3.144	equivalent memory usage for states (stored*(State-vector + overhead))
    2.923	actual memory usage for states (compression: 92.98%)
         	state-vector as stored = 50 byte + 28 byte overhead
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  131.366	total actual memory usage


unreached in proctype Queens
	(0 of 41 states)

pan: elapsed time 0.02 seconds
pan: rate   1962450 states/second

-o2オプション有りでの実行

書き込みダミー(_)を使用していませんが92個の解が検出されます。

$ spin -o2 -run -E -c0 8qeen.pml
pan:1: assertion violated 0 (at depth 104)

(Spin Version 6.4.9 -- 17 December 2018)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	- (disabled by -E flag)

State-vector 64 byte, depth reached 106, errors: 92
    41433 states, stored
        0 states, matched
    41433 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    3.635	equivalent memory usage for states (stored*(State-vector + overhead))
    3.411	actual memory usage for states (compression: 93.84%)
         	state-vector as stored = 58 byte + 28 byte overhead
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  131.855	total actual memory usage


unreached in proctype Queens
	(0 of 41 states)

pan: elapsed time 0.02 seconds
pan: rate   2071650 states/second

spinヘルプ -o2オプション

-o2オプションを見ると書き込みだけが行われた変数を
隠さずに検証器が処理するような記述が有ります。

$ spin --help
use: spin [-option] ... [-option] file
	Note: file must always be the last argument
	-A apply slicing algorithm
:
(省略)
:
	-o1 turn off dataflow-optimizations in verifier
	-o2 don't hide write-only variables in verifier
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
	-o3 turn off statement merging in verifier
: