diff --git a/prism/src/explicit/CTMDP.java b/prism/src/explicit/CTMDP.java index 3f6bd7ba..9ddf9dd8 100644 --- a/prism/src/explicit/CTMDP.java +++ b/prism/src/explicit/CTMDP.java @@ -29,29 +29,25 @@ package explicit; import prism.ModelType; /** - * Explicit representation of continuous-time Markov decision process (CTMDP). + * Interface for classes that provide (read-only) access to an explicit-state CTMDP. */ -public class CTMDP extends MDP +public interface CTMDP extends MDP { - // Model type (TODO: move to interface) + // Model type public static ModelType modelType = ModelType.CTMDP; - - // Uniformisation rate used to build CTMC/CTMDP - public double unif; + // TODO: copy/modify functions from CTMC + /** - * Constructor: empty CTMDP. + * Build the discretised (DT)MDP for this CTMDP, in implicit form + * (i.e. where the details are computed on the fly from this one). + * @param tau Step duration */ - public CTMDP() - { - initialise(0); - } + public MDP buildImplicitDiscretisedMDP(double tau); /** - * Constructor: new CTMDP with fixed number of states. + * Build (a new) discretised (DT)MDP for this CTMDP. + * @param tau Step duration */ - public CTMDP(int numStates) - { - initialise(numStates); - } + public MDPSimple buildDiscretisedMDP(double tau); } diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index 6e75ff64..fc1838e2 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/prism/src/explicit/CTMDPModelChecker.java @@ -27,6 +27,7 @@ package explicit; import java.util.BitSet; +import java.util.Map; import prism.PrismException; @@ -35,6 +36,30 @@ import prism.PrismException; */ public class CTMDPModelChecker extends MDPModelChecker { + /** + * Compute bounded probabilistic reachability. + * @param target: Target states + * @param t: Time bound + * @param min: Min or max probabilities for (true=min, false=max) + * @param init: Initial solution vector - pass null for default + * @param results: Optional array of size b+1 to store (init state) results for each step (null if unused) + */ + public ModelCheckerResult probReachBounded2(CTMDP ctmdp, BitSet target, double t, boolean min, double init[], + double results[]) throws PrismException + { + MDP mdp; + MDPModelChecker mc; + ModelCheckerResult res; + + mdp = ctmdp.buildDiscretisedMDP(0.0002); + mainLog.println(mdp); + mc = new MDPModelChecker(); + mc.inheritSettings(this); + res = mc.probReachBounded(mdp, target, 4500, min); + + return res; + } + /** * Compute bounded probabilistic reachability. * @param target: Target states @@ -60,10 +85,10 @@ public class CTMDPModelChecker extends MDPModelChecker mainLog.println("Starting time-bounded probabilistic reachability..."); // Store num states - n = ctmdp.numStates; + n = ctmdp.getNumStates(); // Get uniformisation rate; do Fox-Glynn - q = ctmdp.unif; + q = 99;//ctmdp.unif; qt = q * t; mainLog.println("\nUniformisation: q.t = " + q + " x " + t + " = " + qt); fg = new FoxGlynn(qt, 1e-300, 1e+300, termCritParam / 8.0); @@ -138,4 +163,40 @@ public class CTMDPModelChecker extends MDPModelChecker res.timeTaken = timer / 1000.0; return res; } + + /** + * Simple test program. + */ + public static void main(String args[]) + { + CTMDPModelChecker mc; + CTMDPSimple ctmdp; + ModelCheckerResult res; + BitSet target; + Map labels; + boolean min = true; + try { + mc = new CTMDPModelChecker(); + ctmdp = new CTMDPSimple(); + ctmdp.buildFromPrismExplicit(args[0]); + System.out.println(ctmdp); + labels = mc.loadLabelsFile(args[1]); + System.out.println(labels); + target = labels.get(args[2]); + if (target == null) + throw new PrismException("Unknown label \"" + args[2] + "\""); + for (int i = 3; i < args.length; i++) { + if (args[i].equals("-min")) + min = true; + else if (args[i].equals("-max")) + min = false; + else if (args[i].equals("-nopre")) + mc.setPrecomp(false); + } + res = mc.probReachBounded2(ctmdp, target, 1.0, min, null, null); + System.out.println(res.soln[0]); + } catch (PrismException e) { + System.out.println(e); + } + } } diff --git a/prism/src/explicit/CTMDPSimple.java b/prism/src/explicit/CTMDPSimple.java new file mode 100644 index 00000000..9b15724d --- /dev/null +++ b/prism/src/explicit/CTMDPSimple.java @@ -0,0 +1,95 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +import java.util.Map; + +/** + * Simple explicit-state representation of a CTMDP. + */ +public class CTMDPSimple extends MDPSimple implements CTMDP +{ + // Constructors + + /** + * Constructor: empty CTMDP. + */ + public CTMDPSimple() + { + initialise(0); + } + + /** + * Constructor: new CTMDP with fixed number of states. + */ + public CTMDPSimple(int numStates) + { + initialise(numStates); + } + + /** + * Copy constructor. + */ + public CTMDPSimple(CTMDPSimple ctmdp) + { + super(ctmdp); + } + + // Accessors (for CTMDP) + + @Override + public MDP buildImplicitDiscretisedMDP(double tau) + { + // TODO + return null; + } + + @Override + public MDPSimple buildDiscretisedMDP(double tau) + { + MDPSimple mdp; + Distribution distrNew; + int i; + double d; + mdp = new MDPSimple(numStates); + for (int in : getInitialStates()) { + mdp.addInitialState(in); + } + for (i = 0; i < numStates; i++) { + for (Distribution distr : trans.get(i)) { + distrNew = new Distribution(); + d = Math.exp(-distr.sum() * tau); + for (Map.Entry e : distr) { + distrNew.add(e.getKey(), (1 - d) * e.getValue()); + } + distrNew.add(i, d); + mdp.addChoice(i, distrNew); + } + } + return mdp; + } +} diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 129084e9..57b1f9a1 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -77,10 +77,8 @@ public class DTMCModelChecker extends ModelChecker b2 = target.get(i) || dtmc.someSuccessorsInSet(i, u); soln.set(i, b2); } - // Check termination u_done = soln.equals(u); - // u = soln u.clear(); u.or(soln); @@ -140,18 +138,14 @@ public class DTMCModelChecker extends ModelChecker b2 = target.get(i) || (dtmc.allSuccessorsInSet(i, u) && dtmc.someSuccessorsInSet(i, v)); soln.set(i, b2); } - // Check termination (inner) v_done = soln.equals(v); - // v = soln v.clear(); v.or(soln); } - // Check termination (outer) u_done = v.equals(u); - // u = v u.clear(); u.or(v); diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index ff258f98..e5616f6c 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -27,760 +27,98 @@ package explicit; import java.util.*; -import java.io.*; import prism.ModelType; -import prism.PrismException; -import prism.PrismUtils; /** - * Explicit representation of Markov decision process (MDP). + * Interface for classes that provide (read-only) access to an explicit-state MDP. */ -public class MDP extends ModelSimple +public interface MDP extends Model { - // Model type (TODO: move to interface) + // Model type public static ModelType modelType = ModelType.MDP; - // Transition function (Steps) - protected List> trans; - - // Action labels - // (null in element s means no actions for that state) - protected List> actions; - - // Rewards - // (if transRewardsConstant non-null, use this for all transitions; otherwise, use transRewards list) - // (for transRewards, null in element s means no rewards for that state) - protected Double transRewardsConstant; - protected List> transRewards; - - // Flag: allow duplicates in distribution sets? - protected boolean allowDupes = false; - - // Other statistics - protected int numDistrs; - protected int numTransitions; - protected int maxNumDistrs; - protected boolean maxNumDistrsOk; - - /** - * Constructor: empty MDP. - */ - public MDP() - { - initialise(0); - } - - /** - * Constructor: new MDP with fixed number of states. - */ - public MDP(int numStates) - { - initialise(numStates); - } - - /** - * Constructor: new MDP copied from an existing DTMC. - */ - public MDP(DTMCSimple dtmc) - { - this(dtmc.getNumStates()); - for (int s : dtmc.getInitialStates()) { - addInitialState(s); - } - for (int s = 0; s < numStates; s++) { - addChoice(s, new Distribution(dtmc.getTransitions(s))); - } - // TODO: copy rewards, etc. - } - - /** - * Initialise: new model with fixed number of states. - */ - public void initialise(int numStates) - { - super.initialise(numStates); - numDistrs = numTransitions = maxNumDistrs = 0; - maxNumDistrsOk = true; - trans = new ArrayList>(numStates); - for (int i = 0; i < numStates; i++) { - trans.add(new ArrayList()); - } - actions = null; - clearAllRewards(); - } - - /** - * Clear all information for a state (i.e. remove all transitions). - */ - public void clearState(int s) - { - // Do nothing if state does not exist - if (s >= numStates || s < 0) - return; - // Clear data structures and update stats - List list = trans.get(s); - numDistrs -= list.size(); - for (Distribution distr : list) { - numTransitions -= distr.size(); - } - maxNumDistrsOk = false; - trans.get(s).clear(); - if (actions != null && actions.get(s) != null) - actions.get(s).clear(); - if (transRewards != null && transRewards.get(s) != null) - transRewards.get(s).clear(); - } - - /** - * Add a new state and return its index. - */ - public int addState() - { - addStates(1); - return numStates - 1; - } - /** - * Add multiple new states. + * Check if any successor states are in a set for all choices of a state. + * @param s The state to check + * @param set The set to test for inclusion */ - public void addStates(int numToAdd) - { - for (int i = 0; i < numToAdd; i++) { - trans.add(new ArrayList()); - if (actions != null) - actions.add(null); - if (transRewards != null) - transRewards.add(null); - numStates++; - } - } - - /** - * Add a choice (distribution 'distr') to state s (which must exist). - * Distribution is only actually added if it does not already exists for state s. - * (Assuming 'allowDupes' flag is not enabled.) - * Returns the index of the (existing or newly added) distribution. - * Returns -1 in case of error. - */ - public int addChoice(int s, Distribution distr) - { - List set; - // Check state exists - if (s >= numStates || s < 0) - return -1; - // Add distribution (if new) - set = trans.get(s); - if (!allowDupes) { - int i = set.indexOf(distr); - if (i != -1) - return i; - } - set.add(distr); - // Add null action if necessary - if (actions != null && actions.get(s) != null) - actions.get(s).add(null); - // Add zero reward if necessary - if (transRewards != null && transRewards.get(s) != null) - transRewards.get(s).add(0.0); - // Update stats - numDistrs++; - maxNumDistrs = Math.max(maxNumDistrs, set.size()); - numTransitions += distr.size(); - return set.size() - 1; - } - - /** - * Remove all rewards from the model - */ - public void clearAllRewards() - { - transRewards = null; - transRewardsConstant = null; - } - - /** - * Set the action label for choice i in some state s. - */ - public void setAction(int s, int i, Object o) - { - // If no actions array created yet, create it - if (actions == null) { - actions = new ArrayList>(numStates); - for (int j = 0; j < numStates; j++) - actions.add(null); - } - // If no actions for state i yet, create list - if (actions.get(s) == null) { - int n = trans.get(s).size(); - List list = new ArrayList(n); - for (int j = 0; j < n; j++) { - list.add(0.0); - } - actions.set(s, list); - } - // Set actions - actions.get(s).set(i, o); - } - - /** - * Set a constant reward for all transitions - */ - public void setConstantTransitionReward(double r) - { - // This replaces any other reward definitions - transRewards = null; - // Store as a Double (because we use null to check for its existence) - transRewardsConstant = new Double(r); - } - - /** - * Set the reward for choice i in some state s to r. - */ - public void setTransitionReward(int s, int i, double r) - { - // This would replace any constant reward definition, if it existed - transRewardsConstant = null; - // If no rewards array created yet, create it - if (transRewards == null) { - transRewards = new ArrayList>(numStates); - for (int j = 0; j < numStates; j++) - transRewards.add(null); - } - // If no rewards for state i yet, create list - if (transRewards.get(s) == null) { - int n = trans.get(s).size(); - List list = new ArrayList(n); - for (int j = 0; j < n; j++) { - list.add(0.0); - } - transRewards.set(s, list); - } - // Set reward - transRewards.get(s).set(i, r); - } - - public boolean allSuccessorsInSet(int s, BitSet set) - { - for (Distribution distr : trans.get(s)) { - if (!distr.isSubsetOf(set)) - return false; - } - return true; - } - - public boolean someSuccessorsInSet(int s, BitSet set) - { - for (Distribution distr : trans.get(s)) { - if (distr.isSubsetOf(set)) - return true; - } - return false; - } - - /** - * Get the number of nondeterministic choices in state s. - */ - public int getNumChoices(int s) - { - return trans.get(s).size(); - } - - /** - * Get the list of choices (distributions) for state s. - */ - public List getChoices(int s) - { - return trans.get(s); - } - + public boolean someSuccessorsInSetForAllChoices(int s, BitSet set); + /** - * Get the ith choice (distribution) for state s. + * Check if any successor states are in set1 and all successor states + * are in set2 for some choices of a state. + * @param s The state to check + * @param set1 The set to test for inclusion (some) + * @param set2 The set to test for inclusion (all) */ - public Distribution getChoice(int s, int i) - { - return trans.get(s).get(i); - } - + public boolean someAllSuccessorsInSetForSomeChoices(int s, BitSet set1, BitSet set2); + /** - * Get the action (if any) for choice i of state s. + * Check if any successor states are in set1 and all successor states + * are in set2 for all choices of a state. + * @param s The state to check + * @param set1 The set to test for inclusion (some) + * @param set2 The set to test for inclusion (all) */ - public Object getAction(int s, int i) - { - List list; - if (actions == null || (list = actions.get(s)) == null) - return null; - return list.get(i); - } - + public boolean someAllSuccessorsInSetForAllChoices(int s, BitSet set1, BitSet set2); + /** * Get the transition reward (if any) for choice i of state s. */ - public double getTransitionReward(int s, int i) - { - List list; - if (transRewardsConstant != null) - return transRewardsConstant; - if (transRewards == null || (list = transRewards.get(s)) == null) - return 0.0; - return list.get(i); - } - - /** - * Returns true if state s2 is a successor of state s1. - */ - public boolean isSuccessor(int s1, int s2) - { - for (Distribution distr : trans.get(s1)) { - if (distr.contains(s2)) - return true; - } - return false; - } - - /** - * Get the total number of choices (distributions) over all states. - */ - public int getNumChoices() - { - return numDistrs; - } - - /** - * Get the total number of transitions in the model. - */ - public int getNumTransitions() - { - return numTransitions; - } - - /** - * Get the maximum number of choices (distributions) in any state. - */ - public int getMaxNumChoices() - { - // Recompute if necessary - if (!maxNumDistrsOk) { - maxNumDistrs = 0; - for (int s = 0; s < numStates; s++) - maxNumDistrs = Math.max(maxNumDistrs, getNumChoices(s)); - } - return maxNumDistrs; - } - - /** - * Checks for deadlocks (states with no choices) and throws an exception if any exist. - * States in 'except' (If non-null) are excluded from the check. - */ - public void checkForDeadlocks(BitSet except) throws PrismException - { - for (int i = 0; i < numStates; i++) { - if (trans.get(i).isEmpty() && (except == null || !except.get(i))) - throw new PrismException("MDP has a deadlock in state " + i); - } - // TODO: Check for empty distributions too? - } - - /** - * Build (anew) from a list of transitions exported explicitly by PRISM (i.e. a .tra file). - */ - public void buildFromPrismExplicit(String filename) throws PrismException - { - BufferedReader in; - Distribution distr; - String s, ss[]; - int i, j, k, iLast, kLast, n, lineNum = 0; - double prob; - - try { - // Open file - in = new BufferedReader(new FileReader(new File(filename))); - // Parse first line to get num states - s = in.readLine(); - lineNum = 1; - if (s == null) - throw new PrismException("Missing first line of .tra file"); - ss = s.split(" "); - n = Integer.parseInt(ss[0]); - // Initialise - initialise(n); - // Go though list of transitions in file - iLast = -1; - kLast = -1; - distr = null; - s = in.readLine(); - lineNum++; - while (s != null) { - s = s.trim(); - if (s.length() > 0) { - ss = s.split(" "); - i = Integer.parseInt(ss[0]); - k = Integer.parseInt(ss[1]); - j = Integer.parseInt(ss[2]); - prob = Double.parseDouble(ss[3]); - // For a new state or distribution - if (i != iLast || k != kLast) { - // Add any previous distribution to the last state, create new one - if (distr != null) { - addChoice(iLast, distr); - } - distr = new Distribution(); - } - // Add transition to the current distribution - distr.add(j, prob); - // Prepare for next iter - iLast = i; - kLast = k; - } - s = in.readLine(); - lineNum++; - } - // Add previous distribution to the last state - addChoice(iLast, distr); - // Close file - in.close(); - } catch (IOException e) { - System.out.println(e); - System.exit(1); - } catch (NumberFormatException e) { - throw new PrismException("Problem in .tra file (line " + lineNum + ") for " + modelType); - } - // Set initial state (assume 0) - initialStates.add(0); - } + public double getTransitionReward(int s, int i); /** * Do a matrix-vector multiplication followed by min/max, i.e. one step of value iteration. - * @param vect: Vector to multiply by - * @param min: Min or max for (true=min, false=max) - * @param result: Vector to store result in - * @param subset: Only do multiplication for these rows - * @param complement: If true, 'subset' is taken to be its complement + * @param vect Vector to multiply by + * @param min Min or max for (true=min, false=max) + * @param result Vector to store result in + * @param subset Only do multiplication for these rows + * @param complement If true, 'subset' is taken to be its complement */ - public void mvMultMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement) - { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultMinMaxSingle(s, vect, min); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultMinMaxSingle(s, vect, min); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultMinMaxSingle(s, vect, min); - } - } + public void mvMultMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement); /** * Do a single row of matrix-vector multiplication followed by min/max. - * @param s: Row index - * @param vect: Vector to multiply by - * @param min: Min or max for (true=min, false=max) + * @param s Row index + * @param vect Vector to multiply by + * @param min Min or max for (true=min, false=max) */ - public double mvMultMinMaxSingle(int s, double vect[], boolean min) - { - int k; - double d, prob, minmax; - boolean first; - List step; - - minmax = 0; - first = true; - step = trans.get(s); - for (Distribution distr : step) { - // Compute sum for this distribution - d = 0.0; - for (Map.Entry e : distr) { - k = (Integer) e.getKey(); - prob = (Double) e.getValue(); - d += prob * vect[k]; - } - // Check whether we have exceeded min/max so far - if (first || (min && d < minmax) || (!min && d > minmax)) - minmax = d; - first = false; - } - - return minmax; - } + public double mvMultMinMaxSingle(int s, double vect[], boolean min); /** * Determine which choices result in min/max after a single row of matrix-vector multiplication. - * @param s: Row index - * @param vect: Vector to multiply by - * @param min: Min or max (true=min, false=max) - * @param val: Min or max value to match + * @param s Row index + * @param vect Vector to multiply by + * @param min Min or max (true=min, false=max) + * @param val Min or max value to match */ - public List mvMultMinMaxSingleChoices(int s, double vect[], boolean min, double val) - { - int j, k; - double d, prob; - List res; - List step; - - // Create data structures to store strategy - res = new ArrayList(); - // One row of matrix-vector operation - j = -1; - step = trans.get(s); - for (Distribution distr : step) { - j++; - // Compute sum for this distribution - d = 0.0; - for (Map.Entry e : distr) { - k = (Integer) e.getKey(); - prob = (Double) e.getValue(); - d += prob * vect[k]; - } - // Store strategy info if value matches - //if (PrismUtils.doublesAreClose(val, d, termCritParam, termCrit == TermCrit.ABSOLUTE)) { - if (PrismUtils.doublesAreClose(val, d, 1e-12, false)) { - res.add(j); - //res.add(distrs.getAction()); - } - } - - return res; - } + public List mvMultMinMaxSingleChoices(int s, double vect[], boolean min, double val); /** * Do a matrix-vector multiplication and sum of action reward followed by min/max, i.e. one step of value iteration. - * @param vect: Vector to multiply by - * @param min: Min or max for (true=min, false=max) - * @param result: Vector to store result in - * @param subset: Only do multiplication for these rows - * @param complement: If true, 'subset' is taken to be its complement + * @param vect Vector to multiply by + * @param min Min or max for (true=min, false=max) + * @param result Vector to store result in + * @param subset Only do multiplication for these rows + * @param complement If true, 'subset' is taken to be its complement */ - public void mvMultRewMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement) - { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultRewMinMaxSingle(s, vect, min); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultRewMinMaxSingle(s, vect, min); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultRewMinMaxSingle(s, vect, min); - } - } + public void mvMultRewMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement); /** * Do a single row of matrix-vector multiplication and sum of action reward followed by min/max. - * @param s: Row index - * @param vect: Vector to multiply by - * @param min: Min or max for (true=min, false=max) + * @param s Row index + * @param vect Vector to multiply by + * @param min Min or max for (true=min, false=max) */ - public double mvMultRewMinMaxSingle(int s, double vect[], boolean min) - { - int j, k; - double d, prob, minmax; - boolean first; - List step; - - minmax = 0; - first = true; - j = -1; - step = trans.get(s); - for (Distribution distr : step) { - j++; - // Compute sum for this distribution - d = getTransitionReward(s, j); - for (Map.Entry e : distr) { - k = (Integer) e.getKey(); - prob = (Double) e.getValue(); - d += prob * vect[k]; - } - // Check whether we have exceeded min/max so far - if (first || (min && d < minmax) || (!min && d > minmax)) - minmax = d; - first = false; - } - - return minmax; - } + public double mvMultRewMinMaxSingle(int s, double vect[], boolean min); /** * Determine which choices result in min/max after a single row of matrix-vector multiplication and sum of action reward. - * @param s: Row index - * @param vect: Vector to multiply by - * @param min: Min or max (true=min, false=max) - * @param val: Min or max value to match - */ - public List mvMultRewMinMaxSingleChoices(int s, double vect[], boolean min, double val) - { - int j, k; - double d, prob; - List res; - List step; - - // Create data structures to store strategy - res = new ArrayList(); - // One row of matrix-vector operation - j = -1; - step = trans.get(s); - for (Distribution distr : step) { - j++; - // Compute sum for this distribution - d = getTransitionReward(s, j); - for (Map.Entry e : distr) { - k = (Integer) e.getKey(); - prob = (Double) e.getValue(); - d += prob * vect[k]; - } - // Store strategy info if value matches - //if (PrismUtils.doublesAreClose(val, d, termCritParam, termCrit == TermCrit.ABSOLUTE)) { - if (PrismUtils.doublesAreClose(val, d, 1e-12, false)) { - res.add(j); - //res.add(distrs.getAction()); - } - } - - return res; - } - - /** - * Export to a dot file. - */ - public void exportToDotFile(String filename) throws PrismException - { - exportToDotFile(filename, null); - } - - /** - * Export to explicit format readable by PRISM (i.e. a .tra file, etc.). - */ - public void exportToPrismExplicit(String baseFilename) throws PrismException - { - int i, j; - String filename = null; - FileWriter out; - try { - // Output transitions to .tra file - filename = baseFilename + ".tra"; - out = new FileWriter(filename); - out.write(numStates + " " + numDistrs + " " + numTransitions + "\n"); - for (i = 0; i < numStates; i++) { - j = -1; - for (Distribution distr : trans.get(i)) { - j++; - for (Map.Entry e : distr) { - out.write(i + " " + j + " " + e.getKey() + " " + e.getValue() + "\n"); - } - } - } - out.close(); - // Output transition rewards to .trew file - // TODO - filename = baseFilename + ".trew"; - out = new FileWriter(filename); - out.write(numStates + " " + "?" + " " + "?" + "\n"); - for (i = 0; i < numStates; i++) { - j = -1; - for (Distribution distr : trans.get(i)) { - j++; - for (Map.Entry e : distr) { - out.write(i + " " + j + " " + e.getKey() + " " + "1.0" + "\n"); - } - } - } - out.close(); - } catch (IOException e) { - throw new PrismException("Could not export " + modelType + " to file \"" + filename + "\"" + e); - } - } - - /** - * Export to a dot file, highlighting states in 'mark'. - */ - public void exportToDotFile(String filename, BitSet mark) throws PrismException - { - int i, j; - String nij; - try { - FileWriter out = new FileWriter(filename); - out.write("digraph " + modelType + " {\nsize=\"8,5\"\nnode [shape=box];\n"); - for (i = 0; i < numStates; i++) { - if (mark != null && mark.get(i)) - out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n"); - j = -1; - for (Distribution distr : trans.get(i)) { - j++; - nij = "n" + i + "_" + j; - out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j + "\" ];\n"); - out.write(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n"); - for (Map.Entry e : distr) { - out.write(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); - } - } - } - out.write("}\n"); - out.close(); - } catch (IOException e) { - throw new PrismException("Could not write " + modelType + " to file \"" + filename + "\"" + e); - } - } - - /** - * Get string with model info/stats. - */ - public String infoString() - { - String s = ""; - s += numStates + " states"; - s += " (" + getNumInitialStates() + " initial)"; - s += ", " + numDistrs + " distributions"; - s += ", " + numTransitions + " transitions"; - s += ", dist max/avg = " + getMaxNumChoices() + "/" - + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates); - return s; - } - - /** - * Get transition function as string. - */ - public String toString() - { - int i; - boolean first; - String s = ""; - first = true; - s = "[ "; - for (i = 0; i < numStates; i++) { - if (first) - first = false; - else - s += ", "; - s += i + ": " + trans.get(i); - if (actions != null) - s += actions.get(i); - if (transRewards != null) - s += transRewards.get(i); - } - s += " ]"; - return s; - } - - /** - * Equality check. + * @param s Row index + * @param vect Vector to multiply by + * @param min Min or max (true=min, false=max) + * @param val Min or max value to match */ - public boolean equals(Object o) - { - if (o == null || !(o instanceof MDP)) - return false; - MDP mdp = (MDP) o; - if (numStates != mdp.numStates) - return false; - if (!initialStates.equals(mdp.initialStates)) - return false; - if (!trans.equals(mdp.trans)) - return false; - // TODO: compare actions (complicated: null = null,null,null,...) - // TODO: compare rewards (complicated: null = 0,0,0,0) - return true; - } + public List mvMultRewMinMaxSingleChoices(int s, double vect[], boolean min, double val); } diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index b3dbdca1..cb854ff6 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -42,8 +42,8 @@ public class MDPModelChecker extends ModelChecker */ public BitSet prob0(MDP mdp, BitSet target, boolean min) { - int i, k, n, iters; - boolean b2, b3; + int i, n, iters; + boolean b2; BitSet u, soln; boolean u_done; long timer; @@ -54,13 +54,13 @@ public class MDPModelChecker extends ModelChecker // Special case: no target states if (target.cardinality() == 0) { - soln = new BitSet(mdp.numStates); - soln.set(0, mdp.numStates); + soln = new BitSet(mdp.getNumStates()); + soln.set(0, mdp.getNumStates()); return soln; } // Initialise vectors - n = mdp.numStates; + n = mdp.getNumStates(); u = (BitSet) target.clone(); soln = new BitSet(n); @@ -72,35 +72,18 @@ public class MDPModelChecker extends ModelChecker while (!u_done) { iters++; for (i = 0; i < n; i++) { - // First see if this state is a target state - // (in which case, can skip rest of fixed point function evaluation) - b2 = target.get(i); - if (!b2) { - b2 = min; // there exists or for all nondet choices - for (Distribution distr : mdp.getChoices(i)) { - b3 = false; // some transition goes to u - for (Map.Entry e : distr) { - k = (Integer) e.getKey(); - if (u.get(k)) { - b3 = true; - continue; - } - } - if (min) { - if (!b3) - b2 = false; - } else { - if (b3) - b2 = true; - } - } + // Need either that i is a target state or + // (for min) all choices have a transition to u + // (for max) some choice has a transition to u + if (min) { + b2 = target.get(i) || mdp.someSuccessorsInSetForAllChoices(i, u); + } else { + b2 = target.get(i) || mdp.someSuccessorsInSet(i, u); } soln.set(i, b2); } - // Check termination u_done = soln.equals(u); - // u = soln u.clear(); u.or(soln); @@ -122,8 +105,8 @@ public class MDPModelChecker extends ModelChecker */ public BitSet prob1(MDP mdp, BitSet target, boolean min) { - int i, k, n, iters; - boolean b2, b3, b4, b5; + int i, n, iters; + boolean b2; BitSet u, v, soln; boolean u_done, v_done; long timer; @@ -134,11 +117,11 @@ public class MDPModelChecker extends ModelChecker // Special case: no target states if (target.cardinality() == 0) { - return new BitSet(mdp.numStates); + return new BitSet(mdp.getNumStates()); } // Initialise vectors - n = mdp.numStates; + n = mdp.getNumStates(); u = new BitSet(n); v = new BitSet(n); soln = new BitSet(n); @@ -155,45 +138,24 @@ public class MDPModelChecker extends ModelChecker while (!v_done) { iters++; for (i = 0; i < n; i++) { - // First see if this state is a target state - // (in which case, can skip rest of fixed point function evaluation) - b2 = target.get(i); - if (!b2) { - b2 = min; // there exists or for all choices - for (Distribution distr : mdp.getChoices(i)) { - b3 = true; // all transitions are to u states - b4 = false; // some transition goes to v - for (Map.Entry e : distr) { - k = (Integer) e.getKey(); - if (!u.get(k)) - b3 = false; - if (v.get(k)) - b4 = true; - } - b5 = (b3 && b4); - if (min) { - if (!b5) - b2 = false; - } else { - if (b5) - b2 = true; - } - } + // Need either that i is a target state or + // (for min) all choices have all transitions to v and a transition to u + // (for max) some choice has all transitions to v and a transition to u + if (min) { + b2 = target.get(i) || mdp.someAllSuccessorsInSetForAllChoices(i, u, v); + } else { + b2 = target.get(i) || mdp.someAllSuccessorsInSetForSomeChoices(i, u, v); } soln.set(i, b2); } - // Check termination (inner) v_done = soln.equals(v); - // v = soln v.clear(); v.or(soln); } - // Check termination (outer) u_done = v.equals(u); - // u = v u.clear(); u.or(v); @@ -243,7 +205,7 @@ public class MDPModelChecker extends ModelChecker mdp.checkForDeadlocks(target); // Store num states - n = mdp.numStates; + n = mdp.getNumStates(); // Optimise by enlarging target set (if more info is available) if (init != null && known != null) { @@ -321,7 +283,7 @@ public class MDPModelChecker extends ModelChecker mainLog.println("Starting value iteration (" + (min ? "min" : "max") + ")..."); // Store num states - n = mdp.numStates; + n = mdp.getNumStates(); // Create solution vector(s) soln = new double[n]; @@ -433,7 +395,7 @@ public class MDPModelChecker extends ModelChecker mainLog.println("Starting bounded probabilistic reachability..."); // Store num states - n = mdp.numStates; + n = mdp.getNumStates(); // Create solution vector(s) soln = new double[n]; @@ -529,7 +491,7 @@ public class MDPModelChecker extends ModelChecker mdp.checkForDeadlocks(target); // Store num states - n = mdp.numStates; + n = mdp.getNumStates(); // Optimise by enlarging target set (if more info is available) if (init != null && known != null) { @@ -596,7 +558,7 @@ public class MDPModelChecker extends ModelChecker mainLog.println("Starting value iteration (" + (min ? "min" : "max") + ")..."); // Store num states - n = mdp.numStates; + n = mdp.getNumStates(); // Create solution vector(s) soln = new double[n]; @@ -678,14 +640,14 @@ public class MDPModelChecker extends ModelChecker public static void main(String args[]) { MDPModelChecker mc; - MDP mdp; + MDPSimple mdp; ModelCheckerResult res; BitSet target; Map labels; boolean min = true; try { mc = new MDPModelChecker(); - mdp = new MDP(); + mdp = new MDPSimple(); mdp.buildFromPrismExplicit(args[0]); //System.out.println(mdp); labels = mc.loadLabelsFile(args[1]); @@ -695,7 +657,7 @@ public class MDPModelChecker extends ModelChecker throw new PrismException("Unknown label \"" + args[2] + "\""); for (int i = 3; i < args.length; i++) { if (args[i].equals("-min")) - min =true; + min = true; else if (args[i].equals("-max")) min = false; else if (args[i].equals("-nopre")) diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java new file mode 100644 index 00000000..6c5bf8aa --- /dev/null +++ b/prism/src/explicit/MDPSimple.java @@ -0,0 +1,770 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +import java.util.*; +import java.io.*; + +import prism.PrismException; +import prism.PrismUtils; + +/** + * Simple explicit-state representation of an MDP. + */ +public class MDPSimple extends ModelSimple implements MDP +{ + // Transition function (Steps) + protected List> trans; + + // Action labels + // (null in element s means no actions for that state) + protected List> actions; + + // Rewards + // (if transRewardsConstant non-null, use this for all transitions; otherwise, use transRewards list) + // (for transRewards, null in element s means no rewards for that state) + protected Double transRewardsConstant; + protected List> transRewards; + + // Flag: allow duplicates in distribution sets? + protected boolean allowDupes = false; + + // Other statistics + protected int numDistrs; + protected int numTransitions; + protected int maxNumDistrs; + protected boolean maxNumDistrsOk; + + // Constructors + + /** + * Constructor: empty MDP. + */ + public MDPSimple() + { + initialise(0); + } + + /** + * Constructor: new MDP with fixed number of states. + */ + public MDPSimple(int numStates) + { + initialise(numStates); + } + + /** + * Copy constructor. + */ + public MDPSimple(MDPSimple mdp) + { + this(mdp.numStates); + for (int in : mdp.getInitialStates()) { + addInitialState(in); + } + for (int i = 0; i < numStates; i++) { + for (Distribution distr : mdp.trans.get(i)) { + addChoice(i, new Distribution(distr)); + } + } + // TODO: copy actions, rewards + } + + /** + * Constructor: new MDP copied from an existing DTMC. + */ + public MDPSimple(DTMCSimple dtmc) + { + this(dtmc.getNumStates()); + for (int s : dtmc.getInitialStates()) { + addInitialState(s); + } + for (int s = 0; s < numStates; s++) { + addChoice(s, new Distribution(dtmc.getTransitions(s))); + } + // TODO: copy rewards, etc. + } + + // Mutators (for ModelSimple) + + @Override + public void initialise(int numStates) + { + super.initialise(numStates); + numDistrs = numTransitions = maxNumDistrs = 0; + maxNumDistrsOk = true; + trans = new ArrayList>(numStates); + for (int i = 0; i < numStates; i++) { + trans.add(new ArrayList()); + } + actions = null; + clearAllRewards(); + } + + @Override + public void clearState(int s) + { + // Do nothing if state does not exist + if (s >= numStates || s < 0) + return; + // Clear data structures and update stats + List list = trans.get(s); + numDistrs -= list.size(); + for (Distribution distr : list) { + numTransitions -= distr.size(); + } + maxNumDistrsOk = false; + trans.get(s).clear(); + if (actions != null && actions.get(s) != null) + actions.get(s).clear(); + if (transRewards != null && transRewards.get(s) != null) + transRewards.get(s).clear(); + } + + @Override + public int addState() + { + addStates(1); + return numStates - 1; + } + + @Override + public void addStates(int numToAdd) + { + for (int i = 0; i < numToAdd; i++) { + trans.add(new ArrayList()); + if (actions != null) + actions.add(null); + if (transRewards != null) + transRewards.add(null); + numStates++; + } + } + + @Override + public void buildFromPrismExplicit(String filename) throws PrismException + { + BufferedReader in; + Distribution distr; + String s, ss[]; + int i, j, k, iLast, kLast, n, lineNum = 0; + double prob; + + try { + // Open file + in = new BufferedReader(new FileReader(new File(filename))); + // Parse first line to get num states + s = in.readLine(); + lineNum = 1; + if (s == null) + throw new PrismException("Missing first line of .tra file"); + ss = s.split(" "); + n = Integer.parseInt(ss[0]); + // Initialise + initialise(n); + // Go though list of transitions in file + iLast = -1; + kLast = -1; + distr = null; + s = in.readLine(); + lineNum++; + while (s != null) { + s = s.trim(); + if (s.length() > 0) { + ss = s.split(" "); + i = Integer.parseInt(ss[0]); + k = Integer.parseInt(ss[1]); + j = Integer.parseInt(ss[2]); + prob = Double.parseDouble(ss[3]); + // For a new state or distribution + if (i != iLast || k != kLast) { + // Add any previous distribution to the last state, create new one + if (distr != null) { + addChoice(iLast, distr); + } + distr = new Distribution(); + } + // Add transition to the current distribution + distr.add(j, prob); + // Prepare for next iter + iLast = i; + kLast = k; + } + s = in.readLine(); + lineNum++; + } + // Add previous distribution to the last state + addChoice(iLast, distr); + // Close file + in.close(); + } catch (IOException e) { + System.out.println(e); + System.exit(1); + } catch (NumberFormatException e) { + throw new PrismException("Problem in .tra file (line " + lineNum + ") for " + modelType); + } + // Set initial state (assume 0) + initialStates.add(0); + } + + // Mutators (other) + + /** + * Add a choice (distribution 'distr') to state s (which must exist). + * Distribution is only actually added if it does not already exists for state s. + * (Assuming 'allowDupes' flag is not enabled.) + * Returns the index of the (existing or newly added) distribution. + * Returns -1 in case of error. + */ + public int addChoice(int s, Distribution distr) + { + List set; + // Check state exists + if (s >= numStates || s < 0) + return -1; + // Add distribution (if new) + set = trans.get(s); + if (!allowDupes) { + int i = set.indexOf(distr); + if (i != -1) + return i; + } + set.add(distr); + // Add null action if necessary + if (actions != null && actions.get(s) != null) + actions.get(s).add(null); + // Add zero reward if necessary + if (transRewards != null && transRewards.get(s) != null) + transRewards.get(s).add(0.0); + // Update stats + numDistrs++; + maxNumDistrs = Math.max(maxNumDistrs, set.size()); + numTransitions += distr.size(); + return set.size() - 1; + } + + /** + * Remove all rewards from the model + */ + public void clearAllRewards() + { + transRewards = null; + transRewardsConstant = null; + } + + /** + * Set the action label for choice i in some state s. + */ + public void setAction(int s, int i, Object o) + { + // If no actions array created yet, create it + if (actions == null) { + actions = new ArrayList>(numStates); + for (int j = 0; j < numStates; j++) + actions.add(null); + } + // If no actions for state i yet, create list + if (actions.get(s) == null) { + int n = trans.get(s).size(); + List list = new ArrayList(n); + for (int j = 0; j < n; j++) { + list.add(0.0); + } + actions.set(s, list); + } + // Set actions + actions.get(s).set(i, o); + } + + /** + * Set a constant reward for all transitions + */ + public void setConstantTransitionReward(double r) + { + // This replaces any other reward definitions + transRewards = null; + // Store as a Double (because we use null to check for its existence) + transRewardsConstant = new Double(r); + } + + /** + * Set the reward for choice i in some state s to r. + */ + public void setTransitionReward(int s, int i, double r) + { + // This would replace any constant reward definition, if it existed + transRewardsConstant = null; + // If no rewards array created yet, create it + if (transRewards == null) { + transRewards = new ArrayList>(numStates); + for (int j = 0; j < numStates; j++) + transRewards.add(null); + } + // If no rewards for state i yet, create list + if (transRewards.get(s) == null) { + int n = trans.get(s).size(); + List list = new ArrayList(n); + for (int j = 0; j < n; j++) { + list.add(0.0); + } + transRewards.set(s, list); + } + // Set reward + transRewards.get(s).set(i, r); + } + + // Accessors (for ModelSimple) + + @Override + public int getNumTransitions() + { + return numTransitions; + } + + @Override + public boolean isSuccessor(int s1, int s2) + { + for (Distribution distr : trans.get(s1)) { + if (distr.contains(s2)) + return true; + } + return false; + } + + @Override + public boolean allSuccessorsInSet(int s, BitSet set) + { + for (Distribution distr : trans.get(s)) { + if (!distr.isSubsetOf(set)) + return false; + } + return true; + } + + @Override + public boolean someSuccessorsInSet(int s, BitSet set) + { + for (Distribution distr : trans.get(s)) { + if (distr.containsOneOf(set)) + return true; + } + return false; + } + + @Override + public int getNumChoices(int s) + { + return trans.get(s).size(); + } + + @Override + public void checkForDeadlocks(BitSet except) throws PrismException + { + for (int i = 0; i < numStates; i++) { + if (trans.get(i).isEmpty() && (except == null || !except.get(i))) + throw new PrismException("MDP has a deadlock in state " + i); + } + // TODO: Check for empty distributions too? + } + + @Override + public void exportToPrismExplicit(String baseFilename) throws PrismException + { + int i, j; + String filename = null; + FileWriter out; + try { + // Output transitions to .tra file + filename = baseFilename + ".tra"; + out = new FileWriter(filename); + out.write(numStates + " " + numDistrs + " " + numTransitions + "\n"); + for (i = 0; i < numStates; i++) { + j = -1; + for (Distribution distr : trans.get(i)) { + j++; + for (Map.Entry e : distr) { + out.write(i + " " + j + " " + e.getKey() + " " + e.getValue() + "\n"); + } + } + } + out.close(); + // Output transition rewards to .trew file + // TODO + filename = baseFilename + ".trew"; + out = new FileWriter(filename); + out.write(numStates + " " + "?" + " " + "?" + "\n"); + for (i = 0; i < numStates; i++) { + j = -1; + for (Distribution distr : trans.get(i)) { + j++; + for (Map.Entry e : distr) { + out.write(i + " " + j + " " + e.getKey() + " " + "1.0" + "\n"); + } + } + } + out.close(); + } catch (IOException e) { + throw new PrismException("Could not export " + modelType + " to file \"" + filename + "\"" + e); + } + } + + @Override + public void exportToDotFile(String filename, BitSet mark) throws PrismException + { + int i, j; + String nij; + try { + FileWriter out = new FileWriter(filename); + out.write("digraph " + modelType + " {\nsize=\"8,5\"\nnode [shape=box];\n"); + for (i = 0; i < numStates; i++) { + if (mark != null && mark.get(i)) + out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n"); + j = -1; + for (Distribution distr : trans.get(i)) { + j++; + nij = "n" + i + "_" + j; + out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j + "\" ];\n"); + out.write(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n"); + for (Map.Entry e : distr) { + out.write(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); + } + } + } + out.write("}\n"); + out.close(); + } catch (IOException e) { + throw new PrismException("Could not write " + modelType + " to file \"" + filename + "\"" + e); + } + } + + @Override + public String infoString() + { + String s = ""; + s += numStates + " states"; + s += " (" + getNumInitialStates() + " initial)"; + s += ", " + numDistrs + " distributions"; + s += ", " + numTransitions + " transitions"; + s += ", dist max/avg = " + getMaxNumChoices() + "/" + + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates); + return s; + } + + // Accessors (for MDP) + + @Override + public boolean someSuccessorsInSetForAllChoices(int s, BitSet set) + { + for (Distribution distr : trans.get(s)) { + if (!distr.containsOneOf(set)) + return false; + } + return true; + } + + @Override + public boolean someAllSuccessorsInSetForSomeChoices(int s, BitSet set1, BitSet set2) + { + for (Distribution distr : trans.get(s)) { + if (distr.containsOneOf(set1) && distr.isSubsetOf(set2)) + return true; + } + return false; + } + + @Override + public boolean someAllSuccessorsInSetForAllChoices(int s, BitSet set1, BitSet set2) + { + for (Distribution distr : trans.get(s)) { + if (!distr.containsOneOf(set1) || !distr.isSubsetOf(set2)) + return false; + } + return true; + } + + @Override + public double getTransitionReward(int s, int i) + { + List list; + if (transRewardsConstant != null) + return transRewardsConstant; + if (transRewards == null || (list = transRewards.get(s)) == null) + return 0.0; + return list.get(i); + } + + @Override + public void mvMultMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement) + { + int s; + // Loop depends on subset/complement arguments + if (subset == null) { + for (s = 0; s < numStates; s++) + result[s] = mvMultMinMaxSingle(s, vect, min); + } else if (complement) { + for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) + result[s] = mvMultMinMaxSingle(s, vect, min); + } else { + for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) + result[s] = mvMultMinMaxSingle(s, vect, min); + } + } + + @Override + public double mvMultMinMaxSingle(int s, double vect[], boolean min) + { + int k; + double d, prob, minmax; + boolean first; + List step; + + minmax = 0; + first = true; + step = trans.get(s); + for (Distribution distr : step) { + // Compute sum for this distribution + d = 0.0; + for (Map.Entry e : distr) { + k = (Integer) e.getKey(); + prob = (Double) e.getValue(); + d += prob * vect[k]; + } + // Check whether we have exceeded min/max so far + if (first || (min && d < minmax) || (!min && d > minmax)) + minmax = d; + first = false; + } + + return minmax; + } + + @Override + public List mvMultMinMaxSingleChoices(int s, double vect[], boolean min, double val) + { + int j, k; + double d, prob; + List res; + List step; + + // Create data structures to store strategy + res = new ArrayList(); + // One row of matrix-vector operation + j = -1; + step = trans.get(s); + for (Distribution distr : step) { + j++; + // Compute sum for this distribution + d = 0.0; + for (Map.Entry e : distr) { + k = (Integer) e.getKey(); + prob = (Double) e.getValue(); + d += prob * vect[k]; + } + // Store strategy info if value matches + //if (PrismUtils.doublesAreClose(val, d, termCritParam, termCrit == TermCrit.ABSOLUTE)) { + if (PrismUtils.doublesAreClose(val, d, 1e-12, false)) { + res.add(j); + //res.add(distrs.getAction()); + } + } + + return res; + } + + @Override + public void mvMultRewMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement) + { + int s; + // Loop depends on subset/complement arguments + if (subset == null) { + for (s = 0; s < numStates; s++) + result[s] = mvMultRewMinMaxSingle(s, vect, min); + } else if (complement) { + for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) + result[s] = mvMultRewMinMaxSingle(s, vect, min); + } else { + for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) + result[s] = mvMultRewMinMaxSingle(s, vect, min); + } + } + + @Override + public double mvMultRewMinMaxSingle(int s, double vect[], boolean min) + { + int j, k; + double d, prob, minmax; + boolean first; + List step; + + minmax = 0; + first = true; + j = -1; + step = trans.get(s); + for (Distribution distr : step) { + j++; + // Compute sum for this distribution + d = getTransitionReward(s, j); + for (Map.Entry e : distr) { + k = (Integer) e.getKey(); + prob = (Double) e.getValue(); + d += prob * vect[k]; + } + // Check whether we have exceeded min/max so far + if (first || (min && d < minmax) || (!min && d > minmax)) + minmax = d; + first = false; + } + + return minmax; + } + + @Override + public List mvMultRewMinMaxSingleChoices(int s, double vect[], boolean min, double val) + { + int j, k; + double d, prob; + List res; + List step; + + // Create data structures to store strategy + res = new ArrayList(); + // One row of matrix-vector operation + j = -1; + step = trans.get(s); + for (Distribution distr : step) { + j++; + // Compute sum for this distribution + d = getTransitionReward(s, j); + for (Map.Entry e : distr) { + k = (Integer) e.getKey(); + prob = (Double) e.getValue(); + d += prob * vect[k]; + } + // Store strategy info if value matches + //if (PrismUtils.doublesAreClose(val, d, termCritParam, termCrit == TermCrit.ABSOLUTE)) { + if (PrismUtils.doublesAreClose(val, d, 1e-12, false)) { + res.add(j); + //res.add(distrs.getAction()); + } + } + + return res; + } + + // Accessors (other) + + /** + * Get the list of choices (distributions) for state s. + */ + public List getChoices(int s) + { + return trans.get(s); + } + + /** + * Get the ith choice (distribution) for state s. + */ + public Distribution getChoice(int s, int i) + { + return trans.get(s).get(i); + } + + /** + * Get the action (if any) for choice i of state s. + */ + public Object getAction(int s, int i) + { + List list; + if (actions == null || (list = actions.get(s)) == null) + return null; + return list.get(i); + } + + /** + * Get the total number of choices (distributions) over all states. + */ + public int getNumChoices() + { + return numDistrs; + } + + /** + * Get the maximum number of choices (distributions) in any state. + */ + public int getMaxNumChoices() + { + // Recompute if necessary + if (!maxNumDistrsOk) { + maxNumDistrs = 0; + for (int s = 0; s < numStates; s++) + maxNumDistrs = Math.max(maxNumDistrs, getNumChoices(s)); + } + return maxNumDistrs; + } + + // Standard methods + + @Override + public String toString() + { + int i; + boolean first; + String s = ""; + first = true; + s = "[ "; + for (i = 0; i < numStates; i++) { + if (first) + first = false; + else + s += ", "; + s += i + ": " + trans.get(i); + if (actions != null) + s += actions.get(i); + if (transRewards != null) + s += transRewards.get(i); + } + s += " ]"; + return s; + } + + @Override + public boolean equals(Object o) + { + if (o == null || !(o instanceof MDPSimple)) + return false; + MDPSimple mdp = (MDPSimple) o; + if (numStates != mdp.numStates) + return false; + if (!initialStates.equals(mdp.initialStates)) + return false; + if (!trans.equals(mdp.trans)) + return false; + // TODO: compare actions (complicated: null = null,null,null,...) + // TODO: compare rewards (complicated: null = 0,0,0,0) + return true; + } +} diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java index 032a32ce..c2e66436 100644 --- a/prism/src/explicit/PrismSTPGAbstractRefine.java +++ b/prism/src/explicit/PrismSTPGAbstractRefine.java @@ -79,7 +79,7 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine modelConcrete = new CTMCSimple(); break; case MDP: - modelConcrete = new MDP(); + modelConcrete = new MDPSimple(); break; default: throw new PrismException("Cannot handle model type " + modelType); @@ -143,10 +143,10 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine nAbstract = existsRest ? 3 : 2; switch (modelType) { case DTMC: - abstraction = new MDP(nAbstract); + abstraction = new MDPSimple(nAbstract); break; case CTMC: - abstraction = new CTMDP(nAbstract); + abstraction = new CTMDPSimple(nAbstract); // TODO: ((CTMDP) abstraction).unif = ((CTMCSimple) modelConcrete).unif; break; case MDP: @@ -174,15 +174,15 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine switch (modelType) { case DTMC: distr = buildAbstractDistribution(c, (DTMCSimple) modelConcrete); - j = ((MDP) abstraction).addChoice(a, distr); - ((MDP) abstraction).setTransitionReward(a, j, ((DTMC) modelConcrete).getTransitionReward(c)); + j = ((MDPSimple) abstraction).addChoice(a, distr); + ((MDPSimple) abstraction).setTransitionReward(a, j, ((DTMC) modelConcrete).getTransitionReward(c)); break; case CTMC: distr = buildAbstractDistribution(c, (CTMCSimple) modelConcrete); - j = ((CTMDP) abstraction).addChoice(a, distr); + j = ((CTMDPSimple) abstraction).addChoice(a, distr); break; case MDP: - set = buildAbstractDistributionSet(c, (MDP) modelConcrete, (STPG) abstraction); + set = buildAbstractDistributionSet(c, (MDPSimple) modelConcrete, (STPG) abstraction); j = ((STPG) abstraction).addDistributionSet(a, set); break; default: @@ -206,7 +206,7 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine /** * Abstract a concrete state c of an MDP ready to add to an STPG state. */ - protected DistributionSet buildAbstractDistributionSet(int c, MDP mdp, STPG stpg) + protected DistributionSet buildAbstractDistributionSet(int c, MDPSimple mdp, STPG stpg) { DistributionSet set = ((STPG) stpg).newDistributionSet(null); for (Distribution distr : mdp.getChoices(c)) { @@ -328,16 +328,16 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine switch (modelType) { case DTMC: distr = buildAbstractDistribution(c, (DTMCSimple) modelConcrete); - j = ((MDP) abstraction).addChoice(a, distr); - ((MDP) abstraction).setTransitionReward(a, j, ((DTMC) modelConcrete).getTransitionReward(c)); + j = ((MDPSimple) abstraction).addChoice(a, distr); + ((MDPSimple) abstraction).setTransitionReward(a, j, ((DTMC) modelConcrete).getTransitionReward(c)); break; case CTMC: distr = buildAbstractDistribution(c, (CTMCSimple) modelConcrete); - j = ((CTMDP) abstraction).addChoice(a, distr); + j = ((CTMDPSimple) abstraction).addChoice(a, distr); // TODO: recompute unif? break; case MDP: - set = buildAbstractDistributionSet(c, (MDP) modelConcrete, (STPG) abstraction); + set = buildAbstractDistributionSet(c, (MDPSimple) modelConcrete, (STPG) abstraction); j = ((STPG) abstraction).addDistributionSet(a, set); break; default: diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java index a316b7c5..8937113f 100644 --- a/prism/src/explicit/STPG.java +++ b/prism/src/explicit/STPG.java @@ -78,12 +78,12 @@ public class STPG extends ModelSimple * Constructor: build an STPG from an MDP. * Data is copied directly from the MDP so take a copy first if you plan to keep/modify the MDP. */ - public STPG(MDP m) + public STPG(MDPSimple m) { DistributionSet set; int i; // TODO: actions? rewards? - initialise(m.numStates); + initialise(m.getNumStates()); for (i = 0; i < numStates; i++) { set = newDistributionSet(null); set.addAll(m.getChoices(i)); diff --git a/prism/src/explicit/STPGAbstractRefine.java b/prism/src/explicit/STPGAbstractRefine.java index a49e777d..825f55b2 100644 --- a/prism/src/explicit/STPGAbstractRefine.java +++ b/prism/src/explicit/STPGAbstractRefine.java @@ -1187,8 +1187,8 @@ public abstract class STPGAbstractRefine int i, j, k; if (abstraction instanceof STPG) { stpg = (STPG) abstraction; - } else if (abstraction instanceof MDP) { - stpg = new STPG((MDP) abstraction); + } else if (abstraction instanceof MDPSimple) { + stpg = new STPG((MDPSimple) abstraction); } else { throw new PrismException("Cannot export this model type to a dot file"); } diff --git a/prism/src/pta/PTAExpected.java b/prism/src/pta/PTAExpected.java index e6a9c450..6871dbed 100644 --- a/prism/src/pta/PTAExpected.java +++ b/prism/src/pta/PTAExpected.java @@ -298,13 +298,13 @@ public class PTAExpected int src, count, dest, choice, lzRew, rew, i, j; double rewSum; long timer; - MDP mdp; + MDPSimple mdp; int someClock = 1; // Building MDP... mainLog.println("\nBuilding MDP..."); timer = System.currentTimeMillis(); - mdp = new MDP(); + mdp = new MDPSimple(); // Add all states, including a new initial state mdp.addStates(graph.states.size() + 1); diff --git a/prism/src/pta/ReachabilityGraph.java b/prism/src/pta/ReachabilityGraph.java index 070c4208..5751b29e 100644 --- a/prism/src/pta/ReachabilityGraph.java +++ b/prism/src/pta/ReachabilityGraph.java @@ -28,11 +28,8 @@ package pta; import java.util.*; -import explicit.Distribution; -import explicit.MDP; - -import prism.PrismException; -import prism.PrismLog; +import explicit.*; +import prism.*; /** * Class to store a forwards reachability graph for a PTA. @@ -177,10 +174,10 @@ public class ReachabilityGraph { Distribution distr; int numStates, src, count, dest; - MDP mdp; + MDPSimple mdp; // Building MDP... - mdp = new MDP(); + mdp = new MDPSimple(); // Add all states mdp.addStates(states.size());