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
>