Menu
▾
▴
[Javapathfinder-user] Problem about Heuristic Search
|
From: <jel...@ho...> - 2005-08-09 23:14:01
|
<html><div style='background-color:'><DIV class=RTE>Hi,All</DIV> <DIV class=RTE> </DIV> <DIV class=RTE>I'm trying to model check the Dining Philosophers problem using heuristic search,and specify the heuristic class :</DIV> <DIV class=RTE>search.heuristic.class = gov.nasa.jpf.search.heuristic.Interleaving</DIV> <DIV class=RTE> </DIV> <DIV class=RTE>However,an error occurs when I run JPF.The printout is shown below:</DIV> <DIV class=RTE> </DIV> <DIV class=RTE> </DIV> <DIV class=RTE>G:\JPF\javapathfinder\examples>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>> used within "search.class" instantiation of class gov.nasa.jpf.search.heuristic.HeuristicSearch</DIV> <DIV class=RTE> </DIV> <DIV class=RTE> </DIV> <DIV class=RTE> </DIV> <DIV class=RTE> </DIV> <DIV class=RTE>Thanks.</DIV> <DIV class=RTE> </DIV> <DIV class=RTE>Wanglei</DIV> <DIV class=RTE> </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> |
