仮想環境でSpinモデル検査

この記事は高知工科大 Advent Calendar 2015の18日の記事です。

いきさつ

なぜだかモデル検査することになったので、とりあえず研究室のWindowsに入れることに。

Cygwinが入らねえ・・・。

色々調べてみるのもいいんだけど、ダウンロードが馬鹿みたいに長いのでもうしたくない。

Linuxなら楽そう。

なので

仮想環境でやることにしました。

環境など
- VirtualBox(15/12/18で最新のやつ)
- vagrant(15/12/18で最新のやつ)
- Ubuntu14.04(研究室にあるのと一緒にしたかった)
- spin(15/12/18で最新のやつ)

インストール

1. $ sudo apt-get install -y bisonでyaccをインストール
2. $ sudo apt-get install flexでlexをインストール
3. $ curl -O http://spinroot.com/spin/Src/spin644.tar.gzでソースコードをダウンロード ※適宜 公式で最新版確認してね
4. 下記の手順でインストール

$ gunzip spin644.tar.gz
$ tar -xf spin644.tar
$ cd Spin/Src6.4.4/
$ make
$ sudo mv spin /usr/local/bin/spin

なんの問題もなく突破。
もう開発でWindowsはやめよう。

試しにちょっと

この本を参考にちょっと動かしてみる。
ちなみに言語はPromela。

mtype = { F, S };
mtype turn = F;

active proctype Producer()
{
do
  :: (turn == F) -> printf("Producer\n"); turn = S;
od
}

active proctype Consumer()
{
do
  :: (turn == S) -> printf("Consumer\n"); turn = F;
od
}

上のチュートリアル的なコードをやってみる。
パッと見で変わったところを説明すると。
do...odが無限ループ。
::からがif文。

turnの中に、どっちのターンなのか入ってて、どっちかのプロセスが動くと、もう片方のターンになるっぽい。

下記で実行。

$ spin -u100 alt1.p

ファイル名や拡張子は何でもいいけど、-uはシミュレーションの深さを指定してて、付けないと無限ループにはまる。
何度か忘れてはまった...。

実行結果

      Producer
          Consumer
      Producer
          Consumer
      Producer
          Consumer
      Producer
          Consumer
      Producer
          Consumer
      Producer
          Consumer
      Producer
          Consumer
      Producer
          Consumer
      Producer
          Consumer
      Producer
          Consumer
      Producer
          Consumer
      Producer
          Consumer
      Producer
-------------
depth-limit (-u100 steps) reached
#processes: 2
                turn = S
100:    proc  1 (Consumer:1) alt1.p:14 (state 2)
100:    proc  0 (Producer:1) alt1.p:9 (state 5)
2 processes created

しっかり順番に実行してますね。
問題なし。

まとめ的なナニカ

本当はChromeの拡張機能でもつくろうか思ってたんだけど、12月23日までにモデル作れって言われたのでこんなことになりました......orz

とりあえず、

• Windowsで開発は正気の沙汰じゃない
• モデルによっては-uつけないとはまる
• SpinとPromelaの資料少なくて泣きそう
• クリスマスに死んでる可能性が微レ存
• 雑な記事でごめんなさい

明日はgyanemanのターンです！
よろしく！！