インストールにはWindows OS, Mac OS X,Linuxいずれも管理者権限が必要です。管理者権限がない場合は管理者にご相談ください。

Mac OS X編

準備

Spinの実行には, gccが必要である。gccが入っていない場合は,command line toolsをインストールする必要がある。
Xcodeも一緒に入れる場合は,MacでC言語 - コンパイラ(gcc)のインストール - Xcode - Command Line Tools - C言語入門 - Webkaru
commnad line toolsのみで良いという方は,Command Line Toolsのインストレーション
を参考にしてインストールする。

Dotのインストール

状態遷移図を表示させるにはDotが必要である。Dotをインストールするには,Graphviz | Graphviz - Graph Visualization SoftwareからGraphvizをインストールする。Spinのみに使うのであれば,コマンドラインツールのみあれば十分である。

Spinのインストール

http://spinroot.com/spin/Bin/index.htmlから,「MAC executable」と説明のあるspin***_mac.gzをダウロードして展開する。展開したファイル(名前はspin)をパスの通っている場所(/usr/binなど)にコピーする。(***にはspinのバージョン番号が入る。)

ispinのインストール

http://spinroot.com/spin/Src/index.htmlから,「GUIs」と説明のあるispin.tclをダウンロードし,適当な場所に保存する。ispin.tclに実行権限を付けた後にispin.tclをダブルクリックすると,ispinが起動する。実行権限の付け方としては,ターミナルで以下を実行する。
chmod 755 ispin.tcl
ダブルクリックしたときに「アプリケーション“Wish”は、破損しているか不完全である可能性があるため開けません。」のエラーが出る場合は,ispin.tclアイコンを右クリックして「情報を見る」を選択し,「このアプリケーションで開く」で「Wish」から「ターミナル」に変更する。あるいは,ターミナルで以下を実行してもよい。
$wish ispin.tcl
起動確認はこちら

Windows OS編

CygwinまたはMinGWのインストール

Spinを実行させるためにgccを実行できる環境を作る必要がある。Cygwinはアンインストールが面倒なので,試すだけでその後はアンインストールするのであればMinGWを使う方がよいかもしれない。

Cygwinのインストールの場合

  1. http://cygwin.com/にアクセスする
  2. ページの左に"Install Cygwin"のメニューがあるのでクリック
  3. インストールするPCにあわせ,setup-x86.exeまたはsetup-x86_64.exeのリンクをクリック
  4. (setup.exeを保存するかどうか聞かれたら「ファイルを保存」をクリック)
  5. ダウンロードしたsetup.exeを起動
  6. cygwin setupのウインドウで「次へ」
  7. Install from Internetをチェックして「次へ」
  8. Loca package Directoryは展開したファイルを一時的に保存するための場所,適当に選ぶ。デスクトップで構わない。(インストール終了後は削除して良い。)
  9. Direct Connection で良ければ「次へ」
  10. DownloadSite はそのままでよい。(上手くダウンロードできなければ適当に変更する。)「次へ」
  11. Select Package でgccを次のように選ぶ
  12. 「次へ」
  13. 後は自動的にインストールが進むが,途中でサーバが見つからないとかファイルがダウンロードできないなどのエラーが出たら,一旦キャンセルして別のサーバ(どこでもいい)に切り替えて実行する。
  14. 最後にデスクトップにアイコンを作るかとかメニューに入れるか聞かれるので自分の好みでチェックを入れる。(両方とも作った方がよい)

MinGWのインストールの場合

モデル検査ツール(SPIN)の使い方等のヒントを参考にインストールする。ispinを使わずにコマンドラインでspinを実行する場合はMinGWでMSYSも入れた方がよい。また,2015.2.3日現在で,上記pdfに従いインストールしてコマンドラインでspinを実行するとgcc-4がないというエラーがでるので,MinGW/bin内のgcc.exeをコピーしてgcc-4.exeを作るか,MSYSのlnコマンドを利用してgcc.exeのシンボリックリンクを作る必要がある。(ispinの場合は問題ない。)

ActiveTclのインストール

  1. http://www.activestate.com/Products/activetcl/へアクセス
  2. ActiveTcl Download Now をクリックして,X86かx64を選んでファイルを保存
  3. ダウンロードしたファイルを実行
  4. インストール場所は問題なければデフォルトの場所にする。

Dotのインストール

状態遷移図を表示させるにはDotが必要である。Dotをインストールするには,Graphviz | Graphviz - Graph Visualization SoftwareからGraphvizをインストールする。

spinのインストール

