今回は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