ページ更新: 2011-10-28 (金) (2936日前)

(2005-05-06作成、2010-01-13ページ移動)

目次

[編集]

情報源 #

  • 2006-02-12 Pathfinderあれこれ - 「むじん」の技術と仕事のwiki
    • 曰く『JPFは,対象のプログラムを一度(通常のVMはもちろん一度だけしか実行しません)だけでなく,理論的に可能なすべての入力によって実行を繰り返すことにより,実行経路上で潜在的に生じえるデッドロックや補足されない例外のような違反がないかどうかをチェックする. もし,このような違反を発見した場合,JPFは,どのような実行によってこの違反に達したのかという,実行経路を示す.』
[編集]

jpf-core ソースコードの入手、ビルド、exampleの実行 #

(2010-01-13)

注意:ソースコードの入手には、Mercurial(hg)が必要である。

C:> mkdir jpf
C:> cd jpf
C:> hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core
C:> cd jpf-core
C:> hg tip ★バージョンを確認

入手したファイルを最新版に更新するとき。

C:> cd jpf\jpf-core
C:> hg pull -u

ビルドする。(なお、Antを動かすために環境変数JAVA_HOMEを設定しておくこと)

cd jpf\jpf-core
bin\ant -projecthelp  ★Antが同梱されている。ターゲット一覧を表示(-projecthelp)
bin\ant test dist  ★distだけだとエラーになるので、testとdistを指定
...
build:
      [jar] Building jar: C:\Scratchjpf-projects\jpf-core\build\jpf.jar
      [jar] Building jar: C:\Scratchjpf-projects\jpf-core\build\jpf-classes.jar
      [jar] Building jar: C:\Scratchjpf-projects\jpf-core\build\jpf-annotations.jar
      [jar] Building jar: C:\Scratchjpf-projects\jpf-core\build\RunJPF.jar
      [jar] Building jar: C:\Scratchjpf-projects\jpf-core\build\RunAnt.jar

test:
    [junit] Running TypeNameTest
    [junit] Tests run: 1, Failures: 0, Errors: 0, Time elapsed: 0.5 sec
...
    [junit] Running gov.nasa.jpf.test.mc.threads.SchedulesTest
    [junit] Tests run: 1, Failures: 0, Errors: 0, Time elapsed: 0.547 sec

dist:
     [zip] Building zip: C:\Scratchjpf-projects\jpf-core\build\jpf-core.zip

BUILD SUCCESSFUL
Total time: 1 minute 17 seconds

show-check ターゲット(FindBugs) にclasspathが足りない。 このターゲットを実行したいのなら、build.xml のtaskdef name="findbugs" にclasspathを追加すること:

C:> hg diff -U0
diff -r f438b6253ee3 build.xml
--- a/build.xml Tue Jan 12 10:30:58 2010 -0800
+++ b/build.xml Wed Jan 13 21:07:03 2010 +0900
@@ -143,1 +143,2 @@
-    <taskdef name="findbugs" classname="edu.umd.cs.findbugs.anttask.FindBugsTask"/>
+    <taskdef name="findbugs" classname="edu.umd.cs.findbugs.anttask.FindBugsTask"
+             classpath="tools/findbugs-ant.jar"/>

build.xmlの修正をコミットしておく:

C:> hg commit build.xml -m "fix findbugs target (add classpath)"

C:> hg tip
changeset:   136:2373921d7ff6
tag:         tip
user:        discypus
date:        Wed Jan 13 21:22:44 2010 +0900
summary:     fix findbugs target (add classpath)

C:> hg log -l 2
changeset:   136:2373921d7ff6
tag:         tip
user:        discypus
date:        Wed Jan 13 21:22:44 2010 +0900
summary:     fix findbugs target (add classpath)

changeset:   135:f438b6253ee3
parent:      134:184a310eb218
parent:      133:b98a4345b629
user:        Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date:        Tue Jan 12 10:30:58 2010 -0800
summary:     merged in Willems change

では、jpfを実行してみる。まずは引数なしで:

C:> java -cp build\RunJPF.jar;build\jpf.jar gov.nasa.jpf.Main
Usage: "java [<vm-option>..] gov.nasa.jpf.JPF [<jpf-option>..] [<app> [<app-arg>..]]
  <jpf-option> : -help  : print usage information
               | -log   : print configuration initialization steps
               | -show  : print configuration dictionary contents
               | +<key>=<value>  : add or override key/value pair to config dictionary
  <app>        : *.jpf application properties file pathname | fully qualified application class name
  <app-arg>    : arguments passed into main() method of application class

