s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Dave Parker 11 years ago
parent
7eef2a266c
commit
d0f3e91387
7 changed files with 79 additions and 74 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      prism/src/explicit/DTMCModelChecker.java
  2. 80
      prism/src/explicit/Distribution.java
  3. 4
      prism/src/explicit/MDPModelChecker.java
  4. 2
      prism/src/explicit/ModelSimple.java
  5. 2
      prism/src/explicit/ProbModelChecker.java
  6. 19
      prism/src/explicit/STPGModelChecker.java
  7. 42
      prism/src/explicit/StateModelChecker.java

4
prism/src/explicit/DTMCModelChecker.java
View File

@ -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;
/**

80
prism/src/explicit/Distribution.java
View File

@ -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<Entry<Integer,Double>>
public class Distribution implements Iterable<Entry<Integer, Double>>
{
private HashMap<Integer,Double> map;
private HashMap<Integer, Double> map;
/**
* Create an empty distribution.
*/
@ -46,20 +50,20 @@ public class Distribution implements Iterable<Entry<Integer,Double>>
{
clear();
}
/**
* Copy constructor.
*/
public Distribution(Distribution distr)
{
this();
Iterator<Entry<Integer,Double>> i = distr.iterator();
Iterator<Entry<Integer, Double>> i = distr.iterator();
while (i.hasNext()) {
Map.Entry<Integer,Double> e = i.next();
Map.Entry<Integer, Double> 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<Entry<Integer,Double>>
public Distribution(Distribution distr, int permut[])
{
this();
Iterator<Entry<Integer,Double>> i = distr.iterator();
Iterator<Entry<Integer, Double>> i = distr.iterator();
while (i.hasNext()) {
Map.Entry<Integer,Double> e = i.next();
Map.Entry<Integer, Double> e = i.next();
add(permut[e.getKey()], e.getValue());
}
}
/**
* Clear all entries of the distribution.
*/
public void clear()
{
map = new HashMap<Integer,Double>();
map = new HashMap<Integer, Double>();
}
/**
* 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<Entry<Integer,Double>>
{
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<Entry<Integer,Double>>
{
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<Entry<Integer,Double>> i = iterator();
Iterator<Entry<Integer, Double>> i = iterator();
while (i.hasNext()) {
Map.Entry<Integer,Double> e = i.next();
Map.Entry<Integer, Double> 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<Entry<Integer,Double>> i = iterator();
Iterator<Entry<Integer, Double>> i = iterator();
while (i.hasNext()) {
Map.Entry<Integer,Double> e = i.next();
Map.Entry<Integer, Double> 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<Entry<Integer,Double>>
{
return map.keySet();
}
/**
* Get an iterator over the entries of the map defining the distribution.
*/
public Iterator<Entry<Integer,Double>> iterator()
public Iterator<Entry<Integer, Double>> iterator()
{
return map.entrySet().iterator();
}
@ -181,7 +185,7 @@ public class Distribution implements Iterable<Entry<Integer,Double>>
{
return map.isEmpty();
}
/**
* Get the size of the support of the distribution.
*/
@ -189,36 +193,36 @@ public class Distribution implements Iterable<Entry<Integer,Double>>
{
return map.size();
}
/**
* Get the sum of the probabilities in the distribution.
*/
public double sum()
{
double d = 0.0;
Iterator<Entry<Integer,Double>> i = iterator();
Iterator<Entry<Integer, Double>> i = iterator();
while (i.hasNext()) {
Map.Entry<Integer,Double> e = i.next();
Map.Entry<Integer, Double> 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<Entry<Integer,Double>> i = iterator();
Iterator<Entry<Integer, Double>> i = iterator();
while (i.hasNext()) {
Map.Entry<Integer,Double> e = i.next();
Map.Entry<Integer, Double> 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<Entry<Integer,Double>>
public Distribution map(int map[])
{
Distribution distrNew = new Distribution();
Iterator<Entry<Integer,Double>> i = iterator();
Iterator<Entry<Integer, Double>> i = iterator();
while (i.hasNext()) {
Map.Entry<Integer,Double> e = i.next();
Map.Entry<Integer, Double> 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<Entry<Integer,Double>>
Distribution d = (Distribution) o;
if (d.size() != size())
return false;
Iterator<Entry<Integer,Double>> i = iterator();
Iterator<Entry<Integer, Double>> i = iterator();
while (i.hasNext()) {
Map.Entry<Integer,Double> e = i.next();
Map.Entry<Integer, Double> 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<Entry<Integer,Double>>
}
return true;
}
@Override
public int hashCode()
{

4
prism/src/explicit/MDPModelChecker.java
View File

@ -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;

2
prism/src/explicit/ModelSimple.java
View File

@ -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).
*/

2
prism/src/explicit/ProbModelChecker.java
View File

@ -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;

19
prism/src/explicit/STPGModelChecker.java
View File

@ -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;

42
prism/src/explicit/StateModelChecker.java
View File

@ -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<String> propNames;
private List<BitSet> propBSs;
public CheckMaximalPropositionalFormulas(StateModelChecker mc, Model model, List<String> propNames, List<BitSet> 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.)

Write Preview
Loading…
Cancel
Save