Added -exactcheck and -rebuild=immed options for PRISM-AR (plus tweaks to A-R API wrt rebuilding).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1789 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/PrismSTPGAbstractRefine.java

@@ -41,13 +41,16 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 	protected String targetLabel; // PRISM label denoting target stares
 
 	// Flags/settings
-	protected boolean exact = false; // Just do model checking on the full concrete model
-
+	protected boolean exact = false; // Do model checking on the full concrete model?
+	protected boolean exactCheck = false; // Use exact result to check A-R result? (or just skip A-R?)
+	protected boolean rebuildImmed = false; // Rebuild split states immediately
+	
 	// Concrete model
 	protected Model modelConcrete;
 	protected int nConcrete; // Number of (concrete) states
 	protected BitSet initialConcrete; // Initial (concrete) states
 	protected BitSet targetConcrete; // Target (concrete) states
+	protected double exactInit; // Exact result for concrete model
 
 	// Abstraction info
 	// Map from concrete to abstract states
@@ -110,7 +113,8 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 		// If the 'exact' flag is set, just do model checking on the concrete model (no abstraction)
 		if (exact) {
 			doExactModelChecking();
-			throw new PrismException("Terminated early after exact verification");
+			if (!exactCheck)
+				throw new PrismException("Terminated early after exact verification");
 		}
 
 		// Build a mapping between concrete/abstract states
@@ -211,8 +215,8 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 
 	// Implementation of splitState(...) for abstraction-refinement loop; see superclass for details 
 
-	protected int splitState(int splitState, List<List<Integer>> choiceLists, Set<Integer> rebuildStates)
-			throws PrismException
+	protected int splitState(int splitState, List<List<Integer>> choiceLists, Set<Integer> rebuiltStates,
+			Set<Integer> rebuildStates) throws PrismException
 	{
 		List<Set<Integer>> list, listNew;
 		Set<Integer> concreteStates, concreteStatesNew;
@@ -221,9 +225,6 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 		if (verbosity >= 1)
 			mainLog.println("Splitting: #" + splitState);
 
-		// TODO: this is tmp
-		Set<Integer> rebuildStatesTmp = new HashSet<Integer>();
-
 		// Add an element to the list of choices
 		// corresponding to all remaining choices
 		addRemainderIntoChoiceLists(splitState, choiceLists);
@@ -248,8 +249,6 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 				a = nAbstract + i - 1;
 				abstractToConcrete.add(listNew);
 			}
-			rebuildStates.add(a); // TODO; and more!
-			rebuildStatesTmp.add(a);
 			//log.println(choiceList);
 			for (int j : choiceList) {
 				concreteStates = list.get(j);
@@ -267,7 +266,6 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 			mainLog.println(concreteToAbstract);
 		}
 
-		// TODO: who should do this?
 		// Add new states to the abstraction
 		abstraction.addStates(numNewStates - 1);
 		// Add new states to initial state set if needed
@@ -279,11 +277,18 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 		}
 
 		for (i = 0; i < nAbstract; i++) {
-			if (i == splitState || abstraction.isSuccessor(i, splitState))
-				rebuildAbstractionState(i);
+			if (i == splitState || abstraction.isSuccessor(i, splitState)) {
+				if (rebuildImmed)
+					rebuildAbstractionState(i);
+				else
+					rebuildStates.add(i);
+			}
 		}
 		for (i = 1; i < numNewStates; i++) {
-			rebuildAbstractionState(nAbstract + i - 1);
+			if (rebuildImmed)
+				rebuildAbstractionState(nAbstract + i - 1);
+			else
+				rebuildStates.add(nAbstract + i - 1);
 		}
 
 		return numNewStates;
@@ -293,12 +298,8 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 
 	protected void rebuildAbstraction(Set<Integer> rebuildStates) throws PrismException
 	{
-		int i;
-
-		//TODO: just rebuildStates?
-		//		for (int a : rebuildStates) {
-		for (i = 0; i < abstraction.getNumStates(); i++) {
-			rebuildAbstractionState(i);
+		for (int a : rebuildStates) {
+			rebuildAbstractionState(a);
 		}
 	}
 
@@ -398,6 +399,16 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 			mainLog.print(" " + res.soln[j]);
 		}
 		mainLog.println();
