SPINの支援環境ツールについて
まずSPIN
- SPINを動かすには以下のものが必要
- spin.exe
- gcc.exe(多分Cコンパイラであればなんでも)
- cygwin1.dll(場合により)
- 本家サイトに行けば全部そろう
- Cygwinがインストールしてあれば楽
iSpin
- 本家が開発しているSPIN支援ツール
- xSpinの後継で、2010年12月に誕生
- それに伴いxSpinのサポートは終了らしい
- SPINの検証を楽にしてくれるツールのよう
- Promela記述を楽にはしてくれなさそう
- Editor部分はあるが、反例トレース用だと思う。Promelaをそこで書くものではなさそう
- したがって、Promela editorは別のを使うのが良い（今のところ）
- tcl/td(Active Tcl)のインストールが必要
xSpin
jSpin
- Javaで書かれたSPIN支援ツール
- 日本語が□になって打てない
- iSpinと同じでPromelaはあまり支援してくれない
ETCH : An Enhanced Type Checker for Promela
- Spinのデフォルトのよりも強力なPromelaシンタクスチェッカらしい
- 404でDownloadできなかったので未検証
- ソースコードは落とせるので、そちらからコンパイル？すればいいのかも
- なんとなく面倒になって後回し
promela-mode.el
- EmacsでPromelaを支援してくれるスクリプト
- ハイライトや自動インデント、括弧補完がある
- iSpinや何も設定してないテキストエディタでかくよりははるかに良い
- 自動インデントで若干の不満点
- 個人的にインデントはタブオンリーにしてほしい
- EclipseのプラグインでPromela/SPINを支援してくれる
- Promela記述に関してはハイライトやインデントなど補完してくれる
- SPINの検証もできるが動作がなぜか安定しない
- Promela editorとして使うのが良いかも
- vim用のPromela構文ハイライトスクリプト
- 見た感じ使えそうではあるが、vimは使っていないので未検証
オススメ
- Emacs(promela-mode.el)で書いてシェルモードでコマンドを打って検証し、複雑な検証や大きなトレースはiSpinを使う、というのがいいと思う
- Emacsを使わないのであれば、言語設定、ハイライト設定ができるエディターを使うなどの方法をとるのが良い
最終更新：2011年02月01日 13:58
