From: Wang L. <jel...@ho...> - 2005-08-12 04:06:06
|
<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>>From: Peter C.Mehlitz <pcm...@em...><BR>>To: ?纾 ?<jel...@ho...><BR>>CC: jav...@li...<BR>>Subject: Re: [Javapathfinder-user] Problem about Heuristic Search<BR>>Date: Wed, 10 Aug 2005 09:37:11 -0700<BR>><BR>>some of the Heuristic classes had non-public ctors, which caused <BR>>NoSuchMethodExceptions when instantiating via the Config based <BR>>reflection. Should be fixed in the repository (as always, the public <BR>> CVS takes a bit longer), but not all Heuristic instances have been <BR>> tested recently.<BR>><BR>>-- Peter<BR>><BR>><BR>>On Aug 9, 2005, at 1:40 AM, ?纾 ?wrote:<BR>><BR>>>Hi,All<BR>>><BR>>>I'm trying to model check the Dining Philosophers problem using <BR>>>heuristic search,and specify the heuristic class :<BR>>>search.heuristic.class = gov.nasa.jpf.search.heuristic.Interleaving<BR>>><BR>>>However,an error occurs when I run JPF.The printout is shown below:<BR>>><BR>>><BR>>>G:\JPF\javapathfinder\examples>java gov.nasa.jpf.JPF -c .. <BR>>>\default.properties -show DiningPhilosophers.DiningPhilosophers<BR>>>Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA <BR>>>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 = <BR>>>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 = <BR>>>gov.nasa.jpf.jvm.NotDeadlockedProperty:gov.nasa.jpf.jvm.NoAssertionVio <BR>>>latedPrope<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 = <BR>>>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 <BR>>>gov.nasa.jpf.search.heuristic.Interleaving for en<BR>>>try "search.heuristic.class":no suitable ctor found<BR>>> > used within "search.class" instantiation of class <BR>>>gov.nasa.jpf.search.heuristic.HeuristicSearch<BR>>><BR>>><BR>>><BR>>><BR>>>Thanks.<BR>>><BR>>>Wanglei<BR>>><BR>>>2005-08-09<BR>>><BR>>> 垂涓浇 MSN Explorer Get 2 months FREE*. <BR>>>------------------------------------------------------- SF.Net <BR>>>email is Sponsored by the Better Software Conference & EXPO <BR>>>September 19-22, 2005 * San Francisco, CA * Development Lifecycle <BR>>>Practices Agile & Plan-Driven Development * Managing Projects & <BR>>>Teams * Testing & QA Security * Process Improvement & Measurement * <BR>>> http://www.sqe.com/bsce5sf <BR>>>_______________________________________________ Javapathfinder-user <BR>>> mailing list Jav...@li... https:// <BR>>>lists.sourceforge.net/lists/listinfo/javapathfinder-user<BR>>><BR>><BR>><BR>><BR>><BR>>-------------------------------------------------------<BR>>SF.Net email is Sponsored by the Better Software Conference & EXPO<BR>>September 19-22, 2005 * San Francisco, CA * Development Lifecycle <BR>>Practices<BR>>Agile & Plan-Driven Development * Managing Projects & Teams * <BR>>Testing & QA<BR>>Security * Process Improvement & Measurement * <BR>>http://www.sqe.com/bsce5sf<BR>>_______________________________________________<BR>>Javapathfinder-user mailing list<BR>>Jav...@li...<BR>>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> |