情報科学屋さんを目指す人のメモ(FC2ブログ版)

何かのやり方や、問題の解決方法をどんどんメモするブログ。そんな大学院生の活動「キャッシュ」に誰かがヒットしてくれることを祈って。

ブログ内検索

スポンサーサイト このエントリーを含むはてなブックマーク

上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

スポンサー広告 | 編集
このエントリーをはてなブックマークに追加 Clip to Evernote

Java Pathfinder(JPF)のインストール手順詳細 このエントリーを含むはてなブックマーク

Java Pathfinder はJava用のモデル検査ツールで、実行することなくデッドロックが発生するスレッドの実行順序を発見したり、例外の発生する可能性を検出することが出来ます。

このJava Pathfinderはインストールがすこし面倒なので、インストールしたときのメモを公開しておきます。

Java PathfinderのWebページ

トップページ:http://babelfish.arc.nasa.gov/trac/jpf
Getting and Installing JPF:http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/start

ポイント

ソースコードのダウンロードにMercurialを利用します。JPFのソースコードを取得後ビルドし、Eclipse用のプラグインをインストールしてEclipseから簡単に実行できるようにします。そして、サンプルの実行までを行います。

今回使用したOSはWindows。Java開発にEclipseを利用することを想定。すでにインストールしてある項目はスキップしてください。

Java実行環境(JRE)をインストール

インストール済みだと思いますが、インストールしてない場合はここからインストール:http://www.oracle.com/technetwork/java/javase/downloads/index.html

Eclipseをダウンロード&インストール

こちらもインストールしていなければインストールしてください:http://www.eclipse.org/downloads/

Mercurial Eclipseプラグインをインストール

http://javaforge.com/project/HGE

このページに「How can I download the plugin?」という部分があり、そこに説明があります。以下、そのやり方。

まず、Eclipseで「Help>Install New Software」から「Add...」ボタンを押す。

「Name:」に「MercurialEclipse」、「Location:」に「http://cbes.javaforge.com/update」と入力して「OK」

少し待つと、

  • codeBeamer Eclipse Studio (with Mylyn)
  • MercurialEclipse
  • MercurialEclipse with codeBeamer Eclipse Studio

が表示されるので「MercurialEclipse」のみにチェックを入れて「Next」。

Calculating requirements and dependencies(依存関係の解決)に結構時間がかかるので待つ。

Install Detailsとして

  • MercurialEclipse
  • Windows Binaries for Mercurial (Recommended)

が表示される(環境によって変わる)ので、「Next」を押す。

Licensesを読んで「I accept the terms of the license agreements」にチェックを入れて「Finish」。

Installing Softwareがしばらく表示されるので待機し、Security Warningが表示されたら「OK」を押す。そして、「You will need to restart Eclipse for...」が表示されたら「Restart Now」で再起動する。

JPFのソースコードを入手する

「File>Import...」から「Mercurial>Clone Existing Mercurial Repository」を選択して「Next」。

「Repository location】の「URL」に「http://babelfish.arc.nasa.gov/hg/jpf/jpf-core」を入力し、「Checkout as a project(s) in the workspace」にチェックを入れて、「Next」を押して待機します。

「Select working directory revision」が表示されたら、そのまま「Next」。ちなみに、今回はRevision 415。

「Import Projects」が表示されたら、「Finish」を押して完了。すると、Project Explorerに「jpf-core」というプロジェクトが追加されているはずです。

この時点で自動ビルドによって

BUILD FAILED
(...)\workspace\jpf-core\build.xml:52: no javac was found __or__ check http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/build for possible solutions


Total time: 3 seconds

と表示されますが、特に問題ありません。

site.propertiesファイルを作る

このままだと、後々サンプル実行時に

site.properties file: "C:\Users\(ユーザ名)\.jpf\site.properties" does not exist.

と表示されてしまいます。そこで、ここで指摘されているファイルの作成を行います。

