From b91b8f0b12331cd37b98b1ea5a238f5420a58c24 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 30 Dec 2014 01:00:49 +0000 Subject: [PATCH] Re-factoring in multi-objective model checking. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9467 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 53 ++++++++++++------------- prism/src/prism/ProbModelChecker.java | 1 - 2 files changed, 25 insertions(+), 29 deletions(-) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 4d9e11f8..2372f6b4 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -257,9 +257,8 @@ public class NondetModelChecker extends NonProbModelChecker protected StateValues checkExpressionMultiObjective(ExpressionFunc expr) throws PrismException { // Objective/target info - int numTargets; List targetExprs; - List targetDDs, multitargetDDs = null; + List multitargetDDs = null; List multitargetIDs = null; OpsAndBoundsList opsAndBounds; @@ -289,12 +288,6 @@ public class NondetModelChecker extends NonProbModelChecker ddStateIndex = ODDUtils.SingleIndexToDD(stateIndex, odd, allDDRowVars); } - // Check format and extract bounds/etc. - numTargets = expr.getNumOperands(); - opsAndBounds = new OpsAndBoundsList(); - List rewards = new ArrayList(numTargets); - List rewardsIndex = new ArrayList(numTargets); - // Can't do LTL with time-bounded variants of the temporal operators // TODO removed since it is allowed for valiter. // TODO make sure it is treated correctly for all params @@ -302,10 +295,15 @@ public class NondetModelChecker extends NonProbModelChecker throw new PrismException("Time-bounded operators not supported in LTL: " + expr); }*/ + // Check format and extract bounds/etc. + int numObjectives = expr.getNumOperands(); + opsAndBounds = new OpsAndBoundsList(); + List rewards = new ArrayList(numObjectives); + List rewardsIndex = new ArrayList(numObjectives); ArrayList targetName = new ArrayList(); - targetExprs = new ArrayList(numTargets); - for (int i = 0; i < numTargets; i++) { - extractInfoFromMultiObjectiveOperand(expr.getOperand(i), opsAndBounds, rewardsIndex, targetName, targetExprs, i == 0); + targetExprs = new ArrayList(numObjectives); + for (int i = 0; i < numObjectives; i++) { + extractInfoFromMultiObjectiveOperand(expr.getOperand(i), opsAndBounds, rewardsIndex, targetName, targetExprs); } //currently we do 1 numerical subject to booleans, or multiple numericals only @@ -317,16 +315,13 @@ public class NondetModelChecker extends NonProbModelChecker negateresult = opsAndBounds.contains(Operator.P_MIN); hasMaxReward = opsAndBounds.contains(Operator.R_GE) || opsAndBounds.contains(Operator.R_MAX); - // Create array to store target DDs - targetDDs = new ArrayList(numTargets); - // Multi-objective model checking // Create arrays to store LTL/DRA info - ltl = new Expression[numTargets]; - dra = new DRA[numTargets]; - draDDRowVars = new JDDVars[numTargets]; - draDDColVars = new JDDVars[numTargets]; + ltl = new Expression[numObjectives]; + dra = new DRA[numObjectives]; + draDDRowVars = new JDDVars[numObjectives]; + draDDColVars = new JDDVars[numObjectives]; // For LTL/multi-obj model checking routines mcLtl = new LTLModelChecker(prism); @@ -337,7 +332,7 @@ public class NondetModelChecker extends NonProbModelChecker // Go through probabilistic objectives and construct product MDP. boolean originalmodel = true; - for (int i = 0; i < numTargets; i++) { + for (int i = 0; i < numObjectives; i++) { if (opsAndBounds.isProbabilityObjective(i)) { draDDRowVars[i] = new JDDVars(); draDDColVars[i] = new JDDVars(); @@ -367,7 +362,7 @@ public class NondetModelChecker extends NonProbModelChecker // Removing actions with non-zero reward from the product for maximum cases if (hasMaxReward /*& hasLTLconstraint*/) { - mcMo.removeNonZeroMecsForMax(modelProduct, mcLtl, rewardsIndex, opsAndBounds, numTargets, dra, draDDRowVars, draDDColVars); + mcMo.removeNonZeroMecsForMax(modelProduct, mcLtl, rewardsIndex, opsAndBounds, numObjectives, dra, draDDRowVars, draDDColVars); } // Remove all non-zero reward from trans in order to search for zero reward end components @@ -376,11 +371,11 @@ public class NondetModelChecker extends NonProbModelChecker boolean transchanged = mcMo.removeNonZeroRewardTrans(modelProduct, rewardsIndex, opsAndBounds); // Compute all maximal end components - ArrayList> allstatesH = new ArrayList>(numTargets); - ArrayList> allstatesL = new ArrayList>(numTargets); + ArrayList> allstatesH = new ArrayList>(numObjectives); + ArrayList> allstatesL = new ArrayList>(numObjectives); JDDNode acceptanceVector_H = JDD.Constant(0); JDDNode acceptanceVector_L = JDD.Constant(0); - for (int i = 0; i < numTargets; i++) { + for (int i = 0; i < numObjectives; i++) { if (opsAndBounds.isProbabilityObjective(i)) { ArrayList statesH = new ArrayList(); ArrayList statesL = new ArrayList(); @@ -412,9 +407,11 @@ public class NondetModelChecker extends NonProbModelChecker // Find accepting maximum end components for each LTL formula List allecs = mcMo.computeAllEcs(modelProduct, mcLtl, allstatesH, allstatesL, acceptanceVector_H, acceptanceVector_L, draDDRowVars, draDDColVars, - opsAndBounds, numTargets); + opsAndBounds, numObjectives); - for (int i = 0; i < numTargets; i++) { + // Create array to store target DDs + List targetDDs = new ArrayList(numObjectives); + for (int i = 0; i < numObjectives; i++) { if (opsAndBounds.isProbabilityObjective(i)) { targetDDs.add(mcMo.computeAcceptingEndComponent(dra[i], modelProduct, draDDRowVars[i], draDDColVars[i], allecs, allstatesH.get(i), allstatesL.get(i), mcLtl, conflictformulae > 1, targetName.get(i))); @@ -433,7 +430,7 @@ public class NondetModelChecker extends NonProbModelChecker if (conflictformulae > 1) { multitargetDDs = new ArrayList(); multitargetIDs = new ArrayList(); - mcMo.checkConflictsInObjectives(modelProduct, mcLtl, conflictformulae, numTargets, opsAndBounds, dra, draDDRowVars, draDDColVars, targetDDs, allstatesH, + mcMo.checkConflictsInObjectives(modelProduct, mcLtl, conflictformulae, numObjectives, opsAndBounds, dra, draDDRowVars, draDDColVars, targetDDs, allstatesH, allstatesL, multitargetDDs, multitargetIDs); } @@ -468,7 +465,7 @@ public class NondetModelChecker extends NonProbModelChecker JDD.Deref(ddStateIndex); if (modelProduct != null && modelProduct != model) modelProduct.clear(); - for (int i = 0; i < numTargets; i++) { + for (int i = 0; i < numObjectives; i++) { if (opsAndBounds.isProbabilityObjective(i)) { draDDRowVars[i].derefAll(); draDDColVars[i].derefAll(); @@ -512,7 +509,7 @@ public class NondetModelChecker extends NonProbModelChecker //takes one operand of multi-objective expression and extracts operator, values and reward functions from it. protected void extractInfoFromMultiObjectiveOperand(Expression operand, OpsAndBoundsList opsAndBounds, List rewardsIndex, List targetName, - List targetExprs, boolean isFirst) throws PrismException + List targetExprs) throws PrismException { int stepBound = 0; ExpressionProb exprProb = null; diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 092ca899..3ebb00d0 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -38,7 +38,6 @@ import jdd.JDD; import jdd.JDDNode; import jdd.JDDVars; import mtbdd.PrismMTBDD; -import parser.Values; import parser.ast.Expression; import parser.ast.ExpressionProb; import parser.ast.ExpressionReward;