DTSpinインストール方法

環境

• Ubuntu 20.04

概要

モデル検査ツールのSpinはその構造上、時間の概念を扱うのに難があります。これに時間変数を導入したのがDTSpinです。今後利用方法について記事書く予定です。取り急ぎインストール手順だけまとめます。

手順

配布サイトの以下にてDTSpinLinux.binをダウンロードします。

ダウンロードしたフォルダにて以下コマンドを打っていきます。

chmod +x ./DTSpinLinux.bin
mv DTSpinLinux.bin /usr/bin/dtspin

これで完了です。以下のように、dtspinコマンドが使用可能になっています。

$ dtspin -h
use: spin [-option] ... [-option] file
	Note: file must always be the last argument
	-a generate a verifier in pan.c
	-B no final state details in simulations
	-b don't execute printfs in simulation
	-C print channel access info (structview)
...

ためしに、上記配布サイトのFischerのサンプルを実行してみます。拡張子は適当に.pmlとしました。
実行の際には同じフォルダにこのヘッダ:dtime.hを置いておく必要があります。
以下実行します。

dtspin -a Fischer.pml 

これでpan.c, pan.hが生成されます。
私の環境の場合、pan.hの一行目のdefineがC言語の構文エラーとなってしまったので以下で修正しました。

sed '1 s/$/ \\&/' pan.h > out.h; mv out.h pan.h

以下でコンパイルします。

gcc -DSAFETY -DNOFAIR -o pan pan.c

panが生成されるので、それを実行します。

$ ./pan 
warning: for p.o. reduction to be valid the never claim must be stutter-closed
(never claims generated from LTL formulae are stutter-closed)
(Spin Version 3.3.10 -- 15 March 2000 + Discrete-Time Extension Version 0.1.1 -- 4 April 2000)
        + Partial Order Reduction

Full statespace search for:
        never-claim             +
        assertion violations    + (if within scope of claim)
        cycle checks            - (disabled by -DSAFETY)
        invalid endstates       - (disabled by never-claim)

State-vector 72 byte, depth reached 5181, errors: 0
  503898 states, stored
...

以上。