+
+		// Pick min/max value over all initial states
+		exactInit = min ? Double.POSITIVE_INFINITY : Double.NEGATIVE_INFINITY;
+		for (int j : modelConcrete.getInitialStates()) {
+			if (min) {
+				exactInit = Math.min(exactInit, res.soln[j]);
+			} else {
+				exactInit = Math.max(exactInit, res.soln[j]);
+			}
+		}
 	}
 
 	// Override this to also print out concrete model details at the end
@@ -406,6 +417,8 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 	{
 		mainLog.println("\nConcrete " + modelType + ": " + modelConcrete.infoString());
 		super.printFinalSummary(initAbstractionInfo, canRefine);
+		mainLog.print("Exact (concrete) result: " + exactInit);
+		mainLog.println(" (diff = " + Math.abs(exactInit - ((lbInit + ubInit) / 2)) + ")");
 	}
 
 	public static void main(String args[])
@@ -466,6 +479,11 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 						}
 					} else if (sw.equals("exact")) {
 						abstractRefine.exact = true;
+					} else if (sw.equals("exactcheck")) {
+						abstractRefine.exact = true;
+						abstractRefine.exactCheck = true;
+					} else if (sw.equals("rebuild=immed")) {
+						abstractRefine.rebuildImmed = true;
 					}
 
 					// Otherwise, try passing to abstraction-refinement engine

prism/src/explicit/STPGAbstractRefine.java

@@ -338,26 +338,25 @@ public abstract class STPGAbstractRefine
 
 	/**
 	 * Split an abstract state for refinement, based on sets of nondeterministic choices.
-	 * This function should update any information stored locally about abstract state space etc.
-	 * and then rebuild the abstraction and set of target states appropriately.
+	 * This function should update any information stored locally about abstract state space etc.,
+	 * add new states to the abstraction and update the set of initial/target states appropriately.
 	 * One of the new states should replace the state being split;
 	 * the rest should be appended to the list of abstract states.
-	 * 
+	 * Abstract states that need to be rebuilt (either because they are new, or because
+	 * one of their successors has been split) can either be rebuilt at this point,
+	 * or left until later. If the former, the state should be added to the list rebuiltStates;
+	 * if the latter, it should be added to rebuildStates.
 	 * The total number of new states should be returned.
 	 * Notes:
-	 *  # The union of all these sets may not cover all choices in the state to be split.
-	 *      This is because there may be more efficient ways to compute the remainder of the abstract state.
-	 *      If not, use the utility function addRemainderIntoChoiceLists(...).
-	 * 
-	 * TODO: what about:
-	 * (ii) work out which states of the abstraction will need rebuilding as a result
-	 * 
+	 *  # The union of all the sets in choiceLists may not cover all choices in the state to be split.
+	 *    This is because there may be more efficient ways to compute the remainder of the abstract state.
+	 *    If not, use the utility function addRemainderIntoChoiceLists(...).
 	 * @param splitState: State to split.
 	 * @param choiceLists: Lists of nondeterministic choices defining split.
 	 * @param rebuildStates: States that need rebuilding as a result should be added here.
 	 * @return: Number of states into which split (i.e. 1 denotes split failed).
 	 */
