From d0f3e91387fe2349aaff58e136cf404c1306175e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 23 Jun 2015 09:08:25 +0000 Subject: [PATCH] Some code tidying (automatic mostly) for merging purposes. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10067 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 4 +- prism/src/explicit/Distribution.java | 80 ++++++++++++----------- prism/src/explicit/MDPModelChecker.java | 4 +- prism/src/explicit/ModelSimple.java | 2 +- prism/src/explicit/ProbModelChecker.java | 2 +- prism/src/explicit/STPGModelChecker.java | 19 +++--- prism/src/explicit/StateModelChecker.java | 42 ++++++------ 7 files changed, 79 insertions(+), 74 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 5b900bd3..1038e10c 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -31,14 +31,14 @@ import java.util.BitSet; import java.util.List; import java.util.Map; -import acceptance.AcceptanceReach; -import acceptance.AcceptanceType; import parser.ast.Expression; import parser.type.TypeDouble; import prism.PrismComponent; import prism.PrismException; import prism.PrismNotSupportedException; import prism.PrismUtils; +import acceptance.AcceptanceReach; +import acceptance.AcceptanceType; import explicit.rewards.MCRewards; /** diff --git a/prism/src/explicit/Distribution.java b/prism/src/explicit/Distribution.java index be7c58f8..51311323 100644 --- a/prism/src/explicit/Distribution.java +++ b/prism/src/explicit/Distribution.java @@ -26,8 +26,12 @@ package explicit; -import java.util.*; +import java.util.BitSet; +import java.util.HashMap; +import java.util.Iterator; +import java.util.Map; import java.util.Map.Entry; +import java.util.Set; import prism.PrismUtils; @@ -35,10 +39,10 @@ import prism.PrismUtils; * Explicit representation of a probability distribution. * Basically, a mapping from (integer-valued) state indices to (non-zero, double-valued) probabilities. */ -public class Distribution implements Iterable> +public class Distribution implements Iterable> { - private HashMap map; - + private HashMap map; + /** * Create an empty distribution. */ @@ -46,20 +50,20 @@ public class Distribution implements Iterable> { clear(); } - + /** * Copy constructor. */ public Distribution(Distribution distr) { this(); - Iterator> i = distr.iterator(); + Iterator> i = distr.iterator(); while (i.hasNext()) { - Map.Entry e = i.next(); + Map.Entry e = i.next(); add(e.getKey(), e.getValue()); } } - + /** * Construct a distribution from an existing one and a state index permutation, * i.e. in which state index i becomes index permut[i]. @@ -69,21 +73,21 @@ public class Distribution implements Iterable> public Distribution(Distribution distr, int permut[]) { this(); - Iterator> i = distr.iterator(); + Iterator> i = distr.iterator(); while (i.hasNext()) { - Map.Entry e = i.next(); + Map.Entry e = i.next(); add(permut[e.getKey()], e.getValue()); } } - + /** * Clear all entries of the distribution. */ public void clear() { - map = new HashMap(); + map = new HashMap(); } - + /** * Add 'prob' to the probability for state 'j'. * Return boolean indicating whether or not there was already @@ -119,9 +123,9 @@ public class Distribution implements Iterable> { Double d; d = (Double) map.get(j); - return d==null ? 0.0 : d.doubleValue(); + return d == null ? 0.0 : d.doubleValue(); } - + /** * Returns true if index j is in the support of the distribution. */ @@ -129,35 +133,35 @@ public class Distribution implements Iterable> { return map.get(j) != null; } - + /** * Returns true if all indices in the support of the distribution are in the set. */ public boolean isSubsetOf(BitSet set) { - Iterator> i = iterator(); + Iterator> i = iterator(); while (i.hasNext()) { - Map.Entry e = i.next(); + Map.Entry e = i.next(); if (!set.get((Integer) e.getKey())) return false; } return true; } - + /** * Returns true if at least one index in the support of the distribution is in the set. */ public boolean containsOneOf(BitSet set) { - Iterator> i = iterator(); + Iterator> i = iterator(); while (i.hasNext()) { - Map.Entry e = i.next(); + Map.Entry e = i.next(); if (set.get((Integer) e.getKey())) return true; } return false; } - + /** * Get the support of the distribution. */ @@ -165,11 +169,11 @@ public class Distribution implements Iterable> { return map.keySet(); } - + /** * Get an iterator over the entries of the map defining the distribution. */ - public Iterator> iterator() + public Iterator> iterator() { return map.entrySet().iterator(); } @@ -181,7 +185,7 @@ public class Distribution implements Iterable> { return map.isEmpty(); } - + /** * Get the size of the support of the distribution. */ @@ -189,36 +193,36 @@ public class Distribution implements Iterable> { return map.size(); } - + /** * Get the sum of the probabilities in the distribution. */ public double sum() { double d = 0.0; - Iterator> i = iterator(); + Iterator> i = iterator(); while (i.hasNext()) { - Map.Entry e = i.next(); + Map.Entry e = i.next(); d += e.getValue(); } return d; } - + /** * Get the sum of all the probabilities in the distribution except for state j. */ public double sumAllBut(int j) { double d = 0.0; - Iterator> i = iterator(); + Iterator> i = iterator(); while (i.hasNext()) { - Map.Entry e = i.next(); + Map.Entry e = i.next(); if (e.getKey() != j) d += e.getValue(); } return d; } - + /** * Create a new distribution, based on a mapping from the state indices * used in this distribution to a different set of state indices. @@ -226,14 +230,14 @@ public class Distribution implements Iterable> public Distribution map(int map[]) { Distribution distrNew = new Distribution(); - Iterator> i = iterator(); + Iterator> i = iterator(); while (i.hasNext()) { - Map.Entry e = i.next(); + Map.Entry e = i.next(); distrNew.add(map[e.getKey()], e.getValue()); } return distrNew; } - + @Override public boolean equals(Object o) { @@ -241,9 +245,9 @@ public class Distribution implements Iterable> Distribution d = (Distribution) o; if (d.size() != size()) return false; - Iterator> i = iterator(); + Iterator> i = iterator(); while (i.hasNext()) { - Map.Entry e = i.next(); + Map.Entry e = i.next(); d1 = e.getValue(); d2 = d.map.get(e.getKey()); if (d2 == null || !PrismUtils.doublesAreClose(d1, d2, 1e-12, false)) @@ -251,7 +255,7 @@ public class Distribution implements Iterable> } return true; } - + @Override public int hashCode() { diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 2ee8d24d..ebea9184 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -31,8 +31,6 @@ import java.util.Iterator; import java.util.List; import java.util.Map; -import acceptance.AcceptanceReach; -import acceptance.AcceptanceType; import parser.ast.Expression; import prism.PrismComponent; import prism.PrismDevNullLog; @@ -41,6 +39,8 @@ import prism.PrismFileLog; import prism.PrismLog; import prism.PrismUtils; import strat.MDStrategyArray; +import acceptance.AcceptanceReach; +import acceptance.AcceptanceType; import explicit.rewards.MCRewards; import explicit.rewards.MCRewardsFromMDPRewards; import explicit.rewards.MDPRewards; diff --git a/prism/src/explicit/ModelSimple.java b/prism/src/explicit/ModelSimple.java index 750ee8c5..c3085fea 100644 --- a/prism/src/explicit/ModelSimple.java +++ b/prism/src/explicit/ModelSimple.java @@ -37,7 +37,7 @@ public interface ModelSimple extends Model * Add a state to the list of initial states. */ public abstract void addInitialState(int i); - + /** * Build (anew) from a list of transitions exported explicitly by PRISM (i.e. a .tra file). */ diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 5a721ed7..f36e73b2 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -42,8 +42,8 @@ import prism.IntegerBound; import prism.OpRelOpBound; import prism.PrismComponent; import prism.PrismException; -import prism.PrismSettings; import prism.PrismNotSupportedException; +import prism.PrismSettings; import explicit.rewards.ConstructRewards; import explicit.rewards.MCRewards; import explicit.rewards.MDPRewards; diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 2d834098..18e2821b 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -52,7 +52,7 @@ public class STPGModelChecker extends ProbModelChecker { super(parent); } - + // Model checking functions @Override @@ -60,7 +60,7 @@ public class STPGModelChecker extends ProbModelChecker { throw new PrismNotSupportedException("LTL model checking not yet supported for stochastic games"); } - + // Numerical computation functions /** @@ -79,7 +79,7 @@ public class STPGModelChecker extends ProbModelChecker long timer; timer = System.currentTimeMillis(); - + // Store num states n = stpg.getNumStates(); @@ -474,7 +474,7 @@ public class STPGModelChecker extends ProbModelChecker msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; throw new PrismException(msg); } - + // Print adversary if (genAdv) { PrismLog out = new PrismFileLog(exportAdvFilename); @@ -574,7 +574,7 @@ public class STPGModelChecker extends ProbModelChecker msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; throw new PrismException(msg); } - + // Return results res = new ModelCheckerResult(); res.soln = soln; @@ -741,7 +741,8 @@ public class STPGModelChecker extends ProbModelChecker * @param known Optionally, a set of states for which the exact answer is known * Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values. */ - public ModelCheckerResult computeReachRewards(STPG stpg, STPGRewards rewards, BitSet target, boolean min1, boolean min2, double init[], BitSet known) throws PrismException + public ModelCheckerResult computeReachRewards(STPG stpg, STPGRewards rewards, BitSet target, boolean min1, boolean min2, double init[], BitSet known) + throws PrismException { ModelCheckerResult res = null; BitSet inf; @@ -813,8 +814,8 @@ public class STPGModelChecker extends ProbModelChecker * @param known Optionally, a set of states for which the exact answer is known * Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values. */ - protected ModelCheckerResult computeReachRewardsValIter(STPG stpg, STPGRewards rewards, BitSet target, BitSet inf, boolean min1, boolean min2, double init[], BitSet known) - throws PrismException + protected ModelCheckerResult computeReachRewardsValIter(STPG stpg, STPGRewards rewards, BitSet target, BitSet inf, boolean min1, boolean min2, + double init[], BitSet known) throws PrismException { ModelCheckerResult res; BitSet unknown; @@ -887,7 +888,7 @@ public class STPGModelChecker extends ProbModelChecker msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; throw new PrismException(msg); } - + // Return results res = new ModelCheckerResult(); res.soln = soln; diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 91d04158..fb381d97 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -65,8 +65,8 @@ import prism.ModelType; import prism.PrismComponent; import prism.PrismException; import prism.PrismLangException; -import prism.PrismSettings; import prism.PrismNotSupportedException; +import prism.PrismSettings; import prism.Result; /** @@ -88,7 +88,7 @@ public class StateModelChecker extends PrismComponent // Store the final results vector after model checking? protected boolean storeVector = false; - + // Generate/store a strategy during model checking? protected boolean genStrat = false; @@ -116,13 +116,13 @@ public class StateModelChecker extends PrismComponent public StateModelChecker(PrismComponent parent) throws PrismException { super(parent); - + // For explicit.StateModelChecker and its subclasses, we explicitly set 'settings' // to null if there is no parent or if the parent has a null 'settings'. // This allows us to choose to ignore the default one created by PrismComponent. if (parent == null || parent.getSettings() == null) setSettings(null); - + // If present, initialise settings from PrismSettings if (settings != null) { verbosity = settings.getBoolean(PrismSettings.PRISM_VERBOSE) ? 10 : 1; @@ -294,7 +294,7 @@ public class StateModelChecker extends PrismComponent // Remove any existing filter info currentFilter = null; - + // Wrap a filter round the property, if needed // (in order to extract the final result of model checking) ExpressionFilter exprFilter = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumInitialStates() == 1); @@ -315,7 +315,7 @@ public class StateModelChecker extends PrismComponent mainLog.println("Modified property: " + exprNew); expr = exprNew; } - + // Do model checking and store result vector timer = System.currentTimeMillis(); // check expression for all states (null => statesOfInterest=all) @@ -1025,7 +1025,7 @@ public class StateModelChecker extends PrismComponent private Model model; private List propNames; private List propBSs; - + public CheckMaximalPropositionalFormulas(StateModelChecker mc, Model model, List propNames, List propBSs) { this.mc = mc; @@ -1033,57 +1033,57 @@ public class StateModelChecker extends PrismComponent this.propNames = propNames; this.propBSs = propBSs; } - + public Object visit(ExpressionITE e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + public Object visit(ExpressionBinaryOp e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + public Object visit(ExpressionUnaryOp e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + public Object visit(ExpressionFunc e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + public Object visit(ExpressionIdent e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + public Object visit(ExpressionLiteral e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + public Object visit(ExpressionConstant e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + public Object visit(ExpressionFormula e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + public Object visit(ExpressionVar e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + public Object visit(ExpressionLabel e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + public Object visit(ExpressionProp e) throws PrismLangException { // Look up property and recurse @@ -1094,12 +1094,12 @@ public class StateModelChecker extends PrismComponent throw new PrismLangException("Unknown property reference " + e, e); } } - + public Object visit(ExpressionFilter e) throws PrismLangException { return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); } - + /** * Evaluate this expression in all states (i.e. model check it), * store the resulting BitSet in the list {@code propBSs}, @@ -1137,7 +1137,7 @@ public class StateModelChecker extends PrismComponent return new ExpressionLabel(newLabelName); } } - + /** * Loads labels from a PRISM labels file and stores them in BitSet objects. * (Actually, it returns a map from label name Strings to BitSets.)