SPIN環境


※上記の広告は60日以上更新のないWIKIに表示されています。更新することで広告が下部へ移動します。

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

  • iSpinに代わる
  • が、まだ使えると思う


jSpin

  • Javaで書かれたSPIN支援ツール
  • 日本語が□になって打てない
  • iSpinと同じでPromelaはあまり支援してくれない


ETCH : An Enhanced Type Checker for Promela

  • Spinのデフォルトのよりも強力なPromelaシンタクスチェッカらしい
  • 404でDownloadできなかったので未検証
    • ソースコードは落とせるので、そちらからコンパイル?すればいいのかも
    • なんとなく面倒になって後回し


promela-mode.el

  • EmacsでPromelaを支援してくれるスクリプト
  • ハイライトや自動インデント、括弧補完がある
    • iSpinや何も設定してないテキストエディタでかくよりははるかに良い
    • 自動インデントで若干の不満点
    • 個人的にインデントはタブオンリーにしてほしい


Eclipse plug-in for Spin

  • EclipseのプラグインでPromela/SPINを支援してくれる
  • Promela記述に関してはハイライトやインデントなど補完してくれる
  • SPINの検証もできるが動作がなぜか安定しない
  • Promela editorとして使うのが良いかも


Promela syntax highlighting for vim

  • vim用のPromela構文ハイライトスクリプト
  • 見た感じ使えそうではあるが、vimは使っていないので未検証


オススメ

  • Emacs(promela-mode.el)で書いてシェルモードでコマンドを打って検証し、複雑な検証や大きなトレースはiSpinを使う、というのがいいと思う
  • Emacsを使わないのであれば、言語設定、ハイライト設定ができるエディターを使うなどの方法をとるのが良い
    • そういうEditorがあるのかは知らない…