From 9ba97fe1fceefc62dcd85c1eea647edad47a390f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 14 Sep 2011 09:07:42 +0000 Subject: [PATCH] Add MDPExplicit class to capture shared from MDPSimple/MDPSparse (also a few fixes to same thing done previously for DTMCs). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3709 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCExplicit.java | 47 +++-- prism/src/explicit/DTMCSimple.java | 9 +- prism/src/explicit/MDP.java | 10 + prism/src/explicit/MDPExplicit.java | 261 +++++++++++++++++++++++++++ prism/src/explicit/MDPSimple.java | 233 ++---------------------- prism/src/explicit/MDPSparse.java | 206 +-------------------- 6 files changed, 322 insertions(+), 444 deletions(-) create mode 100644 prism/src/explicit/MDPExplicit.java diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index f4dfa833..b1838c0e 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/prism/src/explicit/DTMCExplicit.java @@ -35,6 +35,7 @@ import java.util.TreeMap; import explicit.rewards.MCRewards; +import prism.ModelType; import prism.PrismException; import prism.PrismLog; import prism.PrismUtils; @@ -44,6 +45,32 @@ import prism.PrismUtils; */ public abstract class DTMCExplicit extends ModelExplicit implements DTMC { + // Accessors (for Model) + + @Override + public ModelType getModelType() + { + return ModelType.DTMC; + } + + @Override + public String infoString() + { + String s = ""; + s += numStates + " states (" + getNumInitialStates() + " initial)"; + s += ", " + getNumTransitions() + " transitions"; + return s; + } + + @Override + public String infoStringTable() + { + String s = ""; + s += "States: " + numStates + " (" + getNumInitialStates() + " initial)\n"; + s += "Transitions: " + getNumTransitions() + "\n"; + return s; + } + @Override public void exportToPrismExplicitTra(PrismLog out) throws PrismException { @@ -133,6 +160,8 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC } } + // Accessors (for DTMC) + @Override public void mvMult(double vect[], double result[], BitSet subset, boolean complement) { @@ -197,22 +226,4 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC result[s] = mvMultRewSingle(s, vect, mcRewards); } } - - @Override - public String infoString() - { - String s = ""; - s += numStates + " states (" + getNumInitialStates() + " initial)"; - s += ", " + getNumTransitions() + " transitions"; - return s; - } - - @Override - public String infoStringTable() - { - String s = ""; - s += "States: " + numStates + " (" + getNumInitialStates() + " initial)\n"; - s += "Transitions: " + getNumTransitions() + "\n"; - return s; - } } diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 93cc9a97..12d563f7 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -31,7 +31,6 @@ import java.util.Map.Entry; import java.io.*; import explicit.rewards.*; -import prism.ModelType; import prism.PrismException; /** @@ -205,13 +204,7 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple } } - // Accessors (for ModelSimple) - - @Override - public ModelType getModelType() - { - return ModelType.DTMC; - } + // Accessors (for Model) @Override public int getNumTransitions() diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index 9948d0ff..eecc63a1 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -36,6 +36,16 @@ import explicit.rewards.*; */ public interface MDP extends Model { + /** + * Get the total number of choices (distributions) over all states. + */ + public int getNumChoices(); + + /** + * Get the maximum number of choices (distributions) in any state. + */ + public int getMaxNumChoices(); + /** * Get the action label (if any) for choice {@code i} of state {@code s}. */ diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java new file mode 100644 index 00000000..4bc89cec --- /dev/null +++ b/prism/src/explicit/MDPExplicit.java @@ -0,0 +1,261 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// * Christian von Essen (Verimag, Grenoble) +// +//------------------------------------------------------------------------------ +// +// 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 explicit.rewards.MDPRewards; +import prism.ModelType; +import prism.PrismException; +import prism.PrismLog; +import prism.PrismUtils; + +/** + * Base class for explicit-state representations of an MDP. + */ +public abstract class MDPExplicit extends ModelExplicit implements MDP +{ + // Accessors (for Model) + + @Override + public ModelType getModelType() + { + return ModelType.MDP; + } + + @Override + public String infoString() + { + String s = ""; + s += numStates + " states (" + getNumInitialStates() + " initial)"; + s += ", " + getNumTransitions() + " transitions"; + s += ", " + getNumChoices() + " choices"; + s += ", dist max/avg = " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) getNumChoices()) / numStates); + return s; + } + + @Override + public String infoStringTable() + { + String s = ""; + s += "States: " + numStates + " (" + getNumInitialStates() + " initial)\n"; + s += "Transitions: " + getNumTransitions() + "\n"; + s += "Choices: " + getNumChoices() + "\n"; + s += "Max/avg: " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) getNumChoices()) / numStates) + "\n"; + return s; + } + + @Override + public void exportToPrismExplicitTra(PrismLog out) throws PrismException + { + int i, j, numChoices; + Object action; + TreeMap sorted; + // Output transitions to .tra file + out.print(numStates + " " + getNumChoices() + " " + getNumTransitions() + "\n"); + sorted = new TreeMap(); + for (i = 0; i < numStates; i++) { + numChoices = getNumChoices(i); + for (j = 0; j < numChoices; j++) { + // Extract transitions and sort by destination state index (to match PRISM-exported files) + Iterator> iter = getTransitionsIterator(i, j); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + sorted.put(e.getKey(), e.getValue()); + } + // Print out (sorted) transitions + for (Map.Entry e : sorted.entrySet()) { + // Note use of PrismUtils.formatDouble to match PRISM-exported files + out.print(i + " " + j + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue())); + action = getAction(i, j); + out.print(action == null ? "\n" : (" " + action + "\n")); + } + sorted.clear(); + } + } + } + + @Override + public void exportToDotFile(String filename, BitSet mark) throws PrismException + { + int i, j, numChoices; + String nij; + Object action; + try { + FileWriter out = new FileWriter(filename); + out.write("digraph " + getModelType() + " {\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"); + numChoices = getNumChoices(i); + for (j = 0; j < numChoices; j++) { + action = getAction(i, j); + nij = "n" + i + "_" + j; + out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j); + if (action != null) + out.write(":" + action); + out.write("\" ];\n"); + out.write(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n"); + Iterator> iter = getTransitionsIterator(i, j); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + out.write(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); + } + } + } + out.write("}\n"); + out.close(); + } catch (IOException e) { + throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e); + } + } + + @Override + public void exportToPrismLanguage(String filename) throws PrismException + { + int i, j, numChoices; + boolean first; + FileWriter out; + TreeMap sorted; + Object action; + try { + // Output transitions to PRISM language file + out = new FileWriter(filename); + out.write(getModelType().keyword() + "\n"); + out.write("module M\nx : [0.." + (numStates - 1) + "];\n"); + sorted = new TreeMap(); + for (i = 0; i < numStates; i++) { + numChoices = getNumChoices(i); + for (j = 0; j < numChoices; j++) { + // Extract transitions and sort by destination state index (to match PRISM-exported files) + Iterator> iter = getTransitionsIterator(i, j); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + sorted.put(e.getKey(), e.getValue()); + } + // Print out (sorted) transitions + action = getAction(i, j); + out.write(action != null ? ("[" + action + "]") : "[]"); + out.write("x=" + i + "->"); + first = true; + for (Map.Entry e : sorted.entrySet()) { + if (first) + first = false; + else + out.write("+"); + // Note use of PrismUtils.formatDouble to match PRISM-exported files + out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")"); + } + out.write(";\n"); + sorted.clear(); + } + } + out.write("endmodule\n"); + out.close(); + } catch (IOException e) { + throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); + } + } + + // Accessors (for MDP) + + @Override + public void mvMultMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement, int adv[]) + { + int s; + // Loop depends on subset/complement arguments + if (subset == null) { + for (s = 0; s < numStates; s++) + result[s] = mvMultMinMaxSingle(s, vect, min, adv); + } else if (complement) { + for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) + result[s] = mvMultMinMaxSingle(s, vect, min, adv); + } else { + for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) + result[s] = mvMultMinMaxSingle(s, vect, min, adv); + } + } + + @Override + public double mvMultGSMinMax(double vect[], boolean min, BitSet subset, boolean complement, boolean absolute) + { + int s; + double d, diff, maxDiff = 0.0; + // Loop depends on subset/complement arguments + if (subset == null) { + for (s = 0; s < numStates; s++) { + d = mvMultJacMinMaxSingle(s, vect, min); + diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); + maxDiff = diff > maxDiff ? diff : maxDiff; + vect[s] = d; + } + } else if (complement) { + for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) { + d = mvMultJacMinMaxSingle(s, vect, min); + diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); + maxDiff = diff > maxDiff ? diff : maxDiff; + vect[s] = d; + } + } else { + for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) { + d = mvMultJacMinMaxSingle(s, vect, min); + diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); + maxDiff = diff > maxDiff ? diff : maxDiff; + vect[s] = d; + } + } + // Use this code instead for backwards Gauss-Seidel + /*for (s = numStates - 1; s >= 0; s--) { + if (subset.get(s)) { + d = mvMultJacMinMaxSingle(s, vect, min); + diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); + maxDiff = diff > maxDiff ? diff : maxDiff; + vect[s] = d; + } + }*/ + return maxDiff; + } + + @Override + public void mvMultRewMinMax(double vect[], MDPRewards mdpRewards, boolean min, double result[], BitSet subset, boolean complement, int adv[]) + { + int s; + // Loop depends on subset/complement arguments + if (subset == null) { + for (s = 0; s < numStates; s++) + result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, adv); + } else if (complement) { + for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) + result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, adv); + } else { + for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) + result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, adv); + } + } +} diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index cdf21677..5a8fde33 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -32,10 +32,7 @@ import java.util.Map.Entry; import java.io.*; import explicit.rewards.MDPRewards; -import explicit.rewards.MDPRewardsSimple; -import prism.ModelType; import prism.PrismException; -import prism.PrismLog; import prism.PrismUtils; /** @@ -44,7 +41,7 @@ import prism.PrismUtils; * The model is, however, easy to manipulate. For a static model (i.e. one that does not change * after creation), consider MDPSparse, which is more efficient. */ -public class MDPSimple extends ModelExplicit implements MDP, ModelSimple +public class MDPSimple extends MDPExplicit implements ModelSimple { // Transition function (Steps) protected List> trans; @@ -384,13 +381,7 @@ public class MDPSimple extends ModelExplicit implements MDP, ModelSimple actions.get(s).set(i, o); } - // Accessors (for ModelSimple) - - @Override - public ModelType getModelType() - { - return ModelType.MDP; - } + // Accessors (for Model) @Override public int getNumTransitions() @@ -464,139 +455,26 @@ public class MDPSimple extends ModelExplicit implements MDP, ModelSimple return deadlocks; } - @Override - public void exportToPrismExplicitTra(PrismLog out) throws PrismException - { - int i, j; - Object action; - TreeMap sorted; - // Output transitions to .tra file - out.print(numStates + " " + numDistrs + " " + numTransitions + "\n"); - sorted = new TreeMap(); - for (i = 0; i < numStates; i++) { - j = -1; - for (Distribution distr : trans.get(i)) { - j++; - // Extract transitions and sort by destination state index (to match PRISM-exported files) - for (Map.Entry e : distr) { - sorted.put(e.getKey(), e.getValue()); - } - // Print out (sorted) transitions - for (Map.Entry e : sorted.entrySet()) { - // Note use of PrismUtils.formatDouble to match PRISM-exported files - out.print(i + " " + j + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue())); - action = getAction(i, j); - out.print(action == null ? "\n" : (" " + action + "\n")); - } - sorted.clear(); - } - } - } + // Accessors (for MDP) @Override - public void exportToDotFile(String filename, BitSet mark) throws PrismException + public int getNumChoices() { - int i, j; - String nij; - Object action; - try { - FileWriter out = new FileWriter(filename); - out.write("digraph " + getModelType() + " {\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++; - action = getAction(i, j); - nij = "n" + i + "_" + j; - out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j); - if (action != null) - out.write(":" + action); - out.write("\" ];\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 " + getModelType() + " to file \"" + filename + "\"" + e); - } + return numDistrs; } @Override - public void exportToPrismLanguage(String filename) throws PrismException + public int getMaxNumChoices() { - int i, j; - boolean first; - FileWriter out; - TreeMap sorted; - Object action; - try { - // Output transitions to PRISM language file - out = new FileWriter(filename); - out.write(getModelType().keyword() + "\n"); - out.write("module M\nx : [0.." + (numStates - 1) + "];\n"); - sorted = new TreeMap(); - for (i = 0; i < numStates; i++) { - j = -1; - for (Distribution distr : trans.get(i)) { - j++; - // Extract transitions and sort by destination state index (to match PRISM-exported files) - for (Map.Entry e : distr) { - sorted.put(e.getKey(), e.getValue()); - } - // Print out (sorted) transitions - action = getAction(i, j); - out.write(action != null ? ("[" + action + "]") : "[]"); - out.write("x=" + i + "->"); - first = true; - for (Map.Entry e : sorted.entrySet()) { - if (first) - first = false; - else - out.write("+"); - // Note use of PrismUtils.formatDouble to match PRISM-exported files - out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")"); - } - out.write(";\n"); - sorted.clear(); - } - } - out.write("endmodule\n"); - out.close(); - } catch (IOException e) { - throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); + // Recompute if necessary + if (!maxNumDistrsOk) { + maxNumDistrs = 0; + for (int s = 0; s < numStates; s++) + maxNumDistrs = Math.max(maxNumDistrs, getNumChoices(s)); } + return maxNumDistrs; } - @Override - public String infoString() - { - String s = ""; - s += numStates + " states (" + getNumInitialStates() + " initial)"; - s += ", " + numTransitions + " transitions"; - s += ", " + numDistrs + " choices"; - s += ", dist max/avg = " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates); - return s; - } - - @Override - public String infoStringTable() - { - String s = ""; - s += "States: " + numStates + " (" + getNumInitialStates() + " initial)\n"; - s += "Transitions: " + numTransitions + "\n"; - s += "Choices: " + numDistrs + "\n"; - s += "Max/avg: " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates) + "\n"; - return s; - } - - // Accessors (for MDP) - @Override public Object getAction(int s, int i) { @@ -672,23 +550,6 @@ public class MDPSimple extends ModelExplicit implements MDP, ModelSimple } } - @Override - public void mvMultMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement, int adv[]) - { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultMinMaxSingle(s, vect, min, adv); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultMinMaxSingle(s, vect, min, adv); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultMinMaxSingle(s, vect, min, adv); - } - } - @Override public double mvMultMinMaxSingle(int s, double vect[], boolean min, int adv[]) { @@ -782,37 +643,6 @@ public class MDPSimple extends ModelExplicit implements MDP, ModelSimple return d; } - @Override - public double mvMultGSMinMax(double vect[], boolean min, BitSet subset, boolean complement, boolean absolute) - { - int s; - double d, diff, maxDiff = 0.0; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) { - d = mvMultJacMinMaxSingle(s, vect, min); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) { - d = mvMultJacMinMaxSingle(s, vect, min); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) { - d = mvMultJacMinMaxSingle(s, vect, min); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } - return maxDiff; - } - @Override public double mvMultJacMinMaxSingle(int s, double vect[], boolean min) { @@ -873,23 +703,6 @@ public class MDPSimple extends ModelExplicit implements MDP, ModelSimple return d; } - @Override - public void mvMultRewMinMax(double vect[], MDPRewards mdpRewards, boolean min, double result[], BitSet subset, boolean complement, int adv[]) - { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, adv); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, adv); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, adv); - } - } - @Override public double mvMultRewMinMaxSingle(int s, double vect[], MDPRewards mdpRewards, boolean min, int adv[]) { @@ -998,28 +811,6 @@ public class MDPSimple extends ModelExplicit implements MDP, ModelSimple return trans.get(s).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; - } - /** * Returns the index of the choice {@code distr} for state {@code s}, if it exists. * If none, -1 is returned. If there are multiple (i.e. allowDupes is true), the first is returned. diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index cf3feebe..fb8f58b7 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -33,9 +33,7 @@ import java.io.*; import explicit.rewards.MDPRewards; import parser.State; -import prism.ModelType; import prism.PrismException; -import prism.PrismLog; import prism.PrismUtils; /** @@ -43,7 +41,7 @@ import prism.PrismUtils; * This is much faster to access than e.g. MDPSimple and should also be more compact. * The catch is that you have to create the model all in one go and then can't modify it. */ -public class MDPSparse extends ModelExplicit implements MDP +public class MDPSparse extends MDPExplicit { // Sparse matrix storing transition function (Steps) /** Probabilities for each transition (array of size numTransitions) */ @@ -277,7 +275,7 @@ public class MDPSparse extends ModelExplicit implements MDP rowStarts[numStates] = numDistrs; } - // Mutators (for ModelSparse) + // Mutators (other) @Override public void initialise(int numStates) @@ -369,13 +367,7 @@ public class MDPSparse extends ModelExplicit implements MDP } } - // Accessors (for ModelSparse) - - @Override - public ModelType getModelType() - { - return ModelType.MDP; - } + // Accessors (for Model) @Override public int getNumTransitions() @@ -472,127 +464,20 @@ public class MDPSparse extends ModelExplicit implements MDP return deadlocks; } - @Override - public void exportToPrismExplicitTra(PrismLog out) throws PrismException - { - // Note: In PRISM .tra files, transitions are usually sorted by column index within choices - // (to ensure this is the case, you may need to sort the model when constructing) - int i, j, k, l1, h1, l2, h2; - Object action; - // Output transitions to .tra file - out.print(numStates + " " + numDistrs + " " + numTransitions + "\n"); - for (i = 0; i < numStates; i++) { - l1 = rowStarts[i]; - h1 = rowStarts[i + 1]; - for (j = l1; j < h1; j++) { - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - out.print(i + " " + (j - l1) + " " + cols[k] + " " + PrismUtils.formatDouble(nonZeros[k])); - action = getAction(i, j - l1); - out.print(action == null ? "\n" : (" " + action + "\n")); - } - } - } - } - - @Override - public void exportToDotFile(String filename, BitSet mark) throws PrismException - { - int i, j, k, l1, h1, l2, h2; - String nij; - Object action; - try { - FileWriter out = new FileWriter(filename); - out.write("digraph " + getModelType() + " {\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"); - l1 = rowStarts[i]; - h1 = rowStarts[i + 1]; - for (j = l1; j < h1; j++) { - action = getAction(i, j - l1); - nij = "n" + i + "_" + (j - l1); - out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j); - if (action != null) - out.write(":" + action); - out.write("\" ];\n"); - out.write(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n"); - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - out.write(nij + " -> " + cols[k] + " [ label=\"" + nonZeros[k] + "\" ];\n"); - } - } - } - out.write("}\n"); - out.close(); - } catch (IOException e) { - throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e); - } - } - - @Override - public void exportToPrismLanguage(String filename) throws PrismException - { - int i, j, k, l1, h1, l2, h2; - FileWriter out; - Object action; - try { - // Output transitions to PRISM language file - out = new FileWriter(filename); - out.write(getModelType().keyword() + "\n"); - out.write("module M\nx : [0.." + (numStates - 1) + "];\n"); - for (i = 0; i < numStates; i++) { - l1 = rowStarts[i]; - h1 = rowStarts[i + 1]; - for (j = l1; j < h1; j++) { - // Print out transitions - action = getAction(i, j - l1); - out.write(action != null ? ("[" + action + "]") : "[]"); - out.write("x=" + i + "->"); - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - if (k > l2) - out.write("+"); - // Note use of PrismUtils.formatDouble to match PRISM-exported files - out.write(PrismUtils.formatDouble(nonZeros[k]) + ":(x'=" + cols[k] + ")"); - } - out.write(";\n"); - } - } - out.write("endmodule\n"); - out.close(); - } catch (IOException e) { - throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); - } - } + // Accessors (for MDP) @Override - public String infoString() + public int getNumChoices() { - String s = ""; - s += numStates + " states (" + getNumInitialStates() + " initial)"; - s += ", " + numTransitions + " transitions"; - s += ", " + numDistrs + " choices"; - s += ", dist max/avg = " + maxNumDistrs + "/" + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates); - return s; + return numDistrs; } @Override - public String infoStringTable() + public int getMaxNumChoices() { - String s = ""; - s += "States: " + numStates + " (" + getNumInitialStates() + " initial)\n"; - s += "Transitions: " + numTransitions + "\n"; - s += "Choices: " + numDistrs + "\n"; - s += "Max/avg: " + maxNumDistrs + "/" + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates) + "\n"; - return s; + return maxNumDistrs; } - // Accessors (for MDP) - @Override public Object getAction(int s, int i) { @@ -738,23 +623,6 @@ public class MDPSparse extends ModelExplicit implements MDP } } - @Override - public void mvMultMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement, int adv[]) - { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultMinMaxSingle(s, vect, min, adv); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultMinMaxSingle(s, vect, min, adv); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultMinMaxSingle(s, vect, min, adv); - } - } - @Override public double mvMultMinMaxSingle(int s, double vect[], boolean min, int adv[]) { @@ -843,46 +711,6 @@ public class MDPSparse extends ModelExplicit implements MDP return d; } - @Override - public double mvMultGSMinMax(double vect[], boolean min, BitSet subset, boolean complement, boolean absolute) - { - int s; - double d, diff, maxDiff = 0.0; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) { - d = mvMultJacMinMaxSingle(s, vect, min); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) { - d = mvMultJacMinMaxSingle(s, vect, min); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) { - d = mvMultJacMinMaxSingle(s, vect, min); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - // Use this code instead for backwards Gauss-Seidel - /*for (s = numStates - 1; s >= 0; s--) { - if (subset.get(s)) { - d = mvMultJacMinMaxSingle(s, vect, min); - diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d); - maxDiff = diff > maxDiff ? diff : maxDiff; - vect[s] = d; - } - }*/ - } - return maxDiff; - } - @Override public double mvMultJacMinMaxSingle(int s, double vect[], boolean min) { @@ -943,23 +771,6 @@ public class MDPSparse extends ModelExplicit implements MDP return d; } - @Override - public void mvMultRewMinMax(double vect[], MDPRewards mdpRewards, boolean min, double result[], BitSet subset, boolean complement, int adv[]) - { - int s; - // Loop depends on subset/complement arguments - if (subset == null) { - for (s = 0; s < numStates; s++) - result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, adv); - } else if (complement) { - for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) - result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, adv); - } else { - for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) - result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, adv); - } - } - @Override public double mvMultRewMinMaxSingle(int s, double vect[], MDPRewards mdpRewards, boolean min, int adv[]) { @@ -1044,6 +855,7 @@ public class MDPSparse extends ModelExplicit implements MDP } } } + // Standard methods @Override