From 663347c3be60d655c03934eb33e50b529bb73479 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Jul 2017 17:01:45 +0000 Subject: [PATCH] multi-objective: use statesOfInterest instead of currentFilter to determine the requested state Multi-objective model checking only supports checking for a single state. Previously, this check required a state-filter with a single matching state (e.g., the default filter(state, ..., "init") placed around a top-level expression). Now, we check that statesOfInterest is a singleton set. Thus, now expressions such as filter(max, multi(P=?[...]. P>0.5[...], "label") filter(print, multi(P=?[...]. P>0.5[...], "label") with single-state labels will work. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12033 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 23 ++++++++--------------- 1 file changed, 8 insertions(+), 15 deletions(-) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index ec4612a6..f67fea25 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -365,7 +365,7 @@ public class NondetModelChecker extends NonProbModelChecker /** * Model check a multi-objective query (from the contents of a strategy operator). * Return the result as a StateValues object (usually this gives values for all states, - * but for a multi-objective query, we just give a single value, usually for the initial state). + * but for a multi-objective query, we just give a single value, i.e., the statesOfInterest should be a singleton set). * *
[ REFS: result, DEREFS: statesOfInterest ] * @param exprs The list of Expressions specifying the objectives @@ -482,19 +482,13 @@ public class NondetModelChecker extends NonProbModelChecker boolean hasMaxReward = false; //boolean hasLTLconstraint = false; - // currently, ignore statesOfInterest - // TODO: switch singleton check below to use statesOfInterest - JDD.Deref(statesOfInterest); - - // Make sure we are only expected to compute a value for a single state - // Assuming yes, determine index of state of interest and build BDD - JDDNode ddStateIndex = null; - if (currentFilter == null || !(currentFilter.getOperator() == Filter.FilterOperator.STATE)) + // Make sure we are only expected to compute a value for a single state, + // i.e., that statesOfInterest is a singleton + if (!JDD.isSingleton(statesOfInterest, model.getAllDDRowVars())) { + JDD.Deref(statesOfInterest); throw new PrismException("Multi-objective model checking can only compute values from a single state"); - else { - int stateIndex = currentFilter.getStateIndex(); - ddStateIndex = ODDUtils.SingleIndexToDD(stateIndex, odd, allDDRowVars); } + JDDNode stateOfInterest = statesOfInterest; // Can't do LTL with time-bounded variants of the temporal operators // TODO removed since it is allowed for valiter. @@ -545,7 +539,7 @@ public class NondetModelChecker extends NonProbModelChecker draDDRowVars[i] = new JDDVars(); draDDColVars[i] = new JDDVars(); modelNew = mcMo.constructDRAandProductMulti(modelProduct, mcLtl, this, ltl[i], i, dra, opsAndBounds.getOperator(i), pathFormulas.get(i), - draDDRowVars[i], draDDColVars[i], ddStateIndex); + draDDRowVars[i], draDDColVars[i], stateOfInterest); // Deref old product (unless is the original model) if (i > 0 & !originalmodel) modelProduct.clear(); @@ -678,8 +672,7 @@ public class NondetModelChecker extends NonProbModelChecker conflictformulae > 1); } finally { // Deref, clean up - if (ddStateIndex != null) - JDD.Deref(ddStateIndex); + JDD.Deref(stateOfInterest); if (modelProduct != null && modelProduct != model) modelProduct.clear(); for (int i = 0; i < numObjectives; i++) {