diff --git a/prism/src/explicit/STPGAbstractRefine.java b/prism/src/explicit/QuantAbstractRefine.java similarity index 93% rename from prism/src/explicit/STPGAbstractRefine.java rename to prism/src/explicit/QuantAbstractRefine.java index 2cbec8e9..b87bec6b 100644 --- a/prism/src/explicit/STPGAbstractRefine.java +++ b/prism/src/explicit/QuantAbstractRefine.java @@ -33,7 +33,24 @@ import prism.*; import explicit.StateModelChecker.TermCrit; import explicit.StateModelChecker.ValIterDir; -public abstract class STPGAbstractRefine +/** + * Base class for implementing quantitative abstraction-refinement loop. + * Subclasses need to implement the following abstract methods: + * + * Various settings are available. In particular, model/property type should be set with: + * + * See other setXXX methods for further configuration options. + *

+ * The abstraction-refinement loop can then be started with {@link #abstractRefine}. + */ +public abstract class QuantAbstractRefine { // Log for output (default: just send to stdout) protected PrismLog mainLog = new PrismPrintStreamLog(System.out); @@ -44,12 +61,6 @@ public abstract class STPGAbstractRefine // Flags/settings - // Model type - protected ModelType modelType = ModelType.MDP; - // Property type - protected PropertyType propertyType = PropertyType.PROB_REACH; - // Bound for when property is bounded reachabilty - protected int reachBound = 0; // Verbosity level protected int verbosity = 0; // Maximum number of refinement iterations @@ -91,13 +102,24 @@ public abstract class STPGAbstractRefine ALL, VAL }; - // Objects needed for abstraction refinement - // (abstract model, target states) + // Concrete model info + /** Type of (concrete) model; default is MDP. */ + protected ModelType modelType = ModelType.MDP; + + // Property info + /** Property type; default is PROB_REACH */ + protected PropertyType propertyType = PropertyType.PROB_REACH; + /** For nondeterministic (concrete) models, compute min? (or max?) */ + protected boolean min; + /** Bound for when property is bounded reachability */ + protected int reachBound = 0; + + // Abstract model info (updated by subclasses) + /** Abstract model */ protected ModelSimple abstraction; + /** BitSet of (abstract) target states for property to drive refinement */ protected BitSet target; - // Other parameters - protected boolean min; - protected boolean buildEmbeddedDtmc = false; // Construct DTMC from CTMC? + // Stuff for refinement loop protected ModelType abstractionType; protected double[] lbSoln; @@ -108,6 +130,7 @@ public abstract class STPGAbstractRefine protected double ubInit; protected BitSet known; protected List refineStates; + protected boolean buildEmbeddedDtmc = false; // Construct DTMC from CTMC? // Timing info, etc. protected double timeBuild; protected double timeRebuild; @@ -124,7 +147,7 @@ public abstract class STPGAbstractRefine /** * Default constructor. */ - public STPGAbstractRefine() + public QuantAbstractRefine() { // By default, log output goes to System.out. setLog(new PrismPrintStreamLog(System.out)); @@ -333,39 +356,44 @@ public abstract class STPGAbstractRefine // Abstract methods that must be implemented for abstraction-refinement loop /** - * Initialise: Build initial abstraction and set of target abstract states. - * (storing in abstraction and target, respectively). - * Note: abstraction must respect initial states, + * Initialise: Build initial abstraction and set of target abstract states + * (storing in {@link #abstraction} and {@link #target}, respectively). + * Note: {@link #abstraction} must respect initial states, * i.e. any abstract state contains either all/no initial states. */ protected abstract void initialise() throws PrismException; /** * 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., - * add new states to the abstraction and update the set of initial/target states appropriately. + * This function should add new states to the abstract model ({@link #abstraction}), + * update its initial states and update the {@link #target}. Any information stored locally + * about abstract state space etc. should also be updated at this point. + *

* 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. + * or left until later. If the former, the state should be added to the list {@code rebuiltStates}; + * if the latter, it should be added to {@code rebuildStates}. * The total number of new states should be returned. + *

* Notes: - * # 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). + * + * @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 rebuiltStates, Set rebuildStates) throws PrismException; /** * Rebuild the abstraction after a refinement. - * @param rebuildStates: States that need rebuilding. + * @param rebuildStates States that need rebuilding. */ protected abstract void rebuildAbstraction(Set rebuildStates) throws PrismException; @@ -889,7 +917,7 @@ public abstract class STPGAbstractRefine /** * Refine a set of states. - * @param refineState: States to refine. + * @param refineState States to refine. */ protected void refine(List refineStates) throws PrismException { @@ -939,10 +967,10 @@ public abstract class STPGAbstractRefine * 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 have been or will need to be rebuilt as a result. - * @param refineState: State to refine. - * @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). + * @param refineState State to refine. + * @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 rebuiltStates, Set rebuildStates) throws PrismException diff --git a/prism/src/pta/PTAAbstractRefine.java b/prism/src/pta/PTAAbstractRefine.java index 76e37eaa..5f2b1d71 100644 --- a/prism/src/pta/PTAAbstractRefine.java +++ b/prism/src/pta/PTAAbstractRefine.java @@ -28,6 +28,7 @@ package pta; import java.util.*; +import prism.ModelType; import prism.PrismException; import explicit.*; @@ -35,7 +36,7 @@ import explicit.*; * Probabilistic reachability for PTAs, using abstraction/refinement of stochastic games. * See: "Stochastic Games for Verification of Probabilistic Timed Automata" (FORMATS'09). */ -public class PTAAbstractRefine extends STPGAbstractRefine +public class PTAAbstractRefine extends QuantAbstractRefine { // PTA, target info protected PTA pta = null; @@ -51,6 +52,16 @@ public class PTAAbstractRefine extends STPGAbstractRefine // bit of time, but at the expense of some space). boolean storeValidZones = true; + /** + * Default constructor. + */ + public PTAAbstractRefine() + { + // Just do basic config for QuantAbstractRefine + setModelType(ModelType.MDP); + setPropertyType(QuantAbstractRefine.PropertyType.PROB_REACH); + } + /** * Compute min/max PTA reachability probabilities using STPG abstraction refinement. */ @@ -68,6 +79,7 @@ public class PTAAbstractRefine extends STPGAbstractRefine // Implementation of initialise() for abstraction-refinement loop; see superclass for details + @Override protected void initialise() throws PrismException { ForwardsReach forwardsReach; @@ -110,6 +122,7 @@ public class PTAAbstractRefine extends STPGAbstractRefine // Implementation of rebuildAbstraction(...) for abstraction-refinement loop; see superclass for details + @Override protected void rebuildAbstraction(Set rebuildStates) throws PrismException { for (int src : rebuildStates) { @@ -270,6 +283,7 @@ public class PTAAbstractRefine extends STPGAbstractRefine // - abstraction (new states, initial states and transitions) // - target set + @Override protected int splitState(int splitState, List> choiceLists, Set rebuiltStates, Set rebuildStates) throws PrismException {