Mac OS X編

準備

Dotのインストール

Spinのインストール

ispinのインストール

chmod 755 ispin.tcl

$wish ispin.tcl

Windows OS編

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. • Root directoryは変更の必要がなければ「C:\cygwin」のまま
9. Loca package Directoryは展開したファイルを一時的に保存するための場所，適当に選ぶ。デスクトップで構わない。（インストール終了後は削除して良い。）
10. Direct Connection で良ければ「次へ」
11. DownloadSite はそのままでよい。（上手くダウンロードできなければ適当に変更する。）「次へ」
12. Select Package でgccを次のように選ぶ
    • Develの左の+字をクリック
    • 出てきたリストの中でpackage名が，gcc-core C compilerにチェックを入れる(Bin?のほうにチェックを入れれば良い）
13. 「次へ」
14. 後は自動的にインストールが進むが，途中でサーバが見つからないとかファイルがダウンロードできないなどのエラーが出たら，一旦キャンセルして別のサーバ（どこでもいい）に切り替えて実行する。
15. 最後にデスクトップにアイコンを作るかとかメニューに入れるか聞かれるので自分の好みでチェックを入れる。（両方とも作った方がよい）

MinGWのインストールの場合

ActiveTclのインストール

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

Dotのインストール

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編

yaccのインストール

$sudo apt-get install bison

$sudo apt-get install flex

spinのインストール

$gunzip spin*.tar.gz
$tar -xf spin*.tar
$cd Spin/Src*
$make
$sudo mv spin /usr/local/bin/spin

ispinのインストール

$sudo sh install.sh

$sudo apt-get install tk

Dotのインストール

$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)
   

   のような表示があることを確認する。

#define random rand
#define srandom srand

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

1. 適当なエディターで，Promelaファイルを作成して保存（spin用のフォルダを作った方がよい）
2. Mac OS Xの場合はターミナル，Windowsの場合はデスクトップのcygwinのショートカットをダブルクリックしてcygwinを起動する。(MinGWの場合はcmd.exeまたはMSYS）
3. cdコマンドを使用して，保存したPromelaファイルのあるフォルダに移動する。