次に、src/example/*.jpf のいずれかを指定して実行してみる:

C:> java -cp build\RunJPF.jar;build\jpf.jar gov.nasa.jpf.Main src\examples\oldclassic.jpf
JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center


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

====================================================== search started: 10/01/13 21:17
1
  2
1
  2
1
  2
1
  2
  2
  2

====================================================== error #1
gov.nasa.jpf.jvm.NotDeadlockedProperty
deadlock encountered:
  thread index=0,name=main,status=TERMINATED,this=null,target=null,priority=5,lockCount=0,suspen
dCount=0
  thread index=1,name=Thread-0,status=WAITING,this=FirstTask@295,priority=5,lockCount=1,suspendC
ount=0
  thread index=2,name=Thread-1,status=WAITING,this=SecondTask@322,priority=5,lockCount=1,suspend
Count=0


====================================================== snapshot #1
thread index=1,name=Thread-0,status=WAITING,this=FirstTask@295,priority=5,lockCount=1,suspendCou
nt=0
  waiting on: Event@290
  call stack:
        at Event.wait_for_event(oldclassic.java:79)
        at FirstTask.run(oldclassic.java:103)

thread index=2,name=Thread-1,status=WAITING,this=SecondTask@322,priority=5,lockCount=1,suspendCo
unt=0
  waiting on: Event@291
  call stack:
        at Event.wait_for_event(oldclassic.java:79)
        at SecondTask.run(oldclassic.java:130)


====================================================== trace #1
------------------------------------------------------ transition #0 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
      [2843 insn w/o sources]
  oldclassic.java:47             : Event      new_event1 = new Event();
  oldclassic.java:59             : class Event {
      [1 insn w/o sources]
  oldclassic.java:60             : int count = 0;
  oldclassic.java:47             : Event      new_event1 = new Event();
  oldclassic.java:48             : Event      new_event2 = new Event();
  oldclassic.java:59             : class Event {
      [1 insn w/o sources]
  oldclassic.java:60             : int count = 0;
  oldclassic.java:48             : Event      new_event2 = new Event();
  oldclassic.java:50             : FirstTask  task1 = new FirstTask(new_event1, new_event2);
  oldclassic.java:91             : public FirstTask (Event e1, Event e2) {
      [181 insn w/o sources]
  oldclassic.java:89             : int   count = 0;  // bad optimization - local cache of event1
 internals
  oldclassic.java:92             : this.event1 = e1;
  oldclassic.java:93             : this.event2 = e2;
  oldclassic.java:94             : }
  oldclassic.java:50             : FirstTask  task1 = new FirstTask(new_event1, new_event2);
  oldclassic.java:51             : SecondTask task2 = new SecondTask(new_event1, new_event2);
  oldclassic.java:117            : public SecondTask (Event e1, Event e2) {
      [134 insn w/o sources]
  oldclassic.java:115            : int   count = 0;  // bad optimization - local cache of event2
 internals
  oldclassic.java:118            : this.event1 = e1;
  oldclassic.java:119            : this.event2 = e2;
  oldclassic.java:120            : }
  oldclassic.java:51             : SecondTask task2 = new SecondTask(new_event1, new_event2);
  oldclassic.java:53             : task1.start();
------------------------------------------------------ transition #1 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main,Thread-0}
  oldclassic.java:53             : task1.start();
  oldclassic.java:54             : task2.start();
------------------------------------------------------ transition #2 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main,Thread-0,Thread-1}
  oldclassic.java:54             : task2.start();
  oldclassic.java:55             : }
------------------------------------------------------ transition #3 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:97             : count = event1.count;          // <race> violates event1 moni
tor encapsulation
------------------------------------------------------ transition #4 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:97             : count = event1.count;          // <race> violates event1 moni
tor encapsulation
  oldclassic.java:100            : System.out.println("1");
  oldclassic.java:102            : if (count == event1.count) { // <race> ditto
------------------------------------------------------ transition #5 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:102            : if (count == event1.count) { // <race> ditto
  oldclassic.java:103            : event1.wait_for_event();
------------------------------------------------------ transition #6 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:103            : event1.wait_for_event();
  oldclassic.java:79             : wait();
------------------------------------------------------ transition #7 thread: 2
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-1}
  oldclassic.java:123            : count = event2.count;          // <race> violates event2 moni
tor encapsulation
  oldclassic.java:126            : System.out.println("  2");
  oldclassic.java:127            : event1.signal_event();       // updates event1.count
  oldclassic.java:71             : count = (count + 1) % 3;
  oldclassic.java:74             : notifyAll();
  oldclassic.java:75             : }
  oldclassic.java:129            : if (count == event2.count) { // <race> ditto
------------------------------------------------------ transition #8 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:79             : wait();
  oldclassic.java:81             : }
  oldclassic.java:82             : }
  oldclassic.java:106            : count = event1.count;        // <race> ditto
------------------------------------------------------ transition #9 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:106            : count = event1.count;        // <race> ditto
  oldclassic.java:107            : event2.signal_event();       // updates event2.count
------------------------------------------------------ transition #10 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:107            : event2.signal_event();       // updates event2.count
  oldclassic.java:71             : count = (count + 1) % 3;
------------------------------------------------------ transition #11 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:71             : count = (count + 1) % 3;
------------------------------------------------------ transition #12 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:71             : count = (count + 1) % 3;
  oldclassic.java:74             : notifyAll();
  oldclassic.java:75             : }
  oldclassic.java:107            : event2.signal_event();       // updates event2.count
  oldclassic.java:100            : System.out.println("1");
  oldclassic.java:102            : if (count == event1.count) { // <race> ditto
------------------------------------------------------ transition #13 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:102            : if (count == event1.count) { // <race> ditto
  oldclassic.java:103            : event1.wait_for_event();
------------------------------------------------------ transition #14 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:103            : event1.wait_for_event();
  oldclassic.java:79             : wait();
------------------------------------------------------ transition #15 thread: 2
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-1}
  oldclassic.java:129            : if (count == event2.count) { // <race> ditto
  oldclassic.java:133            : count = event2.count;        // <race> ditto
  oldclassic.java:126            : System.out.println("  2");
  oldclassic.java:127            : event1.signal_event();       // updates event1.count
  oldclassic.java:71             : count = (count + 1) % 3;
  oldclassic.java:74             : notifyAll();
  oldclassic.java:75             : }
  oldclassic.java:129            : if (count == event2.count) { // <race> ditto
------------------------------------------------------ transition #16 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:79             : wait();
  oldclassic.java:81             : }
  oldclassic.java:82             : }
  oldclassic.java:106            : count = event1.count;        // <race> ditto
------------------------------------------------------ transition #17 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:106            : count = event1.count;        // <race> ditto
  oldclassic.java:107            : event2.signal_event();       // updates event2.count
------------------------------------------------------ transition #18 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:107            : event2.signal_event();       // updates event2.count
  oldclassic.java:71             : count = (count + 1) % 3;
------------------------------------------------------ transition #19 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:71             : count = (count + 1) % 3;
------------------------------------------------------ transition #20 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:71             : count = (count + 1) % 3;
  oldclassic.java:74             : notifyAll();
  oldclassic.java:75             : }
  oldclassic.java:107            : event2.signal_event();       // updates event2.count
  oldclassic.java:100            : System.out.println("1");
  oldclassic.java:102            : if (count == event1.count) { // <race> ditto
------------------------------------------------------ transition #21 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:102            : if (count == event1.count) { // <race> ditto
  oldclassic.java:103            : event1.wait_for_event();
------------------------------------------------------ transition #22 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:103            : event1.wait_for_event();
  oldclassic.java:79             : wait();
------------------------------------------------------ transition #23 thread: 2
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-1}
  oldclassic.java:129            : if (count == event2.count) { // <race> ditto
  oldclassic.java:133            : count = event2.count;        // <race> ditto
  oldclassic.java:126            : System.out.println("  2");
  oldclassic.java:127            : event1.signal_event();       // updates event1.count
  oldclassic.java:71             : count = (count + 1) % 3;
  oldclassic.java:74             : notifyAll();
  oldclassic.java:75             : }
  oldclassic.java:129            : if (count == event2.count) { // <race> ditto
------------------------------------------------------ transition #24 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:79             : wait();
  oldclassic.java:81             : }
  oldclassic.java:82             : }
  oldclassic.java:106            : count = event1.count;        // <race> ditto
------------------------------------------------------ transition #25 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:106            : count = event1.count;        // <race> ditto
  oldclassic.java:107            : event2.signal_event();       // updates event2.count
------------------------------------------------------ transition #26 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:107            : event2.signal_event();       // updates event2.count
  oldclassic.java:71             : count = (count + 1) % 3;
------------------------------------------------------ transition #27 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:71             : count = (count + 1) % 3;
------------------------------------------------------ transition #28 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:71             : count = (count + 1) % 3;
  oldclassic.java:74             : notifyAll();
  oldclassic.java:75             : }
  oldclassic.java:107            : event2.signal_event();       // updates event2.count
  oldclassic.java:100            : System.out.println("1");
  oldclassic.java:102            : if (count == event1.count) { // <race> ditto
------------------------------------------------------ transition #29 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:102            : if (count == event1.count) { // <race> ditto
  oldclassic.java:103            : event1.wait_for_event();
------------------------------------------------------ transition #30 thread: 2
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {Thread-0,>Thread-1}
  oldclassic.java:129            : if (count == event2.count) { // <race> ditto
  oldclassic.java:133            : count = event2.count;        // <race> ditto
------------------------------------------------------ transition #31 thread: 2
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {Thread-0,>Thread-1}
  oldclassic.java:133            : count = event2.count;        // <race> ditto
  oldclassic.java:126            : System.out.println("  2");
  oldclassic.java:127            : event1.signal_event();       // updates event1.count
------------------------------------------------------ transition #32 thread: 2
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {Thread-0,>Thread-1}
  oldclassic.java:127            : event1.signal_event();       // updates event1.count
  oldclassic.java:71             : count = (count + 1) % 3;
  oldclassic.java:74             : notifyAll();
  oldclassic.java:75             : }
  oldclassic.java:129            : if (count == event2.count) { // <race> ditto
------------------------------------------------------ transition #33 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0,Thread-1}
  oldclassic.java:103            : event1.wait_for_event();
  oldclassic.java:79             : wait();
------------------------------------------------------ transition #34 thread: 2
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-1}
  oldclassic.java:129            : if (count == event2.count) { // <race> ditto
  oldclassic.java:130            : event2.wait_for_event();
  oldclassic.java:79             : wait();

====================================================== results
error #1: gov.nasa.jpf.jvm.NotDeadlockedProperty "deadlock encountered:    thread index=0,name=m
ain,..."

====================================================== statistics
elapsed time:       0:00:00
states:             new=38, visited=3, backtracked=6, end=1
search:             maxDepth=34, constraints=0
choice generators:  thread=38, data=0
heap:               gc=33, new=311, free=11
instructions:       3583
max memory:         122MB
loaded code:        classes=76, methods=1015

====================================================== search finished: 10/01/13 21:17

インストールは、build/jpf-core.zip を展開してパスを通す。

「jpf.bat TestExample.jpf」の用にすれば、jpfを実行してコードを検査することが出来る。

[編集]

ディレクトリのレイアウトと設定ファイル site.properties (2010-01-19) #

jpfのファイルをあるディレクトリ (以下$JPF_HOMEとする) に置く場合は、次のように配置する:

$JPF_HOME/
  jpf-core/
  jpf-shell/
  ...

設定ファイルsite.propertiesは、ホームディレクトリ(以下$HOMEとする)の.jpfディレクトリの直下に置く:

$HOME/
  .jpf/
    site.properties

なお、この$HOMEの位置を調べるには、Javaで「System.out.println(System.getProperty("user.home"));」を実行する。

site.properteis の例を以下に示す。仮に $JPF_HOME = c:\java\jpf とし、jpf-core と jpf-shell を用いている:

#JPF site configuration
# Windows users need to specify the full path through their own directory system
# Note for Vista and Windows 7 users there will not be a Documents and Settings
# instead there will be a Users. 

jpf.home = c:/java/jpf

#can only expand system properties at this point
jpf-core = ${jpf.home}/jpf-core

#symbolic execution extension
#jpf-symbc = ${jpf.home}/jpf-symbc

#concurrent extension
#jpf-concurrent = ${jpf.home}/jpf-concurrent

#Shell extention
jpf-shell = ${jpf.home}/jpf-shell
extensions+=,${jpf-shell}
[編集]

メモ #

[編集]

DiningPhil.jpf の結果 #

食事する哲学者の問題 - Wikipedia

C:> java -cp build\RunJPF.jar;build\jpf.jar gov.nasa.jpf.Main src\examples\DiningPhil.jpf
BFS Search
JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center


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

====================================================== search started: 10/01/13 21:31

====================================================== error #1
gov.nasa.jpf.jvm.NotDeadlockedProperty
deadlock encountered:
  thread index=0,name=main,status=TERMINATED,this=null,target=null,priority=5,lockCount=0,suspen
dCount=0
  thread index=1,name=Thread-0,status=BLOCKED,this=DiningPhil$Philosopher@306,priority=5,lockCou
nt=0,suspendCount=0
  thread index=2,name=Thread-1,status=BLOCKED,this=DiningPhil$Philosopher@330,priority=5,lockCou
nt=0,suspendCount=0
  thread index=3,name=Thread-2,status=BLOCKED,this=DiningPhil$Philosopher@336,priority=5,lockCou
nt=0,suspendCount=0
  thread index=4,name=Thread-3,status=BLOCKED,this=DiningPhil$Philosopher@342,priority=5,lockCou
nt=0,suspendCount=0
  thread index=5,name=Thread-4,status=BLOCKED,this=DiningPhil$Philosopher@361,priority=5,lockCou
nt=0,suspendCount=0
  thread index=6,name=Thread-5,status=BLOCKED,this=DiningPhil$Philosopher@367,priority=5,lockCou
nt=0,suspendCount=0


====================================================== snapshot #1
thread index=1,name=Thread-0,status=BLOCKED,this=DiningPhil$Philosopher@306,priority=5,lockCount
=0,suspendCount=0
  owned locks:DiningPhil$Fork@297
  blocked on: DiningPhil$Fork@298
  call stack:
        at DiningPhil$Philosopher.run(DiningPhil.java:42)

thread index=2,name=Thread-1,status=BLOCKED,this=DiningPhil$Philosopher@330,priority=5,lockCount
=0,suspendCount=0
  owned locks:DiningPhil$Fork@298
  blocked on: DiningPhil$Fork@299
  call stack:
        at DiningPhil$Philosopher.run(DiningPhil.java:42)

thread index=3,name=Thread-2,status=BLOCKED,this=DiningPhil$Philosopher@336,priority=5,lockCount
=0,suspendCount=0
  owned locks:DiningPhil$Fork@299
  blocked on: DiningPhil$Fork@300
  call stack:
        at DiningPhil$Philosopher.run(DiningPhil.java:42)

thread index=4,name=Thread-3,status=BLOCKED,this=DiningPhil$Philosopher@342,priority=5,lockCount
=0,suspendCount=0
  owned locks:DiningPhil$Fork@300
  blocked on: DiningPhil$Fork@301
  call stack:
        at DiningPhil$Philosopher.run(DiningPhil.java:42)

thread index=5,name=Thread-4,status=BLOCKED,this=DiningPhil$Philosopher@361,priority=5,lockCount
=0,suspendCount=0
  owned locks:DiningPhil$Fork@301
  blocked on: DiningPhil$Fork@302
  call stack:
        at DiningPhil$Philosopher.run(DiningPhil.java:42)

thread index=6,name=Thread-5,status=BLOCKED,this=DiningPhil$Philosopher@367,priority=5,lockCount
=0,suspendCount=0
  owned locks:DiningPhil$Fork@302
  blocked on: DiningPhil$Fork@297
  call stack:
        at DiningPhil$Philosopher.run(DiningPhil.java:42)


====================================================== results
error #1: gov.nasa.jpf.jvm.NotDeadlockedProperty "deadlock encountered:    thread index=0,name=m
ain,..."

====================================================== statistics
elapsed time:       0:00:03
states:             new=6308, visited=16508, backtracked=22815, end=1
search:             maxDepth=13, constraints=0
choice generators:  thread=5155, data=0
heap:               gc=22828, new=352, free=25170
instructions:       151983
max memory:         218MB
loaded code:        classes=81, methods=1299

====================================================== search finished: 10/01/13 21:31