[Javapathfinder-user] Problem in the first try of JPF

[ZHU H. <ry...@us...>]

Dear Sir or madam,

I tried the example in
http://javapathfinder.sourceforge.net/sw_model_checking.html
I typied "java gov.nasa.jpf.JPF Rand_test" and "bin\jpf Rand_test", both
came to an error like this:

F:\HKUST\recrash\jpf>java gov.nasa.jpf.JPF Rand_test

java.lang.UnsatisfiedLinkError: sun.misc.Unsafe.registerNatives (no peer)
        at sun.misc.Unsafe.<clinit>(sun\misc\Unkown:0)
        at
java.util.concurrent.atomic.AtomicLong.<clinit>(java\util\concurrent\
atomic\Unkown:0)
        at java.util.Random.<init>(java\util\Unkown:10)
        at Rand_test.main(Rand_test.java:5)

----------------------------------- path to error (length: 1)
Transition #0 Thread #0
  Rand_test.java:5               Random random = new Random(42);      // (1)
  [no source for: java\util\Unkown]
  [no source for: java\lang\Object.java]
  [no source for: java\util\Unkown]
  [no source for: java\util\concurrent\atomic\Unkown]
  [no source for: sun\misc\Unkown]
------------------------------------ end error path

------------------------------------ thread stacks
Thread: main
        at sun.misc.Unsafe.<clinit>(sun\misc\Unkown:0)
        at
java.util.concurrent.atomic.AtomicLong.<clinit>(java\util\concurrent\
atomic\Unkown:0)
        at java.util.Random.<init>(java\util\Unkown:10)
        at Rand_test.main(Rand_test.java:5)

------------------------------------ end thread stacks


===================================
  1 Error Found: uncaught exception
===================================


Is the problem caused by the lack of the libraries? How can I fix this?
Thank you.

Best regards
ZHU Hua