-	protected abstract int splitState(int splitState, List<List<Integer>> choiceLists, Set<Integer> rebuildStates)
+	protected abstract int splitState(int splitState, List<List<Integer>> choiceLists, Set<Integer> rebuiltStates, Set<Integer> rebuildStates)
 			throws PrismException;
 
 	/**
@@ -500,7 +499,7 @@ public abstract class STPGAbstractRefine
 				else {
 					HashSet<Integer> rebuildStates = new HashSet<Integer>();
 					timer = System.currentTimeMillis();
-					numNewStates = refineState(i, rebuildStates);
+					numNewStates = refineState(i, null, rebuildStates);
 					timer = System.currentTimeMillis() - timer;
 					timeRefine += timer / 1000.0;
 					if (numNewStates > 1) {
@@ -886,14 +885,15 @@ public abstract class STPGAbstractRefine
 	 */
 	protected void refine(List<Integer> refineStates) throws PrismException
 	{
-		Set<Integer> rebuildStates;
+		Set<Integer> rebuiltStates, rebuildStates;
 		int i, n, refineState, numNewStates, numSuccRefines;
 		long timer;
 
 		mainLog.println("\nRefinement " + refinementNum + "...");
 		timer = System.currentTimeMillis();
 
-		// Store list of game states that will need rebuilding
+		// Store lists of game states that have been or will need to be rebuilt
+		rebuiltStates = new LinkedHashSet<Integer>();
 		rebuildStates = new LinkedHashSet<Integer>();
 
 		numSuccRefines = 0;
@@ -903,7 +903,7 @@ public abstract class STPGAbstractRefine
 			if (verbosity >= 1)
 				mainLog.println("Refinement " + refinementNum + "." + (n - i) + "...");
 			refineState = refineStates.get(i);
-			numNewStates = refineState(refineState, rebuildStates);
+			numNewStates = refineState(refineState, rebuiltStates, rebuildStates);
 			if (numNewStates > 1)
 				numSuccRefines++;
 		}
@@ -913,10 +913,11 @@ public abstract class STPGAbstractRefine
 		mainLog.print(numSuccRefines + " states successfully refined");
 		mainLog.println(" in " + (timer / 1000.0) + " secs.");
 
+		// Rebuild any states as necessary
 		timer = System.currentTimeMillis();
 		if (verbosity >= 1)
 			mainLog.println("Rebuilding states: " + rebuildStates);
-		//rebuildAbstraction(rebuildStates);
+		rebuildAbstraction(rebuildStates);
 		timer = System.currentTimeMillis() - timer;
 		timeRebuild += timer / 1000.0;
 		mainLog.println(rebuildStates.size() + " states of " + abstractionType + " rebuilt in " + (timer / 1000.0)
@@ -928,12 +929,13 @@ public abstract class STPGAbstractRefine
 	 * Refine a single state, by splitting using the current refinement strategy.
 	 * Adds new states to abstraction (and updates initial states), updates target states,
 	 * and resizes/updates lb/ub solution vectors and 'known' set.
-	 * Also keeps track of which states of the abstraction will need rebuilding as a result.
+	 * Also keeps track of which states have been or will need to be rebuilt as a result.
 	 * @param refineState: State to refine.
-	 * @param rebuildStates: States that need rebuilding as a result should be added here.
+	 * @param rebuiltStates: States that have been rebuilt as a result will be added here.
+	 * @param rebuildStates: States that need rebuilding as a result will be added here.
 	 * @return: Number of states into which split (i.e. 1 denotes refinement failed).
 	 */
-	protected int refineState(int refineState, Set<Integer> rebuildStates) throws PrismException
+	protected int refineState(int refineState, Set<Integer> rebuiltStates, Set<Integer> rebuildStates) throws PrismException
 	{
 		List<List<Integer>> choiceLists;
 		List<Integer> lbStrat = null, ubStrat = null;
@@ -953,7 +955,7 @@ public abstract class STPGAbstractRefine
 		}
 
 		// Don't refine a state that we have already modified through refinement
-		if (rebuildStates.contains(refineState)) {
+		if (rebuiltStates.contains(refineState)) {
 			if (verbosity >= 1)
 				mainLog.println("Warning: Skipping refinement of #" + refineState
 						+ " which has already been modified by refinement.");
@@ -1076,7 +1078,7 @@ public abstract class STPGAbstractRefine
 		numStates = abstraction.getNumStates();
 
 		// Split the state, based on nondet choices selected above
-		numNewStates = splitState(refineState, choiceLists, rebuildStates);
+		numNewStates = splitState(refineState, choiceLists, rebuiltStates, rebuildStates);
 
 		// Update existing solution vectors (if any)
 		lbSoln = Utils.extendDoubleArray(lbSoln, numStates, numStates + numNewStates - 1, lbSoln[refineState]);