From 49fb84b25d229059b755ab3f44c554bea500fb59 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 7 May 2010 14:55:51 +0000 Subject: [PATCH] MDPModelChecker uses init state to display results. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1888 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPModelChecker.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index c8a85a53..f1614199 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -642,7 +642,7 @@ public class MDPModelChecker extends StateModelChecker MDPModelChecker mc; MDPSimple mdp; ModelCheckerResult res; - BitSet target; + BitSet init, target; Map labels; boolean min = true; try { @@ -652,6 +652,7 @@ public class MDPModelChecker extends StateModelChecker //System.out.println(mdp); labels = mc.loadLabelsFile(args[1]); //System.out.println(labels); + init = labels.get("init"); target = labels.get(args[2]); if (target == null) throw new PrismException("Unknown label \"" + args[2] + "\""); @@ -664,7 +665,7 @@ public class MDPModelChecker extends StateModelChecker mc.setPrecomp(false); } res = mc.probReach(mdp, target, min); - System.out.println(res.soln[0]); + System.out.println(res.soln[init.nextSetBit(0)]); } catch (PrismException e) { System.out.println(e); }