javapathfinder-user — usage related topics (installing, running, options, output...)

[Javapathfinder-user] Help with NullPpointerException

[Brandon M <bm...@ya...>]

I can successfully run bin/jpf against
examples/HelloWorld.java, with no problems.  I am now
attempting to run jpf against some of my own class
files.  I am getting a NullPointerException each time
I run jpf <myClassName>.  Below is the stack trace,
along with my parameter settings:

STACK TRACE
===========
JPF exception, terminating: class
java.lang.NullPointerException: null

java.lang.NullPointerException
        at
gov.nasa.jpf.jvm.ElementInfo.checkFieldInfo(ElementInfo.java:462)
        at
gov.nasa.jpf.jvm.ElementInfo.getIntField(ElementInfo.java:471)
        at
gov.nasa.jpf.jvm.bytecode.GETSTATIC.execute(GETSTATIC.java:41)
        at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1490)
        at
gov.nasa.jpf.jvm.ThreadInfo.executeMethod(ThreadInfo.java:1522)
        at
gov.nasa.jpf.jvm.ClassInfo.initializeClass(ClassInfo.java:665)
        at
gov.nasa.jpf.jvm.StaticArea.newClass(StaticArea.java:160)
        at
gov.nasa.jpf.jvm.StaticArea.get(StaticArea.java:62)
        at
gov.nasa.jpf.jvm.ClassInfo.getClassObjectRef(ClassInfo.java:368)
        at
gov.nasa.jpf.jvm.bytecode.INVOKESTATIC.isSchedulingRelevant(INVOKESTATIC.java:102)
        at
gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2126)
        at
gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1546)
        at
gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:268)
        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:997)
        at
gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)
        at
gov.nasa.jpf.search.DFSearch.search(DFSearch.java:84)
        at gov.nasa.jpf.JPF.run(JPF.java:308)
        at gov.nasa.jpf.JPF.main(JPF.java:238)
java.lang.NullPointerException
        at
gov.nasa.jpf.jvm.ElementInfo.checkFieldInfo(ElementInfo.java:462)
        at
gov.nasa.jpf.jvm.ElementInfo.getIntField(ElementInfo.java:471)
        at
gov.nasa.jpf.jvm.bytecode.GETSTATIC.execute(GETSTATIC.java:41)
        at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1490)
        at
gov.nasa.jpf.jvm.ThreadInfo.executeMethod(ThreadInfo.java:1522)
        at
gov.nasa.jpf.jvm.ClassInfo.initializeClass(ClassInfo.java:665)
        at
gov.nasa.jpf.jvm.StaticArea.newClass(StaticArea.java:160)
        at
gov.nasa.jpf.jvm.StaticArea.get(StaticArea.java:62)
        at
gov.nasa.jpf.jvm.ClassInfo.getClassObjectRef(ClassInfo.java:368)
        at
gov.nasa.jpf.jvm.bytecode.INVOKESTATIC.isSchedulingRelevant(INVOKESTATIC.java:102)
        at
gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2126)
        at
gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1546)
        at
gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:268)
        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:997)
        at
gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)
        at
gov.nasa.jpf.search.DFSearch.search(DFSearch.java:84)
        at gov.nasa.jpf.JPF.run(JPF.java:308)
        at gov.nasa.jpf.JPF.main(JPF.java:238)
gov.nasa.jpf.JPFException: class
java.lang.NullPointerException: null
        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1040)
        at
gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)
        at
gov.nasa.jpf.search.DFSearch.search(DFSearch.java:84)
        at gov.nasa.jpf.JPF.run(JPF.java:308)
        at gov.nasa.jpf.JPF.main(JPF.java:238)


CONFIGURATION SETTINGS
======================
----------- dictionary contents
branch_start = 1
d0threshold.class =
gov.nasa.jpf.jvm.DoubleThresholdGenerator
d0threshold.high = 1.0
d0threshold.low = -1.0
d0threshold.threshold = 0.0
jpf.basedir = C:\Temp\jpf_release\bin\..
jpf.print_exception_stack = true
jpf.version = 3.1.2
log.level = warning
search.class = gov.nasa.jpf.search.DFSearch
search.error_path = error.xml
search.heuristic.branch.count_early = true
search.heuristic.branch.no_branch_return = -1
search.heuristic.class =
gov.nasa.jpf.search.heuristic.BFSHeuristic
search.heuristic.comparator.class =
gov.nasa.jpf.search.heuristic.DefaultComparator
search.heuristic.queue_limit = -1
search.match_depth = false
search.min_free = 1M
search.multiple_errors = false
search.print_errors = true
search.properties =
gov.nasa.jpf.jvm.NotDeadlockedProperty:gov.nasa.jpf.jvm.NoAssertionViolatedProperty:gov.nasa.jpf.jvm
.NoUncaughtExceptionsProperty
vm.atomic_init = true
vm.attributor.class =
gov.nasa.jpf.jvm.DefaultAttributor
vm.bootclasspath =
C:\Temp\jpf_release\bin\../build/env/jpf
vm.check_fp = false
vm.check_fp_compare = true
vm.class = gov.nasa.jpf.jvm.JVM
vm.classpath = build/env/jpf;test
vm.enable_assertions = *
vm.finalize = true
vm.gc = true
vm.halt_on_throw = false
vm.path_output = false
vm.por = true
vm.por.field_boundaries = true
vm.por.fieldlockinfo.class =
gov.nasa.jpf.jvm.StatisticFieldLockInfo
vm.por.sync_detection = true
vm.report.printStacks = true
vm.report.show_bytecode = false
vm.report.show_missing_lines = false
vm.report.show_steps = true
vm.scheduler.class = gov.nasa.jpf.jvm.DefaultScheduler
vm.scheduler.random_seed = 0
vm.scheduler.use_time_for_seed = false
vm.sourcepath =
C:\Temp\jpf_release\bin\../src:C:\Temp\jpf_release\bin\../examples:C:\Temp\jpf_release\bin\../test
vm.storage.class = gov.nasa.jpf.jvm.Md5StateSet
vm.tree_output = true
vm.verify.ignore_path = true
vm.visible_asserts = false
----------- free arguments

Any suggestions on what I may be doing wrong?


		
__________________________________ 
Yahoo! FareChase: Search multiple travel sites in one click.
http://farechase.yahoo.com

[Javapathfinder-user] Use java pathfinder in Eclipse

[harry h. <har...@ho...>]

Hi,

I am a new user of java PathFinder. I download the Java pathfinder and 
install it on the Eclipse. But How can I use the java pathfinder in the 
Eclipse environment to verfiy my program. For instance, how to verifiy the 
simple class -- HelloWorld.class in the examples directory ?

Thanks,
Harry

Re: [Javapathfinder-user] CVS out?

[Muhammad A. S. <muh...@gm...>]

> >
> > Run "dos2unix" to fix the CR/LF issue.
> >
> > Somebody with CVS access rights, please fix the release or remove it!
>
> I think the problem is that I created the relase zip under Windows and
> Eclipse is set to convert the line feeds.
>
> I can try it again with this off, but this assumes the problem is not
> also in the repository.
>

Yes, the problem is not with the repository (only with the release). I
can test it on Linux (and Sun Solaris as well, if required).

/Ali
--
Dependable Computer Systems
Chalmers University of Technology
Sweden

Re: [Javapathfinder-user] CVS out?

[John P. <joh...@na...>]

Muhammad Ali Shah wrote:
>>to fix the latest stable release (which I was able to download) so
>>that it doesn't fail on Linux with:
>>
>>dusty:JPF $ bin/jpf -show
>>: bad interpreter: No such file or directory
> 
> Run "dos2unix" to fix the CR/LF issue.
> 
> Somebody with CVS access rights, please fix the release or remove it!

I think the problem is that I created the relase zip under Windows and 
Eclipse is set to convert the line feeds.

I can try it again with this off, but this assumes the problem is not 
also in the repository.

Who can test it for me on unix?

jp


