From f8cf00708e337b40983220894bd2ea71a7fedd4d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 5 Mar 2010 11:37:50 +0000 Subject: [PATCH] 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 --- .../src/explicit/PrismSTPGAbstractRefine.java | 58 ++++++++++++------- prism/src/explicit/STPGAbstractRefine.java | 44 +++++++------- 2 files changed, 61 insertions(+), 41 deletions(-) diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java index 59790e85..d8e96c60 100644 --- a/prism/src/explicit/PrismSTPGAbstractRefine.java +++ b/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> choiceLists, Set rebuildStates) - throws PrismException + protected int splitState(int splitState, List> choiceLists, Set rebuiltStates, + Set rebuildStates) throws PrismException { List> list, listNew; Set concreteStates, concreteStatesNew; @@ -221,9 +225,6 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine if (verbosity >= 1) mainLog.println("Splitting: #" + splitState); - // TODO: this is tmp - Set rebuildStatesTmp = new HashSet(); - // 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 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 diff --git a/prism/src/explicit/STPGAbstractRefine.java b/prism/src/explicit/STPGAbstractRefine.java index 69d97d31..28abe135 100644 --- a/prism/src/explicit/STPGAbstractRefine.java +++ b/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> choiceLists, Set rebuildStates) + protected abstract int splitState(int splitState, List> choiceLists, Set rebuiltStates, Set rebuildStates) throws PrismException; /** @@ -500,7 +499,7 @@ public abstract class STPGAbstractRefine else { HashSet rebuildStates = new HashSet(); 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 refineStates) throws PrismException { - Set rebuildStates; + Set 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(); rebuildStates = new LinkedHashSet(); 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 rebuildStates) throws PrismException + protected int refineState(int refineState, Set rebuiltStates, Set rebuildStates) throws PrismException { List> choiceLists; List 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]);