今回作るファイルは「<user.home>\.jpf\site.properties」です。user.homeは、「Help>」の、「Installation Details」にある「Configuration」の中を探すことにより知ることが出来ます。私の場合は「user.home=C:\Users\(ユーザ名)」でした。なので、他の環境でもユーザ名を置き換えただけになると思われます。

「(user.home)\.jpf」というフォルダを作り、「site.properties」というファイルを作成し、中に

jpf-core = D:/path-to-workspace/workspace/jpf-core

と書きます。path-to-workspaceは、workspaceフォルダへのパスのことを意味します。

Windowsの場合、フォルダの区切りはバックスラッシュ(または円マーク)ですが、Java Propertyの仕組みにしたがって、バックスラッシュ(\)ではなくスラッシュ(/)を使ってください。

ここで注意ですが、「.jpf」のようなドットで始まるフォルダは、エクスプローラーから作ろうとすると「ファイル名を入力してください」というエラーになってしまうので、コマンドプロンプトから

mkdir ".jpf"

などとして作った方が良さそうです。

JAVA_HOMEを設定する

Eclipseで通常ビルドする場合は不要ですが、JPFを使う際に必要になります。

「Win+Pause」から「システム」を表示し、「システムの詳細設定」を開きます。「詳細設定>環境変数」の「システム環境変数>新規」を押します。「新しいシステム変数」に、変数名として「JAVA_HOME」、変数値として「C:\Program Files(x86)\Java\jdk1.6.0_20」(JDKまたはJREのある場所を指定する)として、設定を有効化するために一旦再起動します。

ビルドする

build.xmlを右クリックして、「Run As>Ant Build」を押します。

Buildfile: (...)\workspace\jpf-core\build.xml
-cond-clean:
-init:
-compile-annotations:
-compile-main:
-compile-peers:
-compile-classes:
-compile-tests:
-compile-examples:
compile:
build:
    [jar] Building jar:(...)\workspace\jpf-core\build\jpf.jar
BUILD SUCCESSFUL

Total time: 2 seconds

こんなものが表示されて成功です。

JPF pluginをインストール

MercurialEclipseプラグインをインストールしたときと同様に

  • Name:JPFplugin
  • Location:http://babelfish.arc.nasa.gov/trac/jpf/raw-attachment/wiki/install/eclipse-plugin/update/

と入力して「Eclipse-JPF」にチェックを入れて先に進めば、インストールできます。

サンプルの実行

jpf-coreプロジェクトの「jpf-core/src/examples」の中にある.jpfファイルがサンプルファイルです。たくさんあります。

たとえばHelloWorld.jpfを右クリックして「Verify...」をクリックすると、

Executing command: java -jar (...)\workspace\jpf-core\src\examples\HelloWorld.jpf 
JavaPathfinder v6.0 - (C) RIACS/NASA Ames Research Center


====================================================== system under test
application: HelloWorld.java

====================================================== search started: 11/01/01 0:00
I won't say it!

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       0:00:00
states:             new=1, visited=0, backtracked=0, end=1
search:             maxDepth=1, constraints hit=0
choice generators:  thread=1 (signal=0, lock=1, shared ref=0), data=0
heap:               new=319, released=11, max live=319, gc-cycles=1
instructions:       2900
max memory:         122MB
loaded code:        classes=74, methods=915


====================================================== search finished: 11/01/01 0:00

のように実行結果が表示されます。

サンプルについて

Dining philosopher問題など、他にもいろいろなサンプルがあるので、試してみると「へー」となれます。

まとめ

余り大規模なプログラム向けではないそうなのですが、実際こういう方法でテストできるということが体感できて面白いです。

Java | コメント:0 | トラックバック:0 | 編集
このエントリーをはてなブックマークに追加 Clip to Evernote

この記事のコメント

コメントの投稿 エントリの新旧に関わらず、極力18時間中に返信します。














この記事のトラックバック

トラックバックURL:
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。