From 80ddd4be4b549e31e141ba6064238a067aeeaf34 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 27 Jul 2013 00:41:18 +0000 Subject: [PATCH] Some additions to Strategy classes + better integration of symbolic strategy generation. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7169 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 9 ++--- prism/src/sparse/PS_NondetUntil.cc | 17 +++++--- prism/src/strat/MDStrategy.java | 9 ++++- prism/src/strat/MDStrategyArray.java | 27 ++++++++++++- prism/src/strat/MDStrategyIV.java | 54 +++++++++++++------------ prism/src/strat/Strategy.java | 10 +++++ 6 files changed, 87 insertions(+), 39 deletions(-) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index d35e01d0..413709ba 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1961,14 +1961,13 @@ public class NondetModelChecker extends NonProbModelChecker case Prism.SPARSE: IntegerVector strat = null; if (genStrat) { - strat = new IntegerVector((int) model.getNumStates()); + JDDNode ddStrat = JDD.ITE(yes, JDD.Constant(-2), JDD.Constant(-1)); + strat = new IntegerVector(ddStrat, allDDRowVars, odd); + JDD.Deref(ddStrat); } probsDV = PrismSparse.NondetUntil(tr, tra, model.getSynchs(), odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, min, strat); if (genStrat) { - mainLog.println(); - MDStrategyIV strategy = new MDStrategyIV(model, strat); - strategy.exportActions(mainLog); - strategy.clear(); + result.setStrategy(new MDStrategyIV(model, strat)); } probs = new StateValuesDV(probsDV, model); break; diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index 2e3d008c..12e96394 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/prism/src/sparse/PS_NondetUntil.cc @@ -179,14 +179,19 @@ jlong _strat // strategy storage // if required, create storage for adversary and initialise if (export_adv_enabled != EXPORT_ADV_NONE || strat != NULL) { PS_PrintToMainLog(env, "Allocating adversary vector... "); - adv = (strat == NULL) ? new int[n] : strat; + // Use passed in (pre-filled) array, if provided + if (strat) { + adv = strat; + } else { + adv = new int[n]; + // Initialise all entries to -1 ("don't know") + for (i = 0; i < n; i++) { + adv[i] = -1; + } + } kb = n*sizeof(int)/1024.0; kbt += kb; PS_PrintMemoryToMainLog(env, "[", kb, "]\n"); - // Initialise all entries to -1 ("don't know") - for (i = 0; i < n; i++) { - adv[i] = -1; - } } // print total memory usage @@ -362,7 +367,7 @@ jlong _strat // strategy storage if (ndsm) delete ndsm; if (yes_vec) delete[] yes_vec; if (soln2) delete[] soln2; - //if (strat == NULL && adv) delete[] adv; + if (strat == NULL && adv) delete[] adv; if (actions != NULL) { delete[] actions; release_string_array_from_java(env, action_names_jstrings, action_names, num_actions); diff --git a/prism/src/strat/MDStrategy.java b/prism/src/strat/MDStrategy.java index 8ba8089b..2dd80fd9 100644 --- a/prism/src/strat/MDStrategy.java +++ b/prism/src/strat/MDStrategy.java @@ -39,12 +39,17 @@ public abstract class MDStrategy implements Strategy */ public abstract int getNumStates(); + /** + * Get the type of choice information stored for state s. + */ + public abstract Strategy.Choice getChoice(int s); + /** * Get the index of the choice taken in state s. * The index is defined with respect to a particular model, stored locally. * Other possible values: -1 (unknown), -2 (arbitrary), -3 (unreachable) */ - public abstract int getChoice(int s); + public abstract int getChoiceIndex(int s); /** * Get the action taken in state s. @@ -57,7 +62,7 @@ public abstract class MDStrategy implements Strategy int n = getNumStates(); for (int s = 0; s < n; s++) { // Only print actions for reachable states - if (getChoice(s) != -3) + if (getChoice(s) != Choice.UNREACHABLE) out.println(s + ":" + getChoiceAction(s)); } } diff --git a/prism/src/strat/MDStrategyArray.java b/prism/src/strat/MDStrategyArray.java index 2ceb5420..58aa9f80 100644 --- a/prism/src/strat/MDStrategyArray.java +++ b/prism/src/strat/MDStrategyArray.java @@ -48,6 +48,8 @@ public class MDStrategyArray extends MDStrategy this.choices = choices; } + // Methods for MDStrategy + @Override public int getNumStates() { @@ -55,7 +57,22 @@ public class MDStrategyArray extends MDStrategy } @Override - public int getChoice(int s) + public Strategy.Choice getChoice(int s) + { + switch (choices[s]) { + case -1: + return Choice.UNKNOWN; + case -2: + return Choice.ARBITRARY; + case -3: + return Choice.UNREACHABLE; + default: + return Choice.INDEX; + } + } + + @Override + public int getChoiceIndex(int s) { return choices[s]; } @@ -66,4 +83,12 @@ public class MDStrategyArray extends MDStrategy int c = choices[s]; return c >= 0 ? model.getAction(s, c) : c == -1 ? "?" : c == -2 ? "*" : "-"; } + + // Methods for Strategy + + @Override + public void clear() + { + choices = null; + } } diff --git a/prism/src/strat/MDStrategyIV.java b/prism/src/strat/MDStrategyIV.java index d0e9f724..1c446292 100644 --- a/prism/src/strat/MDStrategyIV.java +++ b/prism/src/strat/MDStrategyIV.java @@ -31,34 +31,23 @@ import java.util.List; import dv.IntegerVector; import prism.Model; +import strat.Strategy.Choice; /** - * Class to store a memoryless deterministic (MD) strategy, as a IntegerVector (i.e. stored natively as an array). + * Class to store a memoryless deterministic (MD) strategy, as an IntegerVector (i.e. stored natively as an array). */ public class MDStrategyIV extends MDStrategy { // Model associated with the strategy private Model model; - - private IntegerVector iv; - - private List actions; - + // Other model info private int numStates; - private long ptr; - - /** - * Creates... - */ - public MDStrategyIV(Model model) - { - this.model = model; - numStates = (int) model.getNumStates(); - actions = model.getSynchs(); - } + private List actions; + // Array storing MD strategy (action index for each state) + private IntegerVector iv; /** - * Creates... + * Create an MDStrategyIV from an IntegerVector. */ public MDStrategyIV(Model model, IntegerVector iv) { @@ -68,10 +57,7 @@ public class MDStrategyIV extends MDStrategy this.iv = iv; } - public void setPointer(long ptr) - { - this.ptr = ptr; - } + // Methods for MDStrategy @Override public int getNumStates() @@ -80,19 +66,37 @@ public class MDStrategyIV extends MDStrategy } @Override - public int getChoice(int s) + public Strategy.Choice getChoice(int s) + { + int c = iv.getElement(s); + switch (c) { + case -1: + return Choice.UNKNOWN; + case -2: + return Choice.ARBITRARY; + case -3: + return Choice.UNREACHABLE; + default: + return Choice.INDEX; + } + } + + @Override + public int getChoiceIndex(int s) { - return 99; + throw new UnsupportedOperationException(); } @Override public Object getChoiceAction(int s) { int c = iv.getElement(s); - //return ""+c; //c >= 0 ? actions.get(c) : "?"; return c >= 0 ? actions.get(c) : c == -1 ? "?" : c == -2 ? "*" : "-"; } + // Methods for Strategy + + @Override public void clear() { iv.clear(); diff --git a/prism/src/strat/Strategy.java b/prism/src/strat/Strategy.java index d5902e27..70ab973f 100644 --- a/prism/src/strat/Strategy.java +++ b/prism/src/strat/Strategy.java @@ -34,8 +34,18 @@ import prism.PrismLog; */ public interface Strategy { + // Types of info stored for each choice + public enum Choice { + INDEX, ACTION, UNKNOWN, ARBITRARY, UNREACHABLE; + }; + /** * Export the strategy to a PrismLog, displaying strategy choices as action names. */ public void exportActions(PrismLog out); + + /** + * Clear storage of the strategy. + */ + public void clear(); }