From 11e0bf3d60f0bfa4dfff8cbc11a8b8bbd2859f79 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 19 Jul 2013 20:29:27 +0000 Subject: [PATCH] Small fixes and output changes to DTMC-LTL m/c. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7094 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 836df459..7206f34b 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -248,18 +248,19 @@ public class DTMCModelChecker extends ProbModelChecker modelProduct = pair.first; int invMap[] = pair.second; int modelProductSize = modelProduct.getNumStates(); + mainLog.print("\n" + modelProduct.infoStringTable()); + mainLog.print(modelProduct); // Find accepting BSCCs + compute reachability probabilities mainLog.println("\nFinding accepting BSCCs..."); BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCs(dra, modelProduct, invMap, sccMethod); - mainLog.println(acceptingBSCCs); mainLog.println("\nComputing reachability probabilities..."); mcProduct = new DTMCModelChecker(); probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acceptingBSCCs).soln, modelProduct); // Mapping probabilities in the original model double[] probsProductDbl = probsProduct.getDoubleArray(); - double[] probsDbl = new double[modelProductSize]; + double[] probsDbl = new double[model.getNumStates()]; LinkedList queue = new LinkedList(); for (int s : model.getInitialStates())