今回はMacに、モデル検査器SPINをインストールし、その統合環境jSpinも導入します。

[追記1] Ubuntu on Windows(Windows10)へのspin導入
[追記2] jSpinとは異なる統合環境ispinのMacへの導入

0. 今回の環境 (前提)

OS X EI Capitan "10.11.6"
Homebrew "1.1.12"
Xcode & Xcode Command Line Tools 導入済 (gcc環境が必須)
java 導入済

※. gcc -v と java -versionでそれぞれ導入済であることを確認しておいて下さい。

1. モデル検査器「SPIN」導入

Homebrewで簡単にインストールできるので、以下のコマンドを打ちましょう。

$ brew install spin

その後spinやwhich spinでSPINコマンドが無事通っているかを確認してください。

2. 統合環境「jSpin」導入

次に、GUI環境で操作したいという方向けに、統合環境jSpinを導入します。

1. ダウンロード
https://code.google.com/archive/p/jspin/downloads から、「jspin-5-0.zip」をダウンロードし、解凍して下さい。

2. 設定変更
ダウンロードしてきたjSpinの設定ファイルを以下の手順で修正していきます。

2-1. SPINのパス指定
以下のコマンドでspinコマンドのパスを表示し、そのパスをコピーしてください。

$ which spin

先ほどインストールしたjSpinのフォルダのconfig.cfgを開き、
SPIN=の後に先ほどコピーしたSPINのパスをペースト(指定)してください。

<指定例>

SPIN=/usr/local/bin/spin

2-2. gccのパス指定
以下のコマンドでgccコマンドのパスを表示し、そのパスをコピーしてください。

$ which gcc

同じくconfig.cfgの
C_COMPILER=の後に先ほどコピーしたgccのパスをペースト(指定)してください。

<指定例>

C_COMPILER=/usr/bin/gcc

3. 「jSpin」動作確認

導入作業が全て終わったところで、jSpinが正常に動くかの動作確認をします。

jSpin.jarがあるディレクトリに移り、以下のコマンドを実行してください。(もしくはjspin.jarをダブルクリック)

$ java -jar jspin.jar

jspinの起動後、Openでspin-examples内のcount.pmlなど、いずれかのpmlファイルを開き、Check, Random, Verifyボタンで、それぞれIOExceptionなどのエラーが出ずに実行できれば導入完了です。

【追記1】 Bash on Ubuntu on WindowsにSPIN導入

Bash on Ubuntu on WindowsにもSPINを導入する機会があったので一応追記。基本は[参考]http://herb.h.kobe-u.ac.jp/spin_install_document.html の通りにやれば導入できる。

0. 事前準備

sudo apt-get update
sudo apt-get upgrade
sudo apt-get install build-essential
sudo apt-get install bison
sudo apt-get install default-jre
sudo apt-get install default-jdk
sudo apt-get install wget

でjavaやwget,gcc,makeなどをapt-getでinstall

1. SPINをdownload

wget http://spinroot.com/spin/Src/spin647.tar.gz

2. 解凍~makeまで

tar -xf spin647.tar.gz
cd Spin/Src6.4.7
make
sudo mv spin /usr/local/bin/spin

※. makeやyacc系のエラーが出てる場合は上述のbuild-essentialやbisonをapt-getでinstallするとできるかと思います

これでspinコマンドを打って実行できればOKです

【追記2】Macへispin導入

前提として、spinは導入済。

1. ispinをdownload

http://spinroot.com/spin/Src/index.html のGUIsの「ispin.tcl」をdownload

2. 権限変更

ispin.tclがあるディレクトリに移動し、

chmod 755 ispin.tcl

を実行

3. 実行

wish ispin.tcl

※. 起動確認の参考 -> こちらを参考に起動確認

【追記3】その他参考

先日、previewでVSCodeのPromela拡張機能が出ていた
https://marketplace.visualstudio.com/items?itemName=dsvictor94.promela

モデル検査SPINと統合環境jSpinとispinの導入