From 4f30f4f774e0cea13a4fa7e87729c1d2fba4bf44 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 30 Dec 2014 01:07:13 +0000 Subject: [PATCH] Re-factoring in multi-objective model checking. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9468 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 2372f6b4..8648930a 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -262,8 +262,6 @@ public class NondetModelChecker extends NonProbModelChecker List multitargetIDs = null; OpsAndBoundsList opsAndBounds; - // TODO this only stored prob vs reward objective anyway - // boolean[] reachExpr; // whether target is just reachability (true) or LTL (false) // LTL/product model stuff NondetModel modelProduct, modelNew; JDDVars[] draDDRowVars, draDDColVars; @@ -507,7 +505,10 @@ public class NondetModelChecker extends NonProbModelChecker } - //takes one operand of multi-objective expression and extracts operator, values and reward functions from it. + /** + * Extract the information from the operator defining one objective of a multi-objective query, + * store the info in the passed in arrays and so some checks. + */ protected void extractInfoFromMultiObjectiveOperand(Expression operand, OpsAndBoundsList opsAndBounds, List rewardsIndex, List targetName, List targetExprs) throws PrismException { @@ -600,16 +601,11 @@ public class NondetModelChecker extends NonProbModelChecker } // Now extract targets - // Also store which ones are just reachability (in reachExpr) if (exprProb != null) { targetExprs.add(exprProb.getExpression()); - // TODO check if the following line is unneeded: it only kept track of probs vs rewards - // reachExpr[i] = false; targetName.add(exprProb.getExpression().toString()); } else { targetExprs.add(null); - // TODO check if the following line is unneeded: it only kept track of probs vs rewards - // reachExpr[i] = true; targetName.add(""); } }