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

Some tidying in multi-objective code. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10810 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
ec285b66b1
commit
2de15e6b68
1 changed files with 8 additions and 31 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 39
      prism/src/prism/MultiObjModelChecker.java

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

@ -36,18 +36,18 @@ import java.util.BitSet;
import java.util.List; import java.util.List;
import java.util.Vector; import java.util.Vector;
import acceptance.AcceptanceRabin;
import automata.DA;
import automata.LTL2DA;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
import mtbdd.PrismMTBDD;
import parser.ast.Expression; import parser.ast.Expression;
import parser.ast.RelOp; import parser.ast.RelOp;
import dv.DoubleVector;
import mtbdd.PrismMTBDD;
import sparse.NDSparseMatrix; import sparse.NDSparseMatrix;
import sparse.PrismSparse; import sparse.PrismSparse;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
import acceptance.AcceptanceRabin;
import automata.DA;
import automata.LTL2DA;
import dv.DoubleVector;
/** /**
* Multi-objective model checking functionality * Multi-objective model checking functionality
@ -800,17 +800,6 @@ public class MultiObjModelChecker extends PrismComponent
double[] weights = new double[dimProb + dimReward]; double[] weights = new double[dimProb + dimReward];
weights[i] = 1.0; weights[i] = 1.0;
/*if (prism.getMDPMultiSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
//System.out.println("Doing GS");
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, new DoubleVector[] {probDoubleVectors[i]}, new int[] {probStepBounds[i]}, null,
new double[] { 1.0 }, null);
} else {
//System.out.println("Not doing GS");
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, new DoubleVector[] {probDoubleVectors[i]}, new int[] {probStepBounds[i]}, null,
new double[] { 1.0 }, null);
}*/
if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) { if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) {
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
@ -838,18 +827,6 @@ public class MultiObjModelChecker extends PrismComponent
double[] result; double[] result;
double[] weights = new double[dimProb + dimReward]; double[] weights = new double[dimProb + dimReward];
weights[i] = 1.0; weights[i] = 1.0;
/*System.out.println(prism.getMDPSolnMethod());
if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
//System.out.println("Doing GS");
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, null, null, new NDSparseMatrix[] { rewSparseMatrices[i] },
new double[] { 1.0 }, new int[] { rewardStepBounds[i] });
} else {
//System.out.println("Not doing GS");
result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, null, null, new NDSparseMatrix[] { rewSparseMatrices[i] },
new double[] { 1.0 }, new int[] { rewardStepBounds[i] });
}*/
if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) { if (settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD) == Prism.MDP_MULTI_GAUSSSEIDEL) {
result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(), result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights, modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,

Write Preview
Loading…
Cancel
Save