-- 
John Penix PhD. john.penix+nasa.gov http://ase.arc.nasa.gov/jpenix/
Robust Software Engineering Group  ph:(650)604-6576 bld:N296 rm:268
Intelligent Systems Division  NASA Ames Research Center  Mt.View CA

Re: [Javapathfinder-user] CVS out?

[Muhammad A. S. <muh...@gm...>]

> to fix the latest stable release (which I was able to download) so
> that it doesn't fail on Linux with:
>
> dusty:JPF $ bin/jpf -show
> : bad interpreter: No such file or directory

Run "dos2unix" to fix the CR/LF issue.

Somebody with CVS access rights, please fix the release or remove it!

/Ali
--
Dependable Computer Systems
Chalmers University of Technology, Sweden

Re: [Javapathfinder-user] CVS out?

[Dusty P. <bu...@gm...>]

On 12/11/05, Dusty Phillips <bu...@gm...> wrote:
> Thanks for verifying my sanity.  I just looked at sourceforge's status
> page here, it looks like there are problems with CVS that will
> continue through the weekend:
<snip>
> Patience is the key, I guess.

Ok, the weekend is up and no change on sourceforge's status. I would
love to be patient, but I kind of need to try JPF before the
assignment due date... ;-) Would anybody be able to create a snapshot
of the current CVS at some stable point? Or could somebody tell me how
to fix the latest stable release (which I was able to download) so
that it doesn't fail on Linux with:

dusty:JPF $ bin/jpf -show
: bad interpreter: No such file or directory


Interestingly, gna.org is also out at the moment. It must be a conspiracy.

Dusty

Re: [Javapathfinder-user] CVS out?

[Dusty P. <bu...@gm...>]

Thanks for verifying my sanity.  I just looked at sourceforge's status
page here, it looks like there are problems with CVS that will
continue through the weekend:

http://sourceforge.net/docman/display_doc.php?group_id=3D1&docid=3D2352

Noteably:
__________________
(  2005-11-11 12:47:03 - Project CVS Service )   As of 2005-11-11
developer CVS is back online and operational. Anonymous CVS will be
out of sync throughout the weekend as updates are processed.

( 2005-11-11 06:27:36 - Project CVS Service )   As of 2005-11-11
developer CVS service is presently offline for unplanned maintenance,
estimated time of service restoration to be determined.

<snip>

(  2005-11-01 11:17:41 - Project CVS Service )   As of 2005-11-01 at
10:00 Pacific, project's whose name begins with e, h, i or j will not
have access to anonymous CVS, tarballs and ViewCVS. We are currently
looking into this issue and hope to have it resolved soon.
_________________

Patience is the key, I guess.

Dusty



On 12/11/05, Eric Platon <pl...@ni...> wrote:
> >I'm having trouble connecting to CVS. I don't think I'm doing anything
> wrong, I've connected to >>sourceforge projects before. I can't even get
> anonymous login
>
>
> I am having the same problem and one of my colleagues as well. Note that =
I
> personally use Eclipse.
>
> My colleague has heard about a recent change on sourceforge cvs managemen=
t.
> Although I haven't checked yet in detail, it might be the reason of our
> problem.
>
> Eric
>
>
>
> -------------------------------------------------------
> SF.Net email is sponsored by:
> Tame your development challenges with Apache's Geronimo App Server. Downl=
oad
> it for free - -and be entered to win a 42" plasma tv or your very own
> Sony(tm)PSP.  Click here to play: http://sourceforge.net/geronimo.php
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>

RE: [Javapathfinder-user] CVS out?

[Eric P. <pl...@ni...>]

>I'm having trouble connecting to CVS. I don't think I'm doing anything
wrong, I've connected to >>sourceforge projects before. I can't even get
anonymous login


I am having the same problem and one of my colleagues as well. Note that I
personally use Eclipse.

My colleague has heard about a recent change on sourceforge cvs management.
Although I haven't checked yet in detail, it might be the reason of our
problem.

Eric

[Javapathfinder-user] CVS out?

[Dusty P. <bu...@gm...>]

I'm having trouble connecting to CVS. I don't think I'm doing anything
wrong, I've connected to sourceforge projects before. I can't even get
anonymous login:

---------------------------
dusty:~ $  cvs -d:pserver:ano...@cv...:/cvsroot/javapathfi=
nder
login
Logging in to :pserver:ano...@cv...:2401/cvsroot/javapathf=
inder
CVS password:
cvs login: authorization failed: server cvs.sourceforge.net rejected
access to /cvsroot/javapathfinder for user anonymous
dusty:~ $
-----------------------------

Further, I get a 'Proxy Error' when I go here:
http://cvs.sourceforge.net/viewcvs.py/javapathfinder

Is it just me doing something inane, or is there a problem with CVS
right now? Is it a pathfinder problem, or a sourceforge problem? any
idea when it might be fixed?

Thanks,

Dusty

[Javapathfinder-user] subscribe

[raneotempo\@libero\.it <ran...@li...>]

[Javapathfinder-user] Automated Test Case Generation

[Muhammad A. S. <muh...@gm...>]

Hi!

I've been using JPF to execute my test drivers written with Verify.random(i=
)
to generate all possible integers, array sizes, etc. However, I have also
come across a paper that discusses non-isomorphic test case generation usin=
g
Java Pathfinder. Can somebody please guide me how to use JPF in this
respect? Is a separate component required? Or is it internal research at
this point in time?

Any help will be highly appreciated.

/Ali
---
Dependable Computer Systems
Chalmers University of Technology
Sweden

RE: [Javapathfinder-user] Specifying properties using "Property" scheme

[Eric P. <pl...@ni...>]

Peter,

Thank you for your (quick) reply. One of my goal is to understand the
Property mechanism of JPF, so I will try a bit more with normal Properties.
If something intersting comes up, I will report it here! Thank you for the
guidance.

Eric

Re: [Javapathfinder-user] Re: I can"t run JPF

[Peter C. M. <pcm...@em...>]

>>  JPF exception, terminating: could not load class D:\javapathfinder 
>> \bin\..\build\
>>  env\jpf;
>>

