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

@@ -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<Integer> queue = new LinkedList<Integer>();
 		for (int s : model.getInitialStates())