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

Some tidying in multi-objective code (auto format). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10809 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
e932ae1227
commit
ec285b66b1
1 changed files with 96 additions and 97 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. 91
      prism/src/prism/MultiObjModelChecker.java

91
prism/src/prism/MultiObjModelChecker.java
View File

@ -68,8 +68,9 @@ public class MultiObjModelChecker extends PrismComponent
}
//TODO: dra's element is changed here, not neat.
protected NondetModel constructDRAandProductMulti(NondetModel model, LTLModelChecker mcLtl, ModelChecker modelChecker, Expression ltl, int i, DA<BitSet,AcceptanceRabin> dra[], Operator operator,
Expression targetExpr, JDDVars draDDRowVars, JDDVars draDDColVars, JDDNode ddStateIndex) throws PrismException
protected NondetModel constructDRAandProductMulti(NondetModel model, LTLModelChecker mcLtl, ModelChecker modelChecker, Expression ltl, int i,
DA<BitSet, AcceptanceRabin> dra[], Operator operator, Expression targetExpr, JDDVars draDDRowVars, JDDVars draDDColVars, JDDNode ddStateIndex)
throws PrismException
{
// TODO (JK): Adapt to support simple path formulas with bounds via DRA construction
@ -87,7 +88,7 @@ public class MultiObjModelChecker extends PrismComponent
long l = System.currentTimeMillis();
LTL2DA ltl2da = new LTL2DA(this);
dra[i] = ltl2da.convertLTLFormulaToDRA(ltl, modelChecker.getConstantValues());
mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getAcceptance().getSizeStatistics()+".");
mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getAcceptance().getSizeStatistics() + ".");
l = System.currentTimeMillis() - l;
mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");
// If required, export DRA
@ -169,7 +170,7 @@ public class MultiObjModelChecker extends PrismComponent
//computes accepting end component for the Rabin automaton dra.
//Vojta: in addition to calling a method which does the computation
//there are some other bits which I don't currently understand
protected JDDNode computeAcceptingEndComponent(DA<BitSet,AcceptanceRabin> dra, NondetModel modelProduct, JDDVars draDDRowVars, JDDVars draDDColVars,
protected JDDNode computeAcceptingEndComponent(DA<BitSet, AcceptanceRabin> dra, NondetModel modelProduct, JDDVars draDDRowVars, JDDVars draDDColVars,
List<JDDNode> allecs, List<JDDNode> statesH, List<JDDNode> statesL, //Vojta: at the time of writing this I have no idea what these two parameters do, so I don't know how to call them
LTLModelChecker mcLtl, boolean conflictformulaeGtOne, String name) throws PrismException
{
@ -190,7 +191,7 @@ public class MultiObjModelChecker extends PrismComponent
}
protected void removeNonZeroMecsForMax(NondetModel modelProduct, LTLModelChecker mcLtl, List<JDDNode> rewardsIndex, OpsAndBoundsList opsAndBounds,
int numTargets, DA<BitSet,AcceptanceRabin> dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[]) throws PrismException
int numTargets, DA<BitSet, AcceptanceRabin> dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[]) throws PrismException
{
List<JDDNode> mecs = mcLtl.findMECStates(modelProduct, modelProduct.getReach());
JDDNode removedActions = JDD.Constant(0);
@ -234,7 +235,7 @@ public class MultiObjModelChecker extends PrismComponent
Vector<JDDNode> tmptargetDDs = new Vector<JDDNode>();
List<JDDNode> tmpmultitargetDDs = new ArrayList<JDDNode>();
List<Integer> tmpmultitargetIDs = new ArrayList<Integer>();
ArrayList<DA<BitSet,AcceptanceRabin>> tmpdra = new ArrayList<DA<BitSet,AcceptanceRabin>>();
ArrayList<DA<BitSet, AcceptanceRabin>> tmpdra = new ArrayList<DA<BitSet, AcceptanceRabin>>();
ArrayList<JDDVars> tmpdraDDRowVars = new ArrayList<JDDVars>();
ArrayList<JDDVars> tmpdraDDColVars = new ArrayList<JDDVars>();
int count = 0;
@ -248,7 +249,7 @@ public class MultiObjModelChecker extends PrismComponent
}
if (count > 0) {
// TODO: distinguish whether rtarget is empty
DA<BitSet,AcceptanceRabin> newdra[] = new DA[count];
DA<BitSet, AcceptanceRabin> newdra[] = new DA[count];
tmpdra.toArray(newdra);
JDDVars newdraDDRowVars[] = new JDDVars[count];
tmpdraDDRowVars.toArray(newdraDDRowVars);
@ -262,7 +263,8 @@ public class MultiObjModelChecker extends PrismComponent
for (int i = 0; i < opsAndBounds.probSize(); i++) {
if (opsAndBounds.getProbOperator(i) != Operator.P_MAX) {
tmpOpsAndBounds.add(opsAndBounds.getOpRelOpBound(i), opsAndBounds.getProbOperator(i), opsAndBounds.getProbBound(i), opsAndBounds.getProbStepBound(i));
tmpOpsAndBounds.add(opsAndBounds.getOpRelOpBound(i), opsAndBounds.getProbOperator(i), opsAndBounds.getProbBound(i),
opsAndBounds.getProbStepBound(i));
}
}
tmpOpsAndBounds.add(new OpRelOpBound("R", RelOp.MAX, -1.0), Operator.R_MAX, -1.0, -1);
@ -302,11 +304,11 @@ public class MultiObjModelChecker extends PrismComponent
//TODO is conflictformulae actually just no of prob?
protected void checkConflictsInObjectives(NondetModel modelProduct, LTLModelChecker mcLtl, int conflictformulae, int numTargets,
OpsAndBoundsList opsAndBounds, DA<BitSet,AcceptanceRabin> dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List<JDDNode> targetDDs,
OpsAndBoundsList opsAndBounds, DA<BitSet, AcceptanceRabin> dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List<JDDNode> targetDDs,
List<ArrayList<JDDNode>> allstatesH, List<ArrayList<JDDNode>> allstatesL, List<JDDNode> multitargetDDs, List<Integer> multitargetIDs)
throws PrismException
{
DA<BitSet,AcceptanceRabin>[] tmpdra = new DA[conflictformulae];
DA<BitSet, AcceptanceRabin>[] tmpdra = new DA[conflictformulae];
JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae];
JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae];
List<JDDNode> tmptargetDDs = new ArrayList<JDDNode>(conflictformulae);
@ -354,9 +356,9 @@ public class MultiObjModelChecker extends PrismComponent
}
}
protected void findTargetStates(NondetModel modelProduct, LTLModelChecker mcLtl, int numTargets, int conflictformulae, boolean reachExpr[], DA<BitSet,AcceptanceRabin> dra[],
JDDVars draDDRowVars[], JDDVars draDDColVars[], List<JDDNode> targetDDs, List<JDDNode> multitargetDDs, List<Integer> multitargetIDs)
throws PrismException
protected void findTargetStates(NondetModel modelProduct, LTLModelChecker mcLtl, int numTargets, int conflictformulae, boolean reachExpr[],
DA<BitSet, AcceptanceRabin> dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List<JDDNode> targetDDs, List<JDDNode> multitargetDDs,
List<Integer> multitargetIDs) throws PrismException
{
int i, j;
long l;
@ -459,7 +461,7 @@ public class MultiObjModelChecker extends PrismComponent
// check if there are conflicts in objectives
if (conflictformulae > 1) {
DA<BitSet,AcceptanceRabin>[] tmpdra = new DA[conflictformulae];
DA<BitSet, AcceptanceRabin>[] tmpdra = new DA[conflictformulae];
JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae];
JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae];
List<JDDNode> tmptargetDDs = new ArrayList<JDDNode>(conflictformulae);
@ -679,8 +681,7 @@ public class MultiObjModelChecker extends PrismComponent
double time = ((double) (timePost - timePre)) / 1000.0;
mainLog.println("Multi-objective value iterations took " + time + " s.");
} else {
throw new PrismException("Don't know how to model-check using the method: "
+ method);
throw new PrismException("Don't know how to model-check using the method: " + method);
}
} catch (PrismException e) {
throw e;
@ -701,8 +702,8 @@ public class MultiObjModelChecker extends PrismComponent
return value;
}
protected Object weightedMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, JDDNode st, JDDNode[] targets, List<JDDNode> rewards, OpsAndBoundsList opsAndBounds)
throws PrismException
protected Object weightedMultiReachProbs(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, JDDNode st, JDDNode[] targets, List<JDDNode> rewards,
OpsAndBoundsList opsAndBounds) throws PrismException
{
int numberOfMaximizing = opsAndBounds.numberOfNumerical();
@ -730,7 +731,6 @@ public class MultiObjModelChecker extends PrismComponent
for (int i = 0; i < probStepBounds.length; i++)
probStepBounds[i] = opsAndBounds.getProbStepBound(i);
double timer = System.currentTimeMillis();
boolean min = false;
@ -812,13 +812,13 @@ public class MultiObjModelChecker extends PrismComponent
new double[] { 1.0 }, null);
}*/
if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) {
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
rewardStepBounds);
} else {
result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
rewardStepBounds);
}
//The following is thrown because in this case the i-th dimension is
@ -851,13 +851,13 @@ public class MultiObjModelChecker extends PrismComponent
new double[] { 1.0 }, new int[] { rewardStepBounds[i] });
}*/
if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) {
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
rewardStepBounds);
} else {
result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
rewardStepBounds);
}
numberOfPoints++;
@ -894,13 +894,13 @@ public class MultiObjModelChecker extends PrismComponent
double[] result;
if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
rewardStepBounds);
} else {
result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
rewardStepBounds);
}
/* //Minimizing operators are negated, and for Pareto we need to maximize.
@ -976,7 +976,6 @@ public class MultiObjModelChecker extends PrismComponent
for (int i = 0; i < probStepBounds.length; i++)
probStepBounds[i] = opsAndBounds.getProbStepBound(i);
double timer = System.currentTimeMillis();
boolean min = false;
@ -999,7 +998,8 @@ public class MultiObjModelChecker extends PrismComponent
boolean maximizingProb = (opsAndBounds.probSize() > 0 && (opsAndBounds.getProbOperator(0) == Operator.P_MAX || opsAndBounds.getProbOperator(0) == Operator.P_MIN));
boolean maximizingReward = (opsAndBounds.rewardSize() > 0 && (opsAndBounds.getRewardOperator(0) == Operator.R_MAX || opsAndBounds.getRewardOperator(0) == Operator.R_MIN));
boolean maximizingNegated = (maximizingProb && opsAndBounds.getProbOperator(0) == Operator.P_MIN) || (maximizingReward && opsAndBounds.getRewardOperator(0) == Operator.R_MIN);
boolean maximizingNegated = (maximizingProb && opsAndBounds.getProbOperator(0) == Operator.P_MIN)
|| (maximizingReward && opsAndBounds.getRewardOperator(0) == Operator.R_MIN);
int maxIters = settings.getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS);
@ -1103,13 +1103,13 @@ public class MultiObjModelChecker extends PrismComponent
double[] result;
if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
rewardStepBounds);
} else {
result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(),
modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), false, st, adversary,
trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, rewardStepBounds);
result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
rewardStepBounds);
}
numberOfPoints++;
@ -1123,7 +1123,6 @@ public class MultiObjModelChecker extends PrismComponent
computedPoints.add(newPoint);
computedDirections.add(direction);
//if (prism.getExportMultiGraphs())
// MultiObjUtils.printGraphFileDebug(targetPoint, computedPoints, computedDirections, prism.getExportMultiGraphsDir(), output++);

Write Preview
Loading…
Cancel
Save