the property spec was split into two, causing the value ("D: 
\javapathfinder...") to become an argument of its own, which is  
interpreted as the class name. You probably have to quote the script  
arguments in jpf.bat (I don't have a windows box here to check). At  
least, this was a bug in the Unix script version, but not the next  
problem you encountered

>>  When I ran the jpf in Linux, I encountered the error as following:
>>  $ bin/jpf HelloWorld
>>  : bad interpreter: No such file or directory
>>  The jdk version I used is 1.4.2.

that is probably a corrupted shell script (containing <CR>s after a  
CVS checkout from Windows). Try to run recode or dos2unix

-- Peter

Re: [Javapathfinder-user] Re: I can"t run JPF

[Peter C. M. <pcm...@em...>]

> Before that, I tried the command line "+vm.bootclasspath = c:...", but
> oddly enough it did not solve the problem.

Just noticed that command line key/value Strings were not trimmed,  
causing this to add "vm.bootclasspath " instead of overloading  
"vm.bootclasspath". It's fixed, but as always it takes a day until  
that reaches the public CVS archive. I also forgot to quote shell  
arguments in the bin/jpf startup script, but I don't have a Windows  
version at hand to see if the same applies to jpf.bat

> A very tiny issue is that the online docu says that the default  
> property
> file is "default.properties". The help menu ("jpf" or "jpf -help")  
> says
> the default is "jpf.properties". It seems the online docu is correct.

both of them are loaded. The load order is

default.properties (might be looked up via "+jpf.basedir=<jpf-dir>"  
command line arg)
jpf.properties (or whatever file you specify with the "-c <mode- 
property>" command line arg)
"+<key>=<value>" command line args

i.e. command line args override everything. default.properties is  
used to specify all the internals JPF needs, but users rarely change.  
The mode property file "jpf.propeties" (or its replacement) shoudl  
contain application specific settings like listeners or report  
options. The command line is just to quickly play around with  
different settings.

-- Peter

Re: [Javapathfinder-user] Specifying properties using "Property" scheme

[Peter C. M. <pcm...@em...>]

Eric,

the check 'Object' argument is a left-over, and indeed null (I should  
clean it up). Extracting JPF object values from normal Properties is  
difficult. You get the vm, and from there you can obtain the  
DynamicArea (heap), but you still have to know the object reference  
(ElementInfo index) for your object in question. The problem is that  
'check' is evaluated after executing the whole transition, i.e. many  
instructions, so you don't have the instruction context anymore. Any  
property that needs this (e.g. to monitor certain field values)  
should better be a VMListener. For this specific purpose, there is a  
generic PropertyListenerAdapter class that implements the listener  
and property interfaces (see gov.nasa.jpf.tools.RaceDetector as an  
example - note that those properties get automatically registered  
during the SearchListener.searchStarted() notification). That's  
probably the best choice if your properties depend on object values,  
and not general search or vm execution states.

-- Peter

> My question targets the check(VM,Object) method: Is it possible to  
> extract
> the variable we need to check from the arguments? If yes, I have  
> not find
> how for the moment. For example, I tried to observe step-by-step  
> with jdb
> the behavior of JPF on a simple toy program (to check some  
> assertions on
> variable values). Setting a breakpoint on the check(VM,Object)  
> method of
> NoAssertionViolatedProperty, it turns out that the local variables  
> vm and
> arg are null and throw a NullPointerException when accessed.
>
> My group suggested other ideas to test out, but if anyone has  
> experience on
> that or encounters the same issue, let's get in touch.

Re: [Javapathfinder-user] Re: I can"t run JPF

[En Ye <ye....@gm...>]

Thanks for your help. When I used the download version, I encountered
the problem. Then I tried the CVS version, I didn't encounter the same
problem.

Yearn

On 10/5/05, Eric Platon <pl...@ni...> wrote:
> Hi Yearn,
>
> The both cases might be path problems. Have you tried to run your
> current systems with "jpf -show"? It should show you the dictionary of
> your configuration. If some values are not assigned, it might be your
> problem. If the command fails, so it might be a bootclasspath problem.
> As for Wxp, I encountered the latter and I ended up with (sigh) inlining
> the path directly into default.properties (for the moment):
> ***From default.properties***
> # the next two are used to load classes into JPF which are NOT in the
> normal classpath
> # (we can use the automatic defaults if started from the JPF root dir)
> # where to load essential system model classes from (like java.lang.Threa=
d)
> vm.bootclasspath =3D C:\\javapathfinder\\build\\env\\jpf
> ***END***
>
> Before that, I tried the command line "+vm.bootclasspath =3D c:...", but
> oddly enough it did not solve the problem. On Wxp, it seems there are
> some issues with the environment values such as
> "${jpf.basedir}/build/env/jpf"... No value is assigned indeed.
>
> A very tiny issue is that the online docu says that the default property
> file is "default.properties". The help menu ("jpf" or "jpf -help") says
> the default is "jpf.properties". It seems the online docu is correct.
> So, the proper way to do the above would be to create a
> myProp.properties and use the command option "-c myProp.properties" when
> invoking JPF.
>
> I hope this might help somehow.
>
> Eric
>
>
> From: En Ye <ye@gm...>
> I can"t run JPF
> <http://sourceforge.net/mailarchive/message.php?msg_id=3D12586198>
> 2005-08-07 19:54
>
>  Hi all,
>
>  After I ran the "ant run-tests" command successfully, I tried to use
>  JPF to model check the HelloWorld application in the example
>  directory, however,  I cannot get it to work.
>  When I ran the jpf.bat in WindowXP, I encountered the error as following=
:
>  D:\javapathfinder>bin\jpf.bat HelloWorld
>  Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames
>  Research Center
>  JPF exception, terminating: could not load class D:\javapathfinder\bin\.=
.\build\
>  env\jpf;
>  When I ran the jpf in Linux, I encountered the error as following:
>  $ bin/jpf HelloWorld
>  : bad interpreter: No such file or directory
>  The jdk version I used is 1.4.2.
>  I can"t  figure out the error. So could someone give me some advice?
>  Thanks in advance.
>
>  Yearn
>
>
>
>
> -------------------------------------------------------
> This SF.Net email is sponsored by:
> Power Architecture Resource Center: Free content, downloads, discussions,
> and more. http://solutions.newsforge.com/ibmarch.tmpl
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>

[Javapathfinder-user] Re: I can"t run JPF

[Eric P. <pl...@ni...>]

Hi Yearn,

The both cases might be path problems. Have you tried to run your
current systems with "jpf -show"? It should show you the dictionary of
your configuration. If some values are not assigned, it might be your
problem. If the command fails, so it might be a bootclasspath problem.
As for Wxp, I encountered the latter and I ended up with (sigh) inlining
the path directly into default.properties (for the moment):
***From default.properties***
# the next two are used to load classes into JPF which are NOT in the
normal classpath
# (we can use the automatic defaults if started from the JPF root dir)
# where to load essential system model classes from (like java.lang.Thread)
vm.bootclasspath = C:\\javapathfinder\\build\\env\\jpf
***END***

Before that, I tried the command line "+vm.bootclasspath = c:...", but
oddly enough it did not solve the problem. On Wxp, it seems there are
some issues with the environment values such as
"${jpf.basedir}/build/env/jpf"... No value is assigned indeed.

A very tiny issue is that the online docu says that the default property
file is "default.properties". The help menu ("jpf" or "jpf -help") says
the default is "jpf.properties". It seems the online docu is correct.
So, the proper way to do the above would be to create a
myProp.properties and use the command option "-c myProp.properties" when
invoking JPF.

I hope this might help somehow.

Eric


From: En Ye <ye@gm...>
I can"t run JPF
<http://sourceforge.net/mailarchive/message.php?msg_id=12586198>
2005-08-07 19:54

 Hi all,
 
 After I ran the "ant run-tests" command successfully, I tried to use
 JPF to model check the HelloWorld application in the example
 directory, however,  I cannot get it to work.
 When I ran the jpf.bat in WindowXP, I encountered the error as following:
 D:\javapathfinder>bin\jpf.bat HelloWorld
 Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames
 Research Center
 JPF exception, terminating: could not load class D:\javapathfinder\bin\..\build\
 env\jpf;
 When I ran the jpf in Linux, I encountered the error as following:
 $ bin/jpf HelloWorld
 : bad interpreter: No such file or directory
 The jdk version I used is 1.4.2. 
 I can"t  figure out the error. So could someone give me some advice?
 Thanks in advance.
 
 Yearn
 

[Javapathfinder-user] Specifying properties using "Property" scheme

[Eric P. <pl...@ni...>]

Hi everyone,

This question echoes the one from M=EDrian Bruckschen about Specifying
properties using "Listener" scheme.

Since June, our group has started using JPF and we are about writing =
custom
properties. I am trying to figure out how to configure my own properties
according to the documentation, but for the moment my trials are not
conclusive. The first way to implement properties =
(gov.nasa.jpf.Property)
seems sufficient for our current needs, so I have only tried to =
configure
this one.

My question targets the check(VM,Object) method: Is it possible to =
extract
the variable we need to check from the arguments? If yes, I have not =
find
how for the moment. For example, I tried to observe step-by-step with =
jdb
the behavior of JPF on a simple toy program (to check some assertions on
variable values). Setting a breakpoint on the check(VM,Object) method of
NoAssertionViolatedProperty, it turns out that the local variables vm =
and
arg are null and throw a NullPointerException when accessed.

My group suggested other ideas to test out, but if anyone has experience =
on
that or encounters the same issue, let's get in touch.

Eric Platon

Re: [Javapathfinder-user] About java.lang.UnsatisfiedLinkError

[Peter C. M. <pcm...@em...>]

En,

you have basically two choices:

(1) add a File.list() implementation (which shoulnd't be too hard if  
you are only interested in the standard functionality) - but that  
might not be all that's required to make the sun.misc.* classes  
happy. The other thing is that our File class is supposed to be an  
abstraction (even though Owen wrote it mostly being interested in  
RandomAccessFile data state keeping, and File doesn't have a real  
purpose yet) - question is what we would model here (state tracked  
directory contents?) Of course, that would be our preferred choice :)

(2) try to find a cut point in java.security or sun.misc.Launcher,  
where you can cut off further sun.misc (and File) usage by a stub. If  
you are not interested in the java.security.* internals, that sounds  
feasible. That's probably your best shot.

-- Peter

On Sep 15, 2005, at 9:16 PM, En Ye wrote:


> Peter,
>
> Thank you very much for your advice.  After solving the
> "java.lang.UnsatisfiedLinkError" exception by adding native peer
> class, I reran the same program. Then I encountered a new exception as
> following:
>
> java.lang.NoSuchMethodException: java.io.File.list()
>     at sun.misc.Launcher$ExtClassLoader.getExtURLs(sun\misc 
> \Launcher.java:161)
>     at sun.misc.Launcher$ExtClassLoader.<init>(sun\misc 
> \Launcher.java:137)
>     at sun.misc.Launcher$1.run(sun\misc\Launcher.java:121)
>     at java.security.AccessController.doPrivileged(java\security 
> \AccessController.java:53)
>     at sun.misc.Launcher$ExtClassLoader.getExtClassLoader(sun\misc 
> \Launcher.java:118)
>     at sun.misc.Launcher.<init>(sun\misc\Launcher.java:51)
>     at sun.misc.Launcher.<clinit>(sun\misc\Launcher.java:39)
>     at java.security.Security.getEngineClassName(java\security 
> \Security.java:529)
>     at java.security.Security.getEngineClassName(java\security 
> \Security.java:595)
>     at java.security.Security.getImpl(java\security\Security.java: 
> 1044)
>     at java.security.KeyPairGenerator.getInstance(java\security 
> \KeyPairGenerator.java:146)
>     at DHKeyAgreement3.run(DHKeyAgreement3.java:54)
>     at DHKeyAgreement3.main(DHKeyAgreement3.java:38).
>
> I know the exception was thown because the File model class in the
> "javapathfinder\env\jpf\java\io" doesn't provide "list" function while
> the original File class does. So could you kindly tell me how can I
> solve this problem? It is seemly impossible to only add a stubbed
> "list" function to the File model class since the "list" function
> needs to return a String array. If I just delete the File model class,
> what will it affect the JavaPathFinder? Thanks in advance for your
> help.
>
> En
>
> On 9/6/05, Peter C. Mehlitz <pcm...@em...> wrote:
>
>
>> En,
>>
>> Yes, you are right - ObjectStream native methods are not supported
>> yet. It's probably better to intercept the BigInteger.<clinit> in a
>> native peer (like StringBuffer does too) than to fiddle directly with
>> the ObjectStreamClass, since I assume it really needs the native
>> methods. We don't support serialization yet, anyways.
>>
>> -- Peter
>>
>> On Sep 4, 2005, at 9:01 PM, En Ye wrote:
>>
>>
>>
>>> Hi all,
>>>
>>> When I used JavaPathFinder to verify a Java Class DHKeyAgreement3
>>> (source code is attached at the end). I encountered an exception
>>> listed below:
>>>
>>> java.lang.UnsatisfiedLinkError:
>>> java.io.ObjectStreamClass.initNative (no peer)
>>>     at java.io.ObjectStreamClass.<clinit>(java\io
>>> \ObjectStreamClass.java:133)
>>>     at java.io.ObjectStreamField.<init>(java\io
>>> \ObjectStreamField.java:71)
>>>     at java.io.ObjectStreamField.<init>(java\io
>>> \ObjectStreamField.java:45)
>>>     at java.math.BigInteger.<clinit>(java\math\BigInteger.java:3008)
>>>     at DHKeyAgreement3.<clinit>(DHKeyAgreement3.java:204)
>>>     at DHKeyAgreement3.main(DHKeyAgreement3.java:37)
>>> ..
>>> I guess the exception was thrown because the JPF cannot find an
>>> appropriate native peer class for java.io.ObjectStreamClass (JPF  
>>> don't
>>> provide this native peer class). If it is right, can I create a  
>>> native
>>> peer class for it to eliminate the exception? And if I can, can I do
>>> it as the following:
>>> (1) create a MJI model class for java.io.ObjectStreamClass and  
>>> put it
>>> in the env\jpf folder
>>> (2) use "GenPeer" to generate a native peer class for
>>> java.io.ObjectStreamClass and put in the env\jvm folder
>>> ?  Or it there any other solution? Is there any related  
>>> documentation
>>> on it? Thanks in advance for your help.
>>>
>>>
>>
>>
>>
>
>
>

Re: [Javapathfinder-user] About java.lang.UnsatisfiedLinkError

[En Ye <ye....@gm...>]

Peter,

Thank you very much for your advice.  After solving the
"java.lang.UnsatisfiedLinkError" exception by adding native peer
class, I reran the same program. Then I encountered a new exception as
following:

java.lang.NoSuchMethodException: java.io.File.list()
=09at sun.misc.Launcher$ExtClassLoader.getExtURLs(sun\misc\Launcher.java:16=
1)
=09at sun.misc.Launcher$ExtClassLoader.<init>(sun\misc\Launcher.java:137)
=09at sun.misc.Launcher$1.run(sun\misc\Launcher.java:121)
=09at java.security.AccessController.doPrivileged(java\security\AccessContr=
oller.java:53)
=09at sun.misc.Launcher$ExtClassLoader.getExtClassLoader(sun\misc\Launcher.=
java:118)
=09at sun.misc.Launcher.<init>(sun\misc\Launcher.java:51)
=09at sun.misc.Launcher.<clinit>(sun\misc\Launcher.java:39)
=09at java.security.Security.getEngineClassName(java\security\Security.java=
:529)
=09at java.security.Security.getEngineClassName(java\security\Security.java=
:595)
=09at java.security.Security.getImpl(java\security\Security.java:1044)
=09at java.security.KeyPairGenerator.getInstance(java\security\KeyPairGener=
ator.java:146)
=09at DHKeyAgreement3.run(DHKeyAgreement3.java:54)
=09at DHKeyAgreement3.main(DHKeyAgreement3.java:38).

I know the exception was thown because the File model class in the
"javapathfinder\env\jpf\java\io" doesn't provide "list" function while
the original File class does. So could you kindly tell me how can I
solve this problem? It is seemly impossible to only add a stubbed
"list" function to the File model class since the "list" function
needs to return a String array. If I just delete the File model class,
what will it affect the JavaPathFinder? Thanks in advance for your
help.

En

On 9/6/05, Peter C. Mehlitz <pcm...@em...> wrote:
> En,
>=20
> Yes, you are right - ObjectStream native methods are not supported
> yet. It's probably better to intercept the BigInteger.<clinit> in a
> native peer (like StringBuffer does too) than to fiddle directly with
> the ObjectStreamClass, since I assume it really needs the native
> methods. We don't support serialization yet, anyways.
>=20
> -- Peter
>=20
> On Sep 4, 2005, at 9:01 PM, En Ye wrote:
>=20
> > Hi all,
> >
> > When I used JavaPathFinder to verify a Java Class DHKeyAgreement3
> > (source code is attached at the end). I encountered an exception
> > listed below:
> >
> > java.lang.UnsatisfiedLinkError:
> > java.io.ObjectStreamClass.initNative (no peer)
> >     at java.io.ObjectStreamClass.<clinit>(java\io
> > \ObjectStreamClass.java:133)
> >     at java.io.ObjectStreamField.<init>(java\io
> > \ObjectStreamField.java:71)
> >     at java.io.ObjectStreamField.<init>(java\io
> > \ObjectStreamField.java:45)
> >     at java.math.BigInteger.<clinit>(java\math\BigInteger.java:3008)
> >     at DHKeyAgreement3.<clinit>(DHKeyAgreement3.java:204)
> >     at DHKeyAgreement3.main(DHKeyAgreement3.java:37)
> > ..
> > I guess the exception was thrown because the JPF cannot find an
> > appropriate native peer class for java.io.ObjectStreamClass (JPF don't
> > provide this native peer class). If it is right, can I create a native
> > peer class for it to eliminate the exception? And if I can, can I do
> > it as the following:
> > (1) create a MJI model class for java.io.ObjectStreamClass and put it
> > in the env\jpf folder
> > (2) use "GenPeer" to generate a native peer class for
> > java.io.ObjectStreamClass and put in the env\jvm folder
> > ?  Or it there any other solution? Is there any related documentation
> > on it? Thanks in advance for your help.
>

Re: [Javapathfinder-user] About java.lang.UnsatisfiedLinkError

[Peter C. M. <pcm...@em...>]

En,

Yes, you are right - ObjectStream native methods are not supported  
yet. It's probably better to intercept the BigInteger.<clinit> in a  
native peer (like StringBuffer does too) than to fiddle directly with  
the ObjectStreamClass, since I assume it really needs the native  
methods. We don't support serialization yet, anyways.

-- Peter

On Sep 4, 2005, at 9:01 PM, En Ye wrote:

> Hi all,
>
> When I used JavaPathFinder to verify a Java Class DHKeyAgreement3
> (source code is attached at the end). I encountered an exception
> listed below:
>
> java.lang.UnsatisfiedLinkError:  
> java.io.ObjectStreamClass.initNative (no peer)
>     at java.io.ObjectStreamClass.<clinit>(java\io 
> \ObjectStreamClass.java:133)
>     at java.io.ObjectStreamField.<init>(java\io 
> \ObjectStreamField.java:71)
>     at java.io.ObjectStreamField.<init>(java\io 
> \ObjectStreamField.java:45)
>     at java.math.BigInteger.<clinit>(java\math\BigInteger.java:3008)
>     at DHKeyAgreement3.<clinit>(DHKeyAgreement3.java:204)
>     at DHKeyAgreement3.main(DHKeyAgreement3.java:37)
> ..
> I guess the exception was thrown because the JPF cannot find an
> appropriate native peer class for java.io.ObjectStreamClass (JPF don't
> provide this native peer class). If it is right, can I create a native
> peer class for it to eliminate the exception? And if I can, can I do
> it as the following:
> (1) create a MJI model class for java.io.ObjectStreamClass and put it
> in the env\jpf folder
> (2) use "GenPeer" to generate a native peer class for
> java.io.ObjectStreamClass and put in the env\jvm folder
> ?  Or it there any other solution? Is there any related documentation
> on it? Thanks in advance for your help.

[Javapathfinder-user] About java.lang.UnsatisfiedLinkError

[En Ye <ye....@gm...>]

Hi all,

When I used JavaPathFinder to verify a Java Class DHKeyAgreement3
(source code is attached at the end). I encountered an exception
listed below:

java.lang.UnsatisfiedLinkError: java.io.ObjectStreamClass.initNative (no pe=
er)
=09at java.io.ObjectStreamClass.<clinit>(java\io\ObjectStreamClass.java:133=
)
=09at java.io.ObjectStreamField.<init>(java\io\ObjectStreamField.java:71)
=09at java.io.ObjectStreamField.<init>(java\io\ObjectStreamField.java:45)
=09at java.math.BigInteger.<clinit>(java\math\BigInteger.java:3008)
=09at DHKeyAgreement3.<clinit>(DHKeyAgreement3.java:204)
=09at DHKeyAgreement3.main(DHKeyAgreement3.java:37)

----------------------------------- path to error (length: 1)
Transition #0 Thread #0
  DHKeyAgreement3.java:168     private static final byte
skip1024ModulusBytes[] =3D {
  DHKeyAgreement3.java:204     private static final BigInteger skip1024Modu=
lus
  [no source for: java\math\BigInteger.java]
  [no source for: java\lang\Number.java]
  [no source for: java\lang\Object.java]
=09......

------------------------------------ end error path

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
  1 Error Found: uncaught exception
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

I guess the exception was thrown because the JPF cannot find an
appropriate native peer class for java.io.ObjectStreamClass (JPF don't
provide this native peer class). If it is right, can I create a native
peer class for it to eliminate the exception? And if I can, can I do
it as the following:
(1) create a MJI model class for java.io.ObjectStreamClass and put it
in the env\jpf folder
(2) use "GenPeer" to generate a native peer class for
java.io.ObjectStreamClass and put in the env\jvm folder
?  Or it there any other solution? Is there any related documentation
on it? Thanks in advance for your help.

En

The source code of DHKeyAgreement3 class
/*
 * Copyright 1997-2001 by Sun Microsystems, Inc.,
 * 901 San Antonio Road, Palo Alto, California, 94303, U.S.A.
 * All rights reserved.
 *
 * This software is the confidential and proprietary information
 * of Sun Microsystems, Inc. ("Confidential Information").  You
 * shall not disclose such Confidential Information and shall use
 * it only in accordance with the terms of the license agreement
 * you entered into with Sun.
 */

import java.io.*;
import java.math.BigInteger;
import java.security.*;
import java.security.spec.*;
import java.security.interfaces.*;
import javax.crypto.*;
import javax.crypto.spec.*;
import javax.crypto.interfaces.*;
import com.sun.crypto.provider.SunJCE;

/**
 * This program executes the Diffie-Hellman key agreement protocol
 * between 3 parties: Alice, Bob, and Carol.
 *
 * We use the same 1024-bit prime modulus and base generator that are=20
 * used by SKIP.
 */

public class DHKeyAgreement3 {

    private DHKeyAgreement3() {}

    public static void main(String argv[]) {
        try {
            DHKeyAgreement3 keyAgree =3D new DHKeyAgreement3();
            keyAgree.run();
        } catch (Exception e) {
            System.err.println("Error: " + e);
            System.exit(1);
        }
    }

    private void run() throws Exception {

        DHParameterSpec dhSkipParamSpec;

        System.out.println("Using SKIP Diffie-Hellman parameters");
        dhSkipParamSpec =3D new DHParameterSpec(skip1024Modulus, skip1024Ba=
se);

        // Alice creates her own DH key pair
        System.out.println("ALICE: Generate DH keypair ...");
        KeyPairGenerator aliceKpairGen =3D KeyPairGenerator.getInstance("DH=
");
        aliceKpairGen.initialize(dhSkipParamSpec);
        KeyPair aliceKpair =3D aliceKpairGen.generateKeyPair();

        // Bob creates his own DH key pair
        System.out.println("BOB: Generate DH keypair ...");
        KeyPairGenerator bobKpairGen =3D KeyPairGenerator.getInstance("DH")=
;
        bobKpairGen.initialize(dhSkipParamSpec);
        KeyPair bobKpair =3D bobKpairGen.generateKeyPair();

        // Carol creates her own DH key pair
        System.out.println("CAROL: Generate DH keypair ...");
        KeyPairGenerator carolKpairGen =3D KeyPairGenerator.getInstance("DH=
");
        carolKpairGen.initialize(dhSkipParamSpec);
        KeyPair carolKpair =3D carolKpairGen.generateKeyPair();


        // Alice initialize
        System.out.println("ALICE: Initialize ...");
        KeyAgreement aliceKeyAgree =3D KeyAgreement.getInstance("DH");
        aliceKeyAgree.init(aliceKpair.getPrivate());

        // Bob initialize
        System.out.println("BOB: Initialize ...");
        KeyAgreement bobKeyAgree =3D KeyAgreement.getInstance("DH");
        bobKeyAgree.init(bobKpair.getPrivate());

        // Carol initialize
        System.out.println("CAROL: Initialize ...");
        KeyAgreement carolKeyAgree =3D KeyAgreement.getInstance("DH");
        carolKeyAgree.init(carolKpair.getPrivate());


        // Alice uses Carol's public key
        Key ac =3D aliceKeyAgree.doPhase(carolKpair.getPublic(), false);

        // Bob uses Alice's public key
        Key ba =3D bobKeyAgree.doPhase(aliceKpair.getPublic(), false);

        // Carol uses Bob's public key
        Key cb =3D carolKeyAgree.doPhase(bobKpair.getPublic(), false);


        // Alice uses Carol's result from above
        aliceKeyAgree.doPhase(cb, true);

        // Bob uses Alice's result from above
        bobKeyAgree.doPhase(ac, true);

        // Carol uses Bob's result from above
        carolKeyAgree.doPhase(ba, true);


        // Alice, Bob and Carol compute their secrets
        byte[] aliceSharedSecret =3D aliceKeyAgree.generateSecret();
        System.out.println("Alice secret: " + toHexString(aliceSharedSecret=
));

        byte[] bobSharedSecret =3D bobKeyAgree.generateSecret();
        System.out.println("Bob secret: " + toHexString(bobSharedSecret));

        byte[] carolSharedSecret =3D carolKeyAgree.generateSecret();
        System.out.println("Carol secret: " + toHexString(carolSharedSecret=
));


        // Compare Alice and Bob
        if (!java.util.Arrays.equals(aliceSharedSecret, bobSharedSecret))
            throw new Exception("Alice and Bob differ");
        System.out.println("Alice and Bob are the same");

        // Compare Bob and Carol
        if (!java.util.Arrays.equals(bobSharedSecret, carolSharedSecret))
            throw new Exception("Bob and Carol differ");
        System.out.println("Bob and Carol are the same");
    }


    /*
     * Converts a byte to hex digit and writes to the supplied buffer
     */
    private void byte2hex(byte b, StringBuffer buf) {
        char[] hexChars =3D { '0', '1', '2', '3', '4', '5', '6', '7', '8',
                            '9', 'A', 'B', 'C', 'D', 'E', 'F' };
        int high =3D ((b & 0xf0) >> 4);
        int low =3D (b & 0x0f);
        buf.append(hexChars[high]);
        buf.append(hexChars[low]);
    }

    /*
     * Converts a byte array to hex string
     */
    private String toHexString(byte[] block) {
        StringBuffer buf =3D new StringBuffer();

        int len =3D block.length;

        for (int i =3D 0; i < len; i++) {
             byte2hex(block[i], buf);
             if (i < len-1) {
                 buf.append(":");
             }
        }=20
        return buf.toString();
    }

    /*
     * Prints the usage of this test.
     */
    private void usage() {
        System.err.print("DHKeyAgreement usage: ");
        System.err.println("[-gen]");
    }

    // The 1024 bit Diffie-Hellman modulus values used by SKIP
    private static final byte skip1024ModulusBytes[] =3D {
        (byte)0xF4, (byte)0x88, (byte)0xFD, (byte)0x58,
        (byte)0x4E, (byte)0x49, (byte)0xDB, (byte)0xCD,
        (byte)0x20, (byte)0xB4, (byte)0x9D, (byte)0xE4,
        (byte)0x91, (byte)0x07, (byte)0x36, (byte)0x6B,
        (byte)0x33, (byte)0x6C, (byte)0x38, (byte)0x0D,
        (byte)0x45, (byte)0x1D, (byte)0x0F, (byte)0x7C,
        (byte)0x88, (byte)0xB3, (byte)0x1C, (byte)0x7C,
        (byte)0x5B, (byte)0x2D, (byte)0x8E, (byte)0xF6,
        (byte)0xF3, (byte)0xC9, (byte)0x23, (byte)0xC0,
        (byte)0x43, (byte)0xF0, (byte)0xA5, (byte)0x5B,
        (byte)0x18, (byte)0x8D, (byte)0x8E, (byte)0xBB,
        (byte)0x55, (byte)0x8C, (byte)0xB8, (byte)0x5D,
        (byte)0x38, (byte)0xD3, (byte)0x34, (byte)0xFD,
        (byte)0x7C, (byte)0x17, (byte)0x57, (byte)0x43,
        (byte)0xA3, (byte)0x1D, (byte)0x18, (byte)0x6C,
        (byte)0xDE, (byte)0x33, (byte)0x21, (byte)0x2C,
        (byte)0xB5, (byte)0x2A, (byte)0xFF, (byte)0x3C,
        (byte)0xE1, (byte)0xB1, (byte)0x29, (byte)0x40,
        (byte)0x18, (byte)0x11, (byte)0x8D, (byte)0x7C,
        (byte)0x84, (byte)0xA7, (byte)0x0A, (byte)0x72,
        (byte)0xD6, (byte)0x86, (byte)0xC4, (byte)0x03,
        (byte)0x19, (byte)0xC8, (byte)0x07, (byte)0x29,
        (byte)0x7A, (byte)0xCA, (byte)0x95, (byte)0x0C,
        (byte)0xD9, (byte)0x96, (byte)0x9F, (byte)0xAB,
        (byte)0xD0, (byte)0x0A, (byte)0x50, (byte)0x9B,
        (byte)0x02, (byte)0x46, (byte)0xD3, (byte)0x08,
        (byte)0x3D, (byte)0x66, (byte)0xA4, (byte)0x5D,
        (byte)0x41, (byte)0x9F, (byte)0x9C, (byte)0x7C,
        (byte)0xBD, (byte)0x89, (byte)0x4B, (byte)0x22,
        (byte)0x19, (byte)0x26, (byte)0xBA, (byte)0xAB,
        (byte)0xA2, (byte)0x5E, (byte)0xC3, (byte)0x55,
        (byte)0xE9, (byte)0x2F, (byte)0x78, (byte)0xC7
    };

    // The SKIP 1024 bit modulus
    private static final BigInteger skip1024Modulus
    =3D new BigInteger(1, skip1024ModulusBytes);

    // The base used with the SKIP 1024 bit modulus
    private static final BigInteger skip1024Base =3D BigInteger.valueOf(2);
}

Re: [Javapathfinder-user] Problem about Heuristic Search

[Wang L. <jel...@ho...>]

<html><div style='background-color:'><DIV class=RTE>
<P>Hi,Peter,</P>
<P>Thanks for your reply,I got the new version of Interleaving.java via 
CVS,and it works well now.</P>
<P>With regards.</P>
<P>--Wanglei<BR><BR></P><BR><BR><BR>&gt;From: Peter C.Mehlitz 
&lt;pcm...@em...&gt;<BR>&gt;To: ?纾
?&lt;jel...@ho...&gt;<BR>&gt;CC: 
jav...@li...<BR>&gt;Subject: Re: 
[Javapathfinder-user] Problem about Heuristic Search<BR>&gt;Date: Wed, 10 
Aug 2005 09:37:11 -0700<BR>&gt;<BR>&gt;some of the Heuristic classes had 
non-public ctors, which caused&nbsp;&nbsp;<BR>&gt;NoSuchMethodExceptions 
when instantiating via the Config based&nbsp;&nbsp;<BR>&gt;reflection. 
Should be fixed in the repository (as always, the public 
<BR>&gt;&nbsp;&nbsp;CVS takes a bit longer), but not all Heuristic 
instances have been <BR>&gt;&nbsp;&nbsp;tested recently.<BR>&gt;<BR>&gt;-- 
Peter<BR>&gt;<BR>&gt;<BR>&gt;On Aug 9, 2005, at 1:40 AM, ?纾
?wrote:<BR>&gt;<BR>&gt;&gt;Hi,All<BR>&gt;&gt;<BR>&gt;&gt;I'm trying to 
model check the Dining Philosophers problem 
using&nbsp;&nbsp;<BR>&gt;&gt;heuristic search,and specify the heuristic 
class :<BR>&gt;&gt;search.heuristic.class = 
gov.nasa.jpf.search.heuristic.Interleaving<BR>&gt;&gt;<BR>&gt;&gt;However,an 
error occurs when I run JPF.The printout is shown 
below:<BR>&gt;&gt;<BR>&gt;&gt;<BR>&gt;&gt;G:\JPF\javapathfinder\examples&gt;java 
gov.nasa.jpf.JPF -c .. <BR>&gt;&gt;\default.properties -show 
DiningPhilosophers.DiningPhilosophers<BR>&gt;&gt;Java Pathfinder Model 
Checker v3.1.2 - (C) 1999-2004 RIACS/NASA&nbsp;&nbsp;<BR>&gt;&gt;Ames 
Research Center<BR>&gt;&gt;----------- dictionary 
contents<BR>&gt;&gt;branch_start = 1<BR>&gt;&gt;jpf.basedir = 
.<BR>&gt;&gt;jpf.print_exception_stack = false<BR>&gt;&gt;jpf.version = 
3.1.2<BR>&gt;&gt;search.class = 
gov.nasa.jpf.search.heuristic.HeuristicSearch<BR>&gt;&gt;search.error_path 
= error.xml<BR>&gt;&gt;search.heuristic.branch.count_early = 
true<BR>&gt;&gt;search.heuristic.branch.no_branch_return = 
-1<BR>&gt;&gt;search.heuristic.class = 
gov.nasa.jpf.search.heuristic.Interleaving<BR>&gt;&gt;search.heuristic.comparator.class 
=&nbsp;&nbsp;<BR>&gt;&gt;gov.nasa.jpf.search.heuristic.DefaultComparator<BR>&gt;&gt;search.heuristic.queue_limit 
= -1<BR>&gt;&gt;search.match_depth = false<BR>&gt;&gt;search.min_free = 
1M<BR>&gt;&gt;search.multiple_errors = false<BR>&gt;&gt;search.print_errors 
= true<BR>&gt;&gt;search.properties 
=&nbsp;&nbsp;<BR>&gt;&gt;gov.nasa.jpf.jvm.NotDeadlockedProperty:gov.nasa.jpf.jvm.NoAssertionVio 
<BR>&gt;&gt;latedPrope<BR>&gt;&gt;rty:gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty<BR>&gt;&gt;vm.atomic_init 
= true<BR>&gt;&gt;vm.attributor.class = 
gov.nasa.jpf.jvm.DefaultAttributor<BR>&gt;&gt;vm.bootclasspath = 
G:javapathfinderjavapathfinderbuildenvjpf<BR>&gt;&gt;vm.check_fp = 
false<BR>&gt;&gt;vm.check_fp_compare = true<BR>&gt;&gt;vm.class = 
gov.nasa.jpf.jvm.JVM<BR>&gt;&gt;vm.classpath = 
build/examples<BR>&gt;&gt;vm.enable_assertions = *<BR>&gt;&gt;vm.finalize = 
true<BR>&gt;&gt;vm.gc = true<BR>&gt;&gt;vm.halt_on_throw = 
false<BR>&gt;&gt;vm.path_output = false<BR>&gt;&gt;vm.por = 
true<BR>&gt;&gt;vm.por.field_boundaries = 
true<BR>&gt;&gt;vm.por.fieldlockinfo.class = 
<BR>&gt;&gt;gov.nasa.jpf.jvm.StatisticFieldLockInfo<BR>&gt;&gt;vm.por.sync_detection 
= true<BR>&gt;&gt;vm.report.printStacks = 
true<BR>&gt;&gt;vm.report.show_bytecode = 
false<BR>&gt;&gt;vm.report.show_missing_lines = 
false<BR>&gt;&gt;vm.report.show_steps = true<BR>&gt;&gt;vm.scheduler.class 
= gov.nasa.jpf.jvm.DefaultScheduler<BR>&gt;&gt;vm.scheduler.random_seed = 
0<BR>&gt;&gt;vm.scheduler.use_time_for_seed = 
false<BR>&gt;&gt;vm.storage.class = 
gov.nasa.jpf.jvm.Md5StateSet<BR>&gt;&gt;vm.tree_output = 
true<BR>&gt;&gt;vm.verify.ignore_path = true<BR>&gt;&gt;vm.visible_asserts 
= false<BR>&gt;&gt;----------- free 
arguments<BR>&gt;&gt;-show<BR>&gt;&gt;DiningPhilosophers.DiningPhilosophers<BR>&gt;&gt;JPF 
configuration error: error instantiating 
class&nbsp;&nbsp;<BR>&gt;&gt;gov.nasa.jpf.search.heuristic.Interleaving for 
en<BR>&gt;&gt;try "search.heuristic.class":no suitable ctor 
found<BR>&gt;&gt; &gt; used within "search.class" instantiation of 
class&nbsp;&nbsp;<BR>&gt;&gt;gov.nasa.jpf.search.heuristic.HeuristicSearch<BR>&gt;&gt;<BR>&gt;&gt;<BR>&gt;&gt;<BR>&gt;&gt;<BR>&gt;&gt;Thanks.<BR>&gt;&gt;<BR>&gt;&gt;Wanglei<BR>&gt;&gt;<BR>&gt;&gt;2005-08-09<BR>&gt;&gt;<BR>&gt;&gt;
垂涓浇 MSN Explorer Get 2 months 
FREE*.&nbsp;&nbsp;<BR>&gt;&gt;------------------------------------------------------- 
SF.Net&nbsp;&nbsp;<BR>&gt;&gt;email is Sponsored by the Better Software 
Conference &amp; EXPO&nbsp;&nbsp;<BR>&gt;&gt;September 19-22, 2005 * San 
Francisco, CA * Development Lifecycle&nbsp;&nbsp;<BR>&gt;&gt;Practices 
Agile &amp; Plan-Driven Development * Managing Projects 
&amp;&nbsp;&nbsp;<BR>&gt;&gt;Teams * Testing &amp; QA Security * Process 
Improvement &amp; Measurement * 
<BR>&gt;&gt;&nbsp;&nbsp;http://www.sqe.com/bsce5sf&nbsp;&nbsp;<BR>&gt;&gt;_______________________________________________ 
Javapathfinder-user <BR>&gt;&gt;&nbsp;&nbsp;mailing list 
Jav...@li... https:// 
<BR>&gt;&gt;lists.sourceforge.net/lists/listinfo/javapathfinder-user<BR>&gt;&gt;<BR>&gt;<BR>&gt;<BR>&gt;<BR>&gt;<BR>&gt;-------------------------------------------------------<BR>&gt;SF.Net 
email is Sponsored by the Better Software Conference &amp; 
EXPO<BR>&gt;September 19-22, 2005 * San Francisco, CA * Development 
Lifecycle <BR>&gt;Practices<BR>&gt;Agile &amp; Plan-Driven Development * 
Managing Projects &amp; Teams * <BR>&gt;Testing &amp; QA<BR>&gt;Security * 
Process Improvement &amp; Measurement * 
<BR>&gt;http://www.sqe.com/bsce5sf<BR>&gt;_______________________________________________<BR>&gt;Javapathfinder-user 
mailing 
list<BR>&gt;Jav...@li...<BR>&gt;https://lists.sourceforge.net/lists/listinfo/javapathfinder-user<BR></DIV></div><br 
clear=all><hr>使用  <a href="http://g.msn.com/8HMBCNCN/2734??PS=47575" 
target="_top">MSN Messenger </a> 与联机的朋友进行交流 </html>

Re: [Javapathfinder-user] Problem about Heuristic Search

[Peter C. M. <pcm...@em...>]

some of the Heuristic classes had non-public ctors, which caused =20
NoSuchMethodExceptions when instantiating via the Config based =20
reflection. Should be fixed in the repository (as always, the public =20
CVS takes a bit longer), but not all Heuristic instances have been =20
tested recently.

-- Peter


On Aug 9, 2005, at 1:40 AM, =E7=8E=8B =E7=A3=8A wrote:

> Hi,All
>
> I'm trying to model check the Dining Philosophers problem using =20
> heuristic search,and specify the heuristic class :
> search.heuristic.class =3D gov.nasa.jpf.search.heuristic.Interleaving
>
> However,an error occurs when I run JPF.The printout is shown below:
>
>
> G:\JPF\javapathfinder\examples>java gov.nasa.jpf.JPF -c ..=20
> \default.properties -show DiningPhilosophers.DiningPhilosophers
> Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA =20
> Ames Research Center
> ----------- dictionary contents
> branch_start =3D 1
> jpf.basedir =3D .
> jpf.print_exception_stack =3D false
> jpf.version =3D 3.1.2
> search.class =3D gov.nasa.jpf.search.heuristic.HeuristicSearch
> search.error_path =3D error.xml
> search.heuristic.branch.count_early =3D true
> search.heuristic.branch.no_branch_return =3D -1
> search.heuristic.class =3D gov.nasa.jpf.search.heuristic.Interleaving
> search.heuristic.comparator.class =3D =20
> gov.nasa.jpf.search.heuristic.DefaultComparator
> search.heuristic.queue_limit =3D -1
> search.match_depth =3D false
> search.min_free =3D 1M
> search.multiple_errors =3D false
> search.print_errors =3D true
> search.properties =3D =20
> gov.nasa.jpf.jvm.NotDeadlockedProperty:gov.nasa.jpf.jvm.NoAssertionVio=20=

> latedPrope
> rty:gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
> vm.atomic_init =3D true
> vm.attributor.class =3D gov.nasa.jpf.jvm.DefaultAttributor
> vm.bootclasspath =3D G:javapathfinderjavapathfinderbuildenvjpf
> vm.check_fp =3D false
> vm.check_fp_compare =3D true
> vm.class =3D gov.nasa.jpf.jvm.JVM
> vm.classpath =3D build/examples
> vm.enable_assertions =3D *
> vm.finalize =3D true
> vm.gc =3D true
> vm.halt_on_throw =3D false
> vm.path_output =3D false
> vm.por =3D true
> vm.por.field_boundaries =3D true
> vm.por.fieldlockinfo.class =3D gov.nasa.jpf.jvm.StatisticFieldLockInfo
> vm.por.sync_detection =3D true
> vm.report.printStacks =3D true
> vm.report.show_bytecode =3D false
> vm.report.show_missing_lines =3D false
> vm.report.show_steps =3D true
> vm.scheduler.class =3D gov.nasa.jpf.jvm.DefaultScheduler
> vm.scheduler.random_seed =3D 0
> vm.scheduler.use_time_for_seed =3D false
> vm.storage.class =3D gov.nasa.jpf.jvm.Md5StateSet
> vm.tree_output =3D true
> vm.verify.ignore_path =3D true
> vm.visible_asserts =3D false
> ----------- free arguments
> -show
> DiningPhilosophers.DiningPhilosophers
> JPF configuration error: error instantiating class =20
> gov.nasa.jpf.search.heuristic.Interleaving for en
> try "search.heuristic.class":no suitable ctor found
> > used within "search.class" instantiation of class =20
> gov.nasa.jpf.search.heuristic.HeuristicSearch
>
>
>
>
> Thanks.
>
> Wanglei
>
> 2005-08-09
>
> =E5=85=8D=E8=B4=B9=E4=B8=8B=E8=BD=BD MSN Explorer Get 2 months FREE*. =20=

> ------------------------------------------------------- SF.Net =20
> email is Sponsored by the Better Software Conference & EXPO =20
> September 19-22, 2005 * San Francisco, CA * Development Lifecycle =20
> Practices Agile & Plan-Driven Development * Managing Projects & =20
> Teams * Testing & QA Security * Process Improvement & Measurement * =20=

> http://www.sqe.com/bsce5sf =20
> _______________________________________________ Javapathfinder-user =20=

> mailing list Jav...@li... https://=20
> lists.sourceforge.net/lists/listinfo/javapathfinder-user
>

[Javapathfinder-user] Problem about Heuristic Search

[<jel...@ho...>]

<html><div style='background-color:'><DIV class=RTE>Hi,All</DIV>
<DIV class=RTE>&nbsp;</DIV>
<DIV class=RTE>I'm trying to model check the Dining Philosophers problem 
using heuristic search,and specify the heuristic class&nbsp;:</DIV>
<DIV class=RTE>search.heuristic.class = 
gov.nasa.jpf.search.heuristic.Interleaving</DIV>
<DIV class=RTE>&nbsp;</DIV>
<DIV class=RTE>However,an error occurs when I run JPF.The printout is shown 
below:</DIV>
<DIV class=RTE>&nbsp;</DIV>
<DIV class=RTE>&nbsp;</DIV>
<DIV class=RTE>G:\JPF\javapathfinder\examples&gt;java gov.nasa.jpf.JPF -c 
..\default.properties -show DiningPhilosophers.DiningPhilosophers<BR>Java 
Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames Research 
Center<BR>----------- dictionary contents<BR>branch_start = 
1<BR>jpf.basedir = .<BR>jpf.print_exception_stack = false<BR>jpf.version = 
3.1.2<BR>search.class = 
gov.nasa.jpf.search.heuristic.HeuristicSearch<BR>search.error_path = 
error.xml<BR>search.heuristic.branch.count_early = 
true<BR>search.heuristic.branch.no_branch_return = 
-1<BR>search.heuristic.class = 
gov.nasa.jpf.search.heuristic.Interleaving<BR>search.heuristic.comparator.class 
= 
gov.nasa.jpf.search.heuristic.DefaultComparator<BR>search.heuristic.queue_limit 
= -1<BR>search.match_depth = false<BR>search.min_free = 
1M<BR>search.multiple_errors = false<BR>search.print_errors = 
true<BR>search.properties = 
gov.nasa.jpf.jvm.NotDeadlockedProperty:gov.nasa.jpf.jvm.NoAssertionViolatedPrope<BR>rty:gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty<BR>vm.atomic_init 
= true<BR>vm.attributor.class = 
gov.nasa.jpf.jvm.DefaultAttributor<BR>vm.bootclasspath = 
G:javapathfinderjavapathfinderbuildenvjpf<BR>vm.check_fp = 
false<BR>vm.check_fp_compare = true<BR>vm.class = 
gov.nasa.jpf.jvm.JVM<BR>vm.classpath = 
build/examples<BR>vm.enable_assertions = *<BR>vm.finalize = true<BR>vm.gc = 
true<BR>vm.halt_on_throw = false<BR>vm.path_output = false<BR>vm.por = 
true<BR>vm.por.field_boundaries = true<BR>vm.por.fieldlockinfo.class = 
gov.nasa.jpf.jvm.StatisticFieldLockInfo<BR>vm.por.sync_detection = 
true<BR>vm.report.printStacks = true<BR>vm.report.show_bytecode = 
false<BR>vm.report.show_missing_lines = false<BR>vm.report.show_steps = 
true<BR>vm.scheduler.class = 
gov.nasa.jpf.jvm.DefaultScheduler<BR>vm.scheduler.random_seed = 
0<BR>vm.scheduler.use_time_for_seed = false<BR>vm.storage.class = 
gov.nasa.jpf.jvm.Md5StateSet<BR>vm.tree_output = 
true<BR>vm.verify.ignore_path = true<BR>vm.visible_asserts = 
false<BR>----------- free 
arguments<BR>-show<BR>DiningPhilosophers.DiningPhilosophers<BR>JPF 
configuration error: error instantiating class 
gov.nasa.jpf.search.heuristic.Interleaving for en<BR>try 
"search.heuristic.class":no suitable ctor found<BR>&gt; used within 
"search.class" instantiation of class 
gov.nasa.jpf.search.heuristic.HeuristicSearch</DIV>
<DIV class=RTE>&nbsp;</DIV>
<DIV class=RTE>&nbsp;</DIV>
<DIV class=RTE>&nbsp;</DIV>
<DIV class=RTE>&nbsp;</DIV>
<DIV class=RTE>Thanks.</DIV>
<DIV class=RTE>&nbsp;</DIV>
<DIV class=RTE>Wanglei</DIV>
<DIV class=RTE>&nbsp;</DIV>
<DIV class=RTE>2005-08-09</DIV></div><br clear=all><hr>免费下载  <a 
href="http://g.msn.com/8HMACNCN/2746??PS=47575" target="_top">MSN Explorer 
</a> Get 2 months FREE*. </html>