Cygwinをインストールした場合は下記に従い,MinGWの場合はモデル検査ツール(SPIN)の使い方等のヒントを参考にする。
  1. http://spinroot.com/spin/Src/index.htmlから, 「PC executable, ispin, and documentation, but no sources」と説明のある zip ファイル: pc_spin***.zipをダウンロードする。(***にはspinのバージョン番号が入る。以下***はその番号で読み替える。)
  2. ダウンロードした zip ファイルを適当なディレクトリ(例えばCドライブの直下)に展開する。
  3. 展開したディレクトリを PATH に含める。
    1. 方法:コントロールパネルのシステムを開く
    2. 「システム詳細設定」をクリックする
    3. 下部にある「環境変数」をクリック
    4. システム環境変数の中のPathをクリックして,編集をクリックする。
    5. 変数値の最後にspinのフォルダへのpathを書く(一番右のところでクリックすると入力できる。間違えて全部消してしまったときは,あわてずキャンセルして再度編集する。)
    6. pathは既に書かれているものの最後にセミコロン(;)を書いてその後ろに書く。Cドライブの直下であれば「C:\pc_spin***」等となる。
    7. 書いたら,「OK」をクリックしていく。
  4. デスクトップに,展開したディレクトリにあるispinのショートカットを作る。
起動確認はこちら

Linux編

Spinのインストール自体はhttp://spinroot.com/spin/Man/README.htmlに従えば問題なくインストールできる。ただし,Raspbianなどyaccが含まれていない場合はmakeの前にyaccをインストールする必要がある。

yaccのインストール

Raspbianの場合は
$sudo apt-get install bison
を実行する。これでyaccがインストールされる。lexもインストールする場合は
$sudo apt-get install flex
を実行する。

spinのインストール

http://spinroot.com/spin/Src/index.htmlからspin*.tar.gzをダウンロードして適当な場所で以下を実行する。
$gunzip spin*.tar.gz
$tar -xf spin*.tar
$cd Spin/Src*
$make
$sudo mv spin /usr/local/bin/spin
ターミナルからspinを実行して,Spinのバージョンが表示されればインストールは成功である。

ispinのインストール

展開したソース内のiSpinフォルダ内のinstall.shを実行する。
$sudo sh install.sh
これでターミナルからispinを実行することができる。

Dotのインストール

Raspbianの場合は
$sudo apt-get install graphviz
を実行する。

起動確認

  1. 適当なエディターで次のファイルを作成して,test.pmlと名前をつけ保存する。
    int x=0;
    active proctype P(){ 
    do 	:: true->x=x+1  ;assert (x <=5)
    	:: x>0->x=x-1
    od; 
    }
    
  2. ispin を起動する。
  3. File メニューから Open を選び,test.pmlを開く。
  4. Verificationタブをクリックして,Safetyにチェックがあり,+assertion violattionsにもチェックがあることを確認して,Runをクリックする
  5. ウインドウ下部に
    pan:1: assertion violated (x<=5) (at depth 17)
    pan: wrote test.pml.trail
    
    ...
    
    State-vector 20 byte, depth reached 17, errors: 1
           18 states, stored
            0 states, matched
           18 transitions (= stored+matched)
            0 atomic steps
    hash conflicts:         0 (resolved)
    
    のような表示があることを確認する。
なお,MinGWでspinを使う場合に,undefined reference to random and srandomのエラーが出た場合は,Spin verification - undefined reference to random and srandom - Stack Overflowに従い,MinGW\include内のstdlib.hファイルに
#define random rand
#define srandom srand
の2行を付け加える。

ispinではなく,コマンドラインからspinを使う方法

  1. 適当なエディターで,Promelaファイルを作成して保存(spin用のフォルダを作った方がよい)
  2. Mac OS Xの場合はターミナル,Windowsの場合はデスクトップのcygwinのショートカットをダブルクリックしてcygwinを起動する。(MinGWの場合はcmd.exeまたはMSYS)
  3. cdコマンドを使用して,保存したPromelaファイルのあるフォルダに移動する。
あとは
spin -u100 alt1.p
などで実行できる。
2015. 3. 9 一部リンクと語句の修正
2015. 2. 4 Mac OS Xの場合でispin.tclに実行権限をつける必要があることを追加
2015. 2. 3 MinGWの使用方法について追加
2015.1.16 Raspberry PiでSpinを使うためにLinuxの情報を追加
2014.9.16 Dotのインストールについて追記
2014.9.12 情報が相当古くなりxspinはもう配付されていないので,記載を修正し,Mac OS Xの情報も追加した。