From 4f3d2090e889761a9adde1edd1dd34b74fcbf0df Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 22 Feb 2010 10:15:16 +0000
Subject: [PATCH] A-R loop output tidy + bugfix (in PRISM version).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1764 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 .../src/explicit/PrismSTPGAbstractRefine.java  | 18 ++++++++++++------
 prism/src/explicit/STPGAbstractRefine.java     | 11 ++++++++---
 2 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java
index 98fc70e4..1a61c4d4 100644
--- a/prism/src/explicit/PrismSTPGAbstractRefine.java
+++ b/prism/src/explicit/PrismSTPGAbstractRefine.java
@@ -126,6 +126,11 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 		if (!existsInitial)
 			throw new PrismException("No non-target initial states");
 
+		if (verbosity >= 10) {
+			mainLog.print("Initial concreteToAbstract: ");
+			mainLog.println(concreteToAbstract);
+		}
+		
 		// Create (empty) abstraction and store initial states info
 		nAbstract = existsRest ? 3 : 2;
 		switch (modelType) {
@@ -180,7 +185,6 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 				list.add(new HashSet<Integer>(1));
 			list.get(j).add(c);
 		}
-		//mainLog.println(abstraction);
 	}
 
 	/**
@@ -255,10 +259,11 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 			}
 			i++;
 		}
-		/*log.print("concreteToAbstract:");
-		for (i = 0; i < nConcrete; i++)
-			log.print(" " + i + "=" + concreteToAbstract[i]);
-		log.println();*/
+		
+		if (verbosity >= 10) {
+			mainLog.print("New concreteToAbstract: ");
+			mainLog.println(concreteToAbstract);
+		}
 
 		// TODO: who should do this?
 		// Add new states to the abstraction
@@ -272,7 +277,7 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 		}
 
 		for (i = 0; i < nAbstract; i++) {
-			if (i == splitState || abstraction.isSuccessor(splitState, i))
+			if (i == splitState || abstraction.isSuccessor(i, splitState))
 				rebuildAbstractionState(i);
 		}
 		for (i = 1; i < numNewStates; i++) {
@@ -309,6 +314,7 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 			for (int c : concreteStates) {
 				a = concreteToAbstract[c];
 				// ASSERT: a = i ???
+				if (a != i) throw new PrismException("Oops");
 				switch (modelType) {
 				case DTMC:
 					distr = buildAbstractDistribution(c, (DTMC) modelConcrete);
diff --git a/prism/src/explicit/STPGAbstractRefine.java b/prism/src/explicit/STPGAbstractRefine.java
index 9777e929..190924b6 100644
--- a/prism/src/explicit/STPGAbstractRefine.java
+++ b/prism/src/explicit/STPGAbstractRefine.java
@@ -425,7 +425,7 @@ public abstract class STPGAbstractRefine
 		mainLog.println(abstractionType + " constructed in " + (timer / 1000.0) + " secs.");
 		timeBuild += timer / 1000.0;
 		mainLog.println(abstractionType + ": " + abstraction.infoString());
-		if (verbosity >= 5) {
+		if (verbosity >= 10) {
 			mainLog.println(abstractionType + ": " + abstraction);
 		}
 
@@ -451,6 +451,9 @@ public abstract class STPGAbstractRefine
 				break;
 			refinementNum++;
 			refine(refineStates);
+			if (verbosity >= 10) {
+				mainLog.println(abstractionType + ": " + abstraction);
+			}
 		}
 
 		// Finish up
@@ -477,6 +480,7 @@ public abstract class STPGAbstractRefine
 		while (i < n) {
 			// Pick next state
 			i = (known == null) ? i + 1 : known.nextClearBit(i + 1);
+			// TODO: check use of nextClearBit here
 			if (i < 0)
 				break;
 
@@ -563,12 +567,11 @@ public abstract class STPGAbstractRefine
 			known.set(i, PrismUtils.doublesAreClose(ubSoln[i], lbSoln[i], refineTermCritParam,
 					refineTermCrit == RefineTermCrit.ABSOLUTE));
 		}
-		mainLog.println(known.cardinality() + "/" + n + " states converged.");
 
 		// Compute bounds for initial states
 		lbInit = ubInit = min ? Double.POSITIVE_INFINITY : Double.NEGATIVE_INFINITY;
 		for (int j : abstraction.getInitialStates()) {
-			if (verbosity >= 5)
+			if (verbosity >= 10)
 				mainLog.println("Init " + j + ": " + lbSoln[j] + "-" + ubSoln[j]);
 			if (min) {
 				lbInit = Math.min(lbInit, lbSoln[j]);
@@ -585,6 +588,7 @@ public abstract class STPGAbstractRefine
 		mainLog.println(abstractionType + " model checked in " + (timer / 1000.0) + " secs.");
 
 		// Display results
+		mainLog.println(known.cardinality() + "/" + n + " states converged.");
 		numInitialStates = abstraction.getNumInitialStates();
 		mainLog.print("Diff across ");
 		mainLog.print(numInitialStates + " initial state" + (numInitialStates == 1 ? "" : "s") + ": ");
@@ -845,6 +849,7 @@ public abstract class STPGAbstractRefine
 			if (ubSoln[i] - lbSoln[i] >= bound && abstraction.getNumChoices(i) > 1)
 				refinableStates.add(i);
 		}
+		mainLog.println(refinableStates.size() + " refineable states.");
 		if (verbosity >= 1) {
 			mainLog.println("Refinable states: " + refinableStates);
 		}