diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index 4d23b012..f89509ef 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/prism/src/explicit/DTMCExplicit.java @@ -72,7 +72,7 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC } @Override - public void exportToPrismExplicitTra(PrismLog out) throws PrismException + public void exportToPrismExplicitTra(PrismLog out) { int i; TreeMap sorted; diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java new file mode 100644 index 00000000..249cb55c --- /dev/null +++ b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java @@ -0,0 +1,260 @@ +//============================================================================== +// +// Copyright (c) 2013- +// Authors: +// * Dave Parker (University of Birmingham/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.util.Map.Entry; + +import explicit.rewards.MCRewards; +import parser.State; +import parser.Values; +import prism.ModelType; +import prism.PrismException; +import strat.MDStrategy; + +/** +* Explicit-state representation of a DTMC, constructed (implicitly) +* from an MDP and a memoryless deterministic (MD) adversary. +* This class is read-only: most of the data is pointers to other model info. +*/ +public class DTMCFromMDPAndMDStrategy extends DTMCExplicit +{ + // Parent MDP + protected MDP mdp; + // MD strategy + protected MDStrategy strat; + + /** + * Constructor: create from MDP and memoryless adversary. + */ + public DTMCFromMDPAndMDStrategy(MDP mdp, MDStrategy strat) + { + this.mdp = mdp; + this.numStates = mdp.getNumStates(); + this.strat = strat; + } + + @Override + public void buildFromPrismExplicit(String filename) throws PrismException + { + throw new PrismException("Not supported"); + } + + // Accessors (for Model) + + public ModelType getModelType() + { + return ModelType.DTMC; + } + + public int getNumStates() + { + return mdp.getNumStates(); + } + + public int getNumInitialStates() + { + return mdp.getNumInitialStates(); + } + + public Iterable getInitialStates() + { + return mdp.getInitialStates(); + } + + public int getFirstInitialState() + { + return mdp.getFirstInitialState(); + } + + public boolean isInitialState(int i) + { + return mdp.isInitialState(i); + } + + public boolean isDeadlockState(int i) + { + return mdp.isDeadlockState(i); + } + + public List getStatesList() + { + return mdp.getStatesList(); + } + + public Values getConstantValues() + { + return mdp.getConstantValues(); + } + + public int getNumTransitions() + { + int numTransitions = 0; + for (int s = 0; s < numStates; s++) + if (strat.isChoiceDefined(s)) + numTransitions += mdp.getNumTransitions(s, strat.getChoiceIndex(s)); + return numTransitions; + } + + public Iterator getSuccessorsIterator(final int s) + { + throw new RuntimeException("Not implemented yet"); + } + + public boolean isSuccessor(int s1, int s2) + { + throw new RuntimeException("Not implemented yet"); + } + + public boolean allSuccessorsInSet(int s, BitSet set) + { + throw new RuntimeException("Not implemented yet"); + } + + public boolean someSuccessorsInSet(int s, BitSet set) + { + throw new RuntimeException("Not implemented yet"); + } + + public int getNumChoices(int s) + { + // Always 1 for a DTMC + return 1; + } + + public void findDeadlocks(boolean fix) throws PrismException + { + // No deadlocks by definition + } + + public void checkForDeadlocks() throws PrismException + { + // No deadlocks by definition + } + + public void checkForDeadlocks(BitSet except) throws PrismException + { + // No deadlocks by definition + } + + @Override + public String infoString() + { + return mdp.infoString() + " + " + "???"; // TODO + } + + @Override + public String infoStringTable() + { + return mdp.infoString() + " + " + "???\n"; // TODO + } + + // Accessors (for DTMC) + + public double getNumTransitions(int s) + { + return strat.isChoiceDefined(s) ? mdp.getNumTransitions(s, strat.getChoiceIndex(s)) : 0; + } + + public Iterator> getTransitionsIterator(int s) + { + if (strat.isChoiceDefined(s)) { + return mdp.getTransitionsIterator(s, strat.getChoiceIndex(s)); + } else { + // Empty iterator + return new Iterator>() + { + @Override + public boolean hasNext() + { + return false; + } + + @Override + public Entry next() + { + return null; + } + + @Override + public void remove() + { + throw new UnsupportedOperationException(); + } + }; + } + } + + public void prob0step(BitSet subset, BitSet u, BitSet result) + { + // TODO + throw new Error("Not yet supported"); + } + + public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result) + { + // TODO + throw new Error("Not yet supported"); + } + + @Override + public double mvMultSingle(int s, double vect[]) + { + return strat.isChoiceDefined(s) ? mdp.mvMultSingle(s, strat.getChoiceIndex(s), vect) : 0; + } + + @Override + public double mvMultJacSingle(int s, double vect[]) + { + return strat.isChoiceDefined(s) ? mdp.mvMultJacSingle(s, strat.getChoiceIndex(s), vect) : 0; + } + + @Override + public double mvMultRewSingle(int s, double vect[], MCRewards mcRewards) + { + throw new RuntimeException("Not implemented yet"); + //return mdp.mvMultRewSingle(s, adv[s], vect); + } + + @Override + public void vmMult(double vect[], double result[]) + { + throw new RuntimeException("Not implemented yet"); + } + + @Override + public String toString() + { + throw new RuntimeException("Not implemented yet"); + } + + @Override + public boolean equals(Object o) + { + throw new RuntimeException("Not implemented yet"); + } +} diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index 1e1e4bbb..65d6fcd6 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/prism/src/explicit/MDPExplicit.java @@ -38,6 +38,7 @@ import prism.ModelType; import prism.PrismException; import prism.PrismLog; import prism.PrismUtils; +import strat.MDStrategy; import explicit.rewards.MDPRewards; /** @@ -76,7 +77,7 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP } @Override - public void exportToPrismExplicitTra(PrismLog out) throws PrismException + public void exportToPrismExplicitTra(PrismLog out) { int i, j, numChoices; Object action; @@ -339,4 +340,10 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP }*/ return maxDiff; } + + @Override + public Model constructInducedModel(MDStrategy strat) + { + return new DTMCFromMDPAndMDStrategy(this, strat); + } } diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 744216c3..9b25a95f 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -185,7 +185,7 @@ public interface Model /** * Export transition matrix to explicit format readable by PRISM (i.e. a .tra file). */ - public void exportToPrismExplicitTra(PrismLog log) throws PrismException; + public void exportToPrismExplicitTra(PrismLog log); /** * Export to a dot file. diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index 7a9b6e5e..2500d049 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -258,17 +258,25 @@ public abstract class ModelExplicit implements Model @Override public void exportToPrismExplicitTra(String filename) throws PrismException { - exportToPrismExplicitTra(new PrismFileLog(filename)); + PrismLog tmpLog = new PrismFileLog(filename); + if (!tmpLog.ready()) { + throw new PrismException("Could not open file \"" + filename + "\" for output"); + } + exportToPrismExplicitTra(tmpLog); } @Override public void exportToPrismExplicitTra(File file) throws PrismException { + PrismLog tmpLog = new PrismFileLog(file.getPath()); + if (!tmpLog.ready()) { + throw new PrismException("Could not open file \"" + file + "\" for output"); + } exportToPrismExplicitTra(new PrismFileLog(file.getPath())); } @Override - public abstract void exportToPrismExplicitTra(PrismLog out) throws PrismException; + public abstract void exportToPrismExplicitTra(PrismLog out); @Override public void exportToDotFile(String filename) throws PrismException diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java index 01e9f6c7..cd9f66a6 100644 --- a/prism/src/explicit/NondetModel.java +++ b/prism/src/explicit/NondetModel.java @@ -30,6 +30,8 @@ import java.util.BitSet; import java.util.Iterator; import java.util.Map.Entry; +import strat.MDStrategy; + /** * Interface for (abstract) classes that provide (read-only) access to an explicit-state model with nondeterminism. */ @@ -77,4 +79,11 @@ public interface NondetModel extends Model * Get an iterator over the transitions of state s and action i. */ public Iterator> getTransitionsIterator(int s, int i); + + /** + * Construct a model that is induced by applying strategy {@code strat} to this model. + * Note that the "new" model may be just an implicit (read-only) representation. + * @param strat (Memoryless) strategy to use + */ + public Model constructInducedModel(MDStrategy strat); } \ No newline at end of file diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index f0a4f622..278838bc 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -36,6 +36,7 @@ import prism.ModelType; import prism.PrismException; import prism.PrismLog; import prism.PrismUtils; +import strat.MDStrategy; /** * Simple explicit-state representation of a stochastic two-player game (STPG), @@ -363,7 +364,7 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS } @Override - public void exportToPrismExplicitTra(PrismLog out) throws PrismException + public void exportToPrismExplicitTra(PrismLog out) { int i, j, k; TreeMap sorted; @@ -521,6 +522,12 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS return null; } + @Override + public Model constructInducedModel(MDStrategy strat) + { + throw new RuntimeException("Not implemented"); + } + @Override public boolean isChoiceNested(int s, int i) { diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java index 295bb9ec..802c4038 100644 --- a/prism/src/explicit/SubNondetModel.java +++ b/prism/src/explicit/SubNondetModel.java @@ -28,7 +28,6 @@ package explicit; import java.io.File; -import java.io.NotSerializableException; import java.util.ArrayList; import java.util.BitSet; import java.util.HashMap; @@ -36,7 +35,6 @@ import java.util.Iterator; import java.util.List; import java.util.Map; import java.util.Map.Entry; -import java.util.NoSuchElementException; import parser.State; import parser.Values; @@ -44,6 +42,7 @@ import parser.VarList; import prism.ModelType; import prism.PrismException; import prism.PrismLog; +import strat.MDStrategy; /* * Class for creating a sub-model of any NondetModel, please note the translate* methods @@ -235,7 +234,7 @@ public class SubNondetModel implements NondetModel { } @Override - public void exportToPrismExplicitTra(PrismLog log) throws PrismException { + public void exportToPrismExplicitTra(PrismLog log) { throw new UnsupportedOperationException(); } @@ -358,6 +357,12 @@ public class SubNondetModel implements NondetModel { return distrs.entrySet().iterator(); } + @Override + public Model constructInducedModel(MDStrategy strat) + { + throw new RuntimeException("Not implemented"); + } + private void generateLookupTable(BitSet states, Map actions) { for(int i=0;i < model.getNumStates();i++) { if(states.get(i)) { diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index 17e44b0c..f5593ba0 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -178,7 +178,7 @@ final class ParamModel extends ModelExplicit } @Override - public void exportToPrismExplicitTra(PrismLog log) throws PrismException + public void exportToPrismExplicitTra(PrismLog log) { throw new UnsupportedOperationException(); } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 4be68c59..8e649263 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -153,6 +153,24 @@ public class Prism extends PrismComponent implements PrismSettingsListener public static final int LOCKSTEP = 2; public static final int SCCFIND = 3; + // Options for type of strategy export + public enum StrategyExportType { + ACTIONS, INDICES, INDUCED_MODEL; + public String description() + { + switch (this) { + case ACTIONS: + return "as actions"; + case INDICES: + return "as indices"; + case INDUCED_MODEL: + return "as an induced model"; + default: + return this.toString(); + } + } + } + //------------------------------------------------------------------------------ // Settings / flags / options //------------------------------------------------------------------------------ @@ -2918,27 +2936,34 @@ public class Prism extends PrismComponent implements PrismSettingsListener } /** - * Export a strategy (for the currently loaded model); - * TODO: is it necessarily loaded? + * Export a strategy. The associated model should be attached to the strategy. + * Strictly, speaking that does not need to be the currently loaded model, + * but it would probably have been discarded if that was not the case. * @param strat The strategy + * @param exportType The type of output * @param file File to output the path to (stdout if null) */ - public void exportStrategy(Strategy strat, File file) throws FileNotFoundException, PrismException + public void exportStrategy(Strategy strat, StrategyExportType exportType, File file) throws FileNotFoundException, PrismException { PrismLog tmpLog; // Print message - mainLog.print("\nExporting strategy "); - //mainLog.print(getStringForExportType(exportType) + " "); + mainLog.print("\nExporting strategy " + exportType.description() + " "); mainLog.println(getDestinationStringForFile(file)); - // Create new file log or use main log + // Export to file (or use main log) tmpLog = getPrismLogForFile(file); - - // Export - strat.exportActions(tmpLog); - - // Tidy up + switch (exportType) { + case ACTIONS: + strat.exportActions(tmpLog); + break; + case INDICES: + strat.exportIndices(tmpLog); + break; + case INDUCED_MODEL: + strat.exportInducedModel(tmpLog); + break; + } if (file != null) tmpLog.close(); } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index bc11cae5..9aec2f8f 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -38,6 +38,7 @@ import parser.ast.ExpressionReward; import parser.ast.ModulesFile; import parser.ast.PropertiesFile; import parser.ast.Property; +import prism.Prism.StrategyExportType; import simulator.GenerateSimulationPath; import simulator.method.ACIconfidence; import simulator.method.ACIiterations; @@ -188,6 +189,9 @@ public class PrismCL implements PrismModelListener private boolean simManual = false; private SimulationMethod simMethod = null; + // strategy export info + private Prism.StrategyExportType exportStratType = StrategyExportType.ACTIONS; + // parametric analysis info private String[] paramLowerBounds = null; private String[] paramUpperBounds = null; @@ -377,7 +381,7 @@ public class PrismCL implements PrismModelListener // if a strategy was generated, and we need to export it, do so if (exportstrat && res.getStrategy() != null) { try { - prism.exportStrategy(res.getStrategy(), exportStratFilename.equals("stdout") ? null : new File(exportStratFilename)); + prism.exportStrategy(res.getStrategy(), exportStratType, exportStratFilename.equals("stdout") ? null : new File(exportStratFilename)); } // in case of error, report it and proceed catch (FileNotFoundException e) { @@ -1806,7 +1810,19 @@ public class PrismCL implements PrismModelListener // Ignore "" if (opt.equals("")) { } - // TODO: add some options + else if (opt.startsWith("type")) { + if (!opt.startsWith("type=")) + throw new PrismException("No value provided for \"type\" option of -exportstrat"); + String optVal = opt.substring(5); + if (optVal.equals("actions")) + exportStratType = StrategyExportType.ACTIONS; + else if (optVal.equals("indices")) + exportStratType = StrategyExportType.INDICES; + else if (optVal.equals("induced")) + exportStratType = StrategyExportType.INDUCED_MODEL; + else + throw new PrismException("Unknown value \"" + optVal + "\" provided for \"type\" option of -exportstrat"); + } // Unknown option else { throw new PrismException("Unknown option \"" + opt + "\" for -exportstrat switch"); diff --git a/prism/src/strat/MDStrategy.java b/prism/src/strat/MDStrategy.java index 72d66aaf..3b3b8dc5 100644 --- a/prism/src/strat/MDStrategy.java +++ b/prism/src/strat/MDStrategy.java @@ -44,6 +44,11 @@ public abstract class MDStrategy implements Strategy */ public abstract int getNumStates(); + /** + * Is choice information stored for state s? + */ + public abstract boolean isChoiceDefined(int s); + /** * Get the type of choice information stored for state s. */ @@ -86,9 +91,18 @@ public abstract class MDStrategy implements Strategy { int n = getNumStates(); for (int s = 0; s < n; s++) { - // Only print actions for reachable states - if (getChoice(s) != Choice.UNREACHABLE) + if (isChoiceDefined(s)) out.println(s + ":" + getChoiceAction(s)); } } + + @Override + public void exportIndices(PrismLog out) + { + int n = getNumStates(); + for (int s = 0; s < n; s++) { + if (isChoiceDefined(s)) + out.println(s + ":" + getChoiceIndex(s)); + } + } } diff --git a/prism/src/strat/MDStrategyArray.java b/prism/src/strat/MDStrategyArray.java index 58aa9f80..63270226 100644 --- a/prism/src/strat/MDStrategyArray.java +++ b/prism/src/strat/MDStrategyArray.java @@ -27,6 +27,10 @@ package strat; +import prism.PrismLog; +import explicit.MDP; +import explicit.Model; + /** * Class to store a memoryless deterministic (MD) strategy, as a (Java) array of choice indices. */ @@ -37,7 +41,7 @@ public class MDStrategyArray extends MDStrategy // Index of choice taken in each state (wrt model above) // Other possible values: -1 (unknown), -2 (arbitrary), -3 (unreachable) private int choices[]; - + /** * Creates an MDStrategyArray from an integer array of choices. * The array may later be modified/delete - take a copy if you want to keep it. @@ -47,15 +51,21 @@ public class MDStrategyArray extends MDStrategy this.model = model; this.choices = choices; } - + // Methods for MDStrategy - + @Override public int getNumStates() { return model.getNumStates(); } - + + @Override + public boolean isChoiceDefined(int s) + { + return choices[s] >= 0; + } + @Override public Strategy.Choice getChoice(int s) { @@ -70,13 +80,13 @@ public class MDStrategyArray extends MDStrategy return Choice.INDEX; } } - + @Override public int getChoiceIndex(int s) { return choices[s]; } - + @Override public Object getChoiceAction(int s) { @@ -85,7 +95,14 @@ public class MDStrategyArray extends MDStrategy } // Methods for Strategy - + + @Override + public void exportInducedModel(PrismLog out) + { + Model dtmcInd = model.constructInducedModel(this); + dtmcInd.exportToPrismExplicitTra(out); + } + @Override public void clear() { diff --git a/prism/src/strat/MDStrategyIV.java b/prism/src/strat/MDStrategyIV.java index 1c446292..adad6483 100644 --- a/prism/src/strat/MDStrategyIV.java +++ b/prism/src/strat/MDStrategyIV.java @@ -29,8 +29,10 @@ package strat; import java.util.List; import dv.IntegerVector; +import explicit.MDP; import prism.Model; +import prism.PrismLog; import strat.Strategy.Choice; /** @@ -65,6 +67,12 @@ public class MDStrategyIV extends MDStrategy return numStates; } + @Override + public boolean isChoiceDefined(int s) + { + return iv.getElement(s) >= 0; + } + @Override public Strategy.Choice getChoice(int s) { @@ -96,6 +104,12 @@ public class MDStrategyIV extends MDStrategy // Methods for Strategy + @Override + public void exportInducedModel(PrismLog out) + { + // TODO + } + @Override public void clear() { diff --git a/prism/src/strat/Strategy.java b/prism/src/strat/Strategy.java index aa73cc15..9900f95b 100644 --- a/prism/src/strat/Strategy.java +++ b/prism/src/strat/Strategy.java @@ -44,6 +44,16 @@ public interface Strategy */ public void exportActions(PrismLog out); + /** + * Export the strategy to a PrismLog, displaying strategy choices as indices. + */ + public void exportIndices(PrismLog out); + + /** + * Export the model induced by this strategy to a PrismLog. + */ + public void exportInducedModel(PrismLog out); + /** * Initialise the strategy, based on an initial model state. * @param s Initial state of the model