Symbolic Path Finder のセットアップ手順

標準

JAVA言語のシンボリック実行ツールであるSymbolic Path Finder(以下SPF)のセットアップ手順を説明します。

対象はWindowsおよびLinuxですが、筆者の環境で確認したものは、Ubuntu, Windows7 64bit, Windows8 64bit です。


JPF Pluginのインストール

 

eclipseから JPF を実行するため、Pluginをインストールします。手順は Mercurial Plugin のインストールと同様です。
Locationに下記を指定します:
http://babelfish.arc.nasa.gov/trac/jpf/raw-attachment/wiki/projects/eclipse-jpf/update

JPFの設定ファイル(site.properties)の作成

  • <user.home>配下に .jpf フォルダを作成します。
    ※ user.homeは、「Help>」->「Installation Details」->「Configuration」の中に記載があります。
    筆者の場合は「user.home=C:\Users\(ユーザ名)」です。
    ※ . (ドット) で始まるフォルダはGUIからは作成できないので、コマンドプロンプトから mkdir を使って作成してください。
  • .jpf フォルダ に site.properties ファイルを作成します。
  • 作ったファイルに下記を記載します:
    ※ jpf-coreフォルダがある場所を指定します。フォルダ区切りは / (スラッシュ)なのでご注意。

    jpf-coreのダウンロードとビルド

eclipse経由でMercurialレポジトリからjpf-core (JPFを動作させるための最小構成)をダウンロードします。

  1. File -> Import -> Mercurial -> Clone repository using Mercurial -> Next を選択します。
  2. Repository Locationに http://babelfish.arc.nasa.gov/hg/jpf/jpf-core を指定します。
  3. Next を押します。
    => jpf-coreのダウンロードが始まります。
  4. 画面にしたがってNextを押していきます。
    => Package Explorer に jpf-core が表示されます。
  5. 同時にjpf-coreのBuildが走ります。
    => Consoleに BUILD SUCCESSFUL と表示されます※ eclipse でダウンロードに失敗した場合は、ターミナルから直接ダウンロードしてみます。
    eclipse の workspace に移動し、以下のコマンドを実行します

    => jpf-core フォルダにファイルがダウンロードされます。
    – eclipse の project に jpf-core を登録します。
    File -> Import -> Mercurial -> Projects from local mercurial repository -> Next を選択します。
    – jpf-core フォルダがある場所を指定します。
    => Package Explorer に jpf-core が表示されます。
    – 同時にjpf-coreのBuildが走ります。
    => Consoleに BUILD SUCCESSFUL と表示されます。

    Mercurial Pluginのインストール

eclipse経由で JPF のソースをMercurialレポジトリからダウンロードするため、Mercurial Pluginをインストールします。

  • Windowsの場合、インストール手順は下記を参照してください:
    http://d.hatena.ne.jp/absj31/20120713/1342235177
    ※ 手順では codeBeamer も入れていますが、MercurialEclipse だけで大丈夫です。
  • Linuxの場合も上記と同様ですが、インストール対象から、”Mercurial Windows Binary” を外します。

    Mercurial のインストール(Linuxのみ)

    eclipse経由で JPF のソースをMercurialレポジトリからダウンロードするため、Mercurial 本体をインストールします。

ターミナルから以下のコマンドを実行します

eclipseのインストール

  • 下記のページよりWindows 32bit版eclipseまたはLinux x68版をダウンロードします。
    https://eclipse.org/downloads/
    ※ JDKが32bit版なので、eclipseも32bit版にします。64bit版を入れても動きませんのでご注意
  • Windowsの場合、解凍したフォルダを適当な場所(例:C:\Program Files (x86)\)に置き、eclipse.exeを実行してみます。
    => 起動することを確認します。
    なお、Eclipse Luna (4.4.1) で動作確認しています。
  • Linuxの場合、解凍したフォルダを適当な場所に置き、ターミナルから eclipse を実行します。
    なお、Eclipse 3.8 で動作確認しています。

Java Path Finderのインストール

  • JDK のインストール(windows, Linux共通)
    • 下記のページよりWindows x86版JDKをインストールします。(jdk-****-windows-i586.exe)
      ※ JRE ではなく JDK なのでご注意。(Javac コンパイラが必要なため)
      http://www.oracle.com/technetwork/java/javase/downloads/index-jsp-138363.html#javasejdk
      なお、v8_25 で動作確認しています。
  • 環境変数JAVA_HOMEの設定 (windows, Linux共通)
    • Windows(Linux)環境変数にJAVA_HOMEを追加します。
    • 変数値に、JDKのインストール先フォルダまでのパスを設定します。
      例) C:\Program Files (x86)\Java\jdk1.8.0_25

動作確認

Package Explorer から、jpf-core/src/examples を選択し、
.jpf という拡張子のファイル(例:BoundedBuffer.jpf)を右クリック -> Verify… を選択します。
=> JPF が実行され、Console に結果が表示されればOKです。

Symbolic Path Finder のインストール

無事JPFがインストールできたら、いよいよSPFのインストールを行います。
※ インストール手順は http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc の情報にもとづきます。

  • JPFの設定ファイル(site.properies) の追記
    ファイルに下記を追記します:
  • jpf-symbc のダウンロード
    jpf-core と同様の手順で jpf-symbc をダウンロードします。
    Repository Location に http://babelfish.arc.nasa.gov/hg/jpf/jpf-symbc を指定します。
  • SPFのビルド
    Package Explorer から jpf-symbc -> build.xml を右クリックし、Run As -> Ant Build を選択します。
    => ビルドが始まります。 BUILD SUCCESSFUL と表示されたらOKです。
  • 動作確認
    Package Explorer から src/examples/demo を選択し、
    .jpf という拡張子のファイル(例:NumericExample.jpf)を右クリック -> Verify… を選択します。
    => SPF が実行され、Console に結果が表示されればOKです。

以上でインストールは完了です。お疲れさまでした!


コメントを残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です

次のHTML タグと属性が使えます: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code class="" title="" data-url=""> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong> <pre class="" title="" data-url=""> <span class="" title="" data-url="">