モデル検査器ProB（フリー＆オープンソース、Windows版、FDRスクリプト対応）のインストール方法を説明します。
（FDR, JCSPのインストール方法はこちらをご覧ください）
[概要]
ProBはBとCSPのモデル検査器で、CSPモデルはFDRと互換性があります（若干の違いはあります）。フリーかつオープンソース（EPL v1.0 license）で、Windows版もあります。FDRを使えない方はProBを試してみてください。商用サポートは FormalMind から受けることもできます。
[基本情報]
開発元: Heinrich-Heine-Universität Düsseldorf
バージョン: 1.3.6 （2013年4月2日現在）
備考: ライセンスは EPL v1.0 license （詳細はこちら）
[インストール手順]
Windows版ProBのインストール方法を説明します。詳しくはこちらを読んでください。ProBを実行するには、次のソフトウェアもインストール必要があります。
Tcl/Tk 8.5 for Windows
Java Runtime Environment （5.0以降）
GraphViz （オプション）
1. Tcl/Tk 8.5 のインストール
現在、Tcl/Tk 8.6もリリースされていますが、8.6 はProBでサポートされていないので 8.5 をインストールしてください。Tcl/Tk 8.5.13 は下記のサイトからダウンロードできます。
http://downloads.activestate.com/ActiveTcl/releases/8.5.13.0/
Windows(32bit)であれば、実行ファイル
ActiveTcl8.5.13.0.296436-win32-ix86-threaded.exe
を適当なフォルダにダウンロードします。ダウンロードしたファイルをダブルクリックで実行し、ライセンス同意、フォルダの指定をして、インストールを完了します（基本的にはデフォルトでOK）。
2. Java Runtime Environment （5.0以降）のインストール
Javaは下記のサイトからダウンロードできます。
Javaのインストール方法は様々なサイトで紹介されているので、そちらを参考にしてください。
3. GraphVizのインストール
ProBで解析した状態遷移図を表示するためにGarphVizを使う場合はインストールします。GarphVizのサイト
からDownloadのページに進み、一番下の[Agree]でライセンスに同意します。その次のページで、Executable Package from AT&T からOSに合うファイルを選択します。Windows ならば
windows
Stable and development Windows Install packages
をクリックします。GraphVizの安定版
current stable release
graphviz-2.30.1.msi （2013/04/02現在）
を選択してダウンロードします。このmsiファイルをダブルクリックして実行し、フォルダの指定をして、インストールを完了します（基本的にはデフォルトでOK）。
4. ProBのインストール
ProBのダウンロードサイトからOSにあう最新のファイルを選択します。Windows版であれば、
1.3.6-final Windows Zipfile (with probcli) [ProB.windows.zip] （2013年4月2日現在）
のファイルをダウンロードします。ダウンロードした ProB.windows.zip を解凍し、ProBフォルダのなかのProBWin.exe をダブルクリックすると ProBが起動します。
[動作確認]
並行システムの検証と実装のProB用のサンプルコードをここからダウンロードし、解凍してください。
ProBWin.exe をダブルクリックしてProBを起動します。
ProBのメインメニューから[File]→[Open]を選択し、解凍したサンプル01sampleのなかの、SR.csp を開きます（ProbB-main.jpg）。
ProBのメインメニューから[Verify]→[Check CSP-M assertions] を選択すると、検証用のサブウィンドウが開きます（この使い方はFDRに似ています）
検証用サブウィンドウの[List of CSP Assertions]のなかから検証したい詳細化関係をダブルクリックします。例えば、
? SRsec(2) [FD= SRconc
をダブルクリックすると、左端の?が✔に変わります。これは検証が成功し、その結果が真であることを表しています（ProB-veri.jpg）。
ProBのメインウィンドウに戻り、メインメニューから [Animate]→[View StateSpace]を選択すると、サブウィンドウに状態遷移図が表示されます（ProB-graph.jpg）。
状態遷移図が表示されない場合は次のことを確認してください。
Graphvizはインストールされてますか？ （コマンドプロンプトから dot -V で確認）
ProBのメインメニュー[Preference]→[Graphical Viewer]で Dot Viewer が選択されていますか？
[注意]
ProBで読み込むFDRスクリプトの拡張子は.fdr2ではなく.cspにしてください。.fdr2でも読み込めますが、CSPモデルと認識されないためエラーになります。