From ff11760860c7010c1bad061816ea28db040f4103 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 10 Jul 2013 06:11:58 +0000 Subject: [PATCH] Update strategy generation in explicit engine to distinguish between: -1 (unknown), -2 (arbitrary), -3 (unreachable). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7008 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPModelChecker.java | 55 +++++++++++++------------ prism/src/explicit/MDPSimple.java | 2 +- prism/src/explicit/MDPSparse.java | 2 +- prism/src/strat/MDStrategy.java | 5 ++- prism/src/strat/MDStrategyArray.java | 6 ++- 5 files changed, 38 insertions(+), 32 deletions(-) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 18a25caf..22bcb658 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -352,15 +352,6 @@ public class MDPModelChecker extends ProbModelChecker // Store num states n = mdp.getNumStates(); - // If required, create/initialise strategy storage - // Set all choices to -1, denoting unknown/arbitrary - if (genStrat || exportAdv) { - strat = new int[n]; - for (i = 0; i < n; i++) { - strat[i] = -1; - } - } - // Optimise by enlarging target set (if more info is available) targetOrig = target; if (init != null && known != null) { @@ -370,6 +361,16 @@ public class MDPModelChecker extends ProbModelChecker } } + // If required, create/initialise strategy storage + // Set choices to -1, denoting unknown + // (except for target states, which are -2, denoting arbitrary) + if (genStrat || exportAdv) { + strat = new int[n]; + for (i = 0; i < n; i++) { + strat[i] = target.get(i) ? -2 : -1; + } + } + // Precomputation timerProb0 = System.currentTimeMillis(); if (precomp && prob0) { @@ -391,18 +392,17 @@ public class MDPModelChecker extends ProbModelChecker numNo = no.cardinality(); mainLog.println("target=" + target.cardinality() + ", yes=" + numYes + ", no=" + numNo + ", maybe=" + (n - (numYes + numNo))); - // If still required, generate strategy for no/yes (0/1) states. - // This is just for the cases max=0 and min=1, where arbitrary choices suffice. - // So just pick the first choice (0) for all these. + // If still required, store strategy for no/yes (0/1) states. + // This is just for the cases max=0 and min=1, where arbitrary choices suffice (denoted by -2) if (genStrat || exportAdv) { if (min) { for (i = yes.nextSetBit(0); i >= 0; i = yes.nextSetBit(i + 1)) { if (!target.get(i)) - strat[i] = 0; + strat[i] = -2; } } else { for (i = no.nextSetBit(0); i >= 0; i = no.nextSetBit(i + 1)) { - strat[i] = 0; + strat[i] = -2; } } } @@ -1205,15 +1205,6 @@ public class MDPModelChecker extends ProbModelChecker // Store num states n = mdp.getNumStates(); - // If required, create/initialise strategy storage - // Set all choices to -1, denoting unknown/arbitrary - if (genStrat || exportAdv) { - strat = new int[n]; - for (i = 0; i < n; i++) { - strat[i] = -1; - } - } - // Optimise by enlarging target set (if more info is available) if (init != null && known != null) { BitSet targetNew = new BitSet(n); @@ -1223,6 +1214,16 @@ public class MDPModelChecker extends ProbModelChecker target = targetNew; } + // If required, create/initialise strategy storage + // Set choices to -1, denoting unknown + // (except for target states, which are -2, denoting arbitrary) + if (genStrat || exportAdv) { + strat = new int[n]; + for (i = 0; i < n; i++) { + strat[i] = target.get(i) ? -2 : -1; + } + } + // Precomputation (not optional) timerProb1 = System.currentTimeMillis(); inf = prob1(mdp, null, target, !min, null); @@ -1237,10 +1238,10 @@ public class MDPModelChecker extends ProbModelChecker // If required, generate strategy for "inf" states. if (genStrat || exportAdv) { if (min) { - // If min reward is infinite, all choices give infinity. - // So just pick the first choice (0) for all "inf" states. + // If min reward is infinite, all choices give infinity + // So the choice can be arbitrary, denoted by -2; for (i = inf.nextSetBit(0); i >= 0; i = inf.nextSetBit(i + 1)) { - strat[i] = 0; + strat[i] = -2; } } else { // If max reward is infinite, there is at least one choice giving infinity. @@ -1535,7 +1536,7 @@ public class MDPModelChecker extends ProbModelChecker // Set strategy choice for non-reachable state to -1 int n = mdp.getNumStates(); for (int s = restrict.nextClearBit(0); s < n; s = restrict.nextClearBit(s + 1)) { - strat[s] = -1; + strat[s] = -3; } } diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index d6288d5a..6a79524b 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -537,7 +537,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple public Object getAction(int s, int i) { List list; - if (actions == null || (list = actions.get(s)) == null) + if (i < 0 || actions == null || (list = actions.get(s)) == null) return null; return list.get(i); } diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index a93bf6fb..ac71e797 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -499,7 +499,7 @@ public class MDPSparse extends MDPExplicit @Override public Object getAction(int s, int i) { - return actions == null ? null : actions[rowStarts[s] + i]; + return i < 0 || actions == null ? null : actions[rowStarts[s] + i]; } @Override diff --git a/prism/src/strat/MDStrategy.java b/prism/src/strat/MDStrategy.java index 161bce3d..8ba8089b 100644 --- a/prism/src/strat/MDStrategy.java +++ b/prism/src/strat/MDStrategy.java @@ -42,6 +42,7 @@ public abstract class MDStrategy implements Strategy /** * 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); @@ -55,7 +56,9 @@ public abstract class MDStrategy implements Strategy { int n = getNumStates(); for (int s = 0; s < n; s++) { - out.println(s + ":" + getChoiceAction(s)); + // Only print actions for reachable states + if (getChoice(s) != -3) + out.println(s + ":" + getChoiceAction(s)); } } } diff --git a/prism/src/strat/MDStrategyArray.java b/prism/src/strat/MDStrategyArray.java index b4bcb11c..2ceb5420 100644 --- a/prism/src/strat/MDStrategyArray.java +++ b/prism/src/strat/MDStrategyArray.java @@ -34,7 +34,8 @@ public class MDStrategyArray extends MDStrategy { // Model associated with the strategy private explicit.NondetModel model; - // Index of choice taken in each state + // Index of choice taken in each state (wrt model above) + // Other possible values: -1 (unknown), -2 (arbitrary), -3 (unreachable) private int choices[]; /** @@ -62,6 +63,7 @@ public class MDStrategyArray extends MDStrategy @Override public Object getChoiceAction(int s) { - return model.getAction(s, choices[s]); + int c = choices[s]; + return c >= 0 ? model.getAction(s, c) : c == -1 ? "?" : c == -2 ? "*" : "-"; } }