diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 67eda68a..488e2c0d 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -30,6 +30,11 @@ import java.io.File; import java.util.BitSet; import java.util.List; +import explicit.rewards.ConstructRewards; +import explicit.rewards.MCRewards; +import explicit.rewards.MDPRewards; +import explicit.rewards.Rewards; +import explicit.rewards.STPGRewards; import parser.ast.Coalition; import parser.ast.Expression; import parser.ast.ExpressionProb; @@ -47,13 +52,10 @@ import prism.IntegerBound; import prism.OpRelOpBound; import prism.PrismComponent; import prism.PrismException; +import prism.PrismLog; import prism.PrismNotSupportedException; import prism.PrismSettings; -import explicit.rewards.ConstructRewards; -import explicit.rewards.MCRewards; -import explicit.rewards.MDPRewards; -import explicit.rewards.Rewards; -import explicit.rewards.STPGRewards; +import prism.PrismUtils; /** * Super class for explicit-state probabilistic model checkers. @@ -1236,4 +1238,57 @@ public class ProbModelChecker extends NonProbModelChecker return dist; } + + /** + * Export (non-zero) state rewards for one reward structure of a model. + * @param model The model + * @param r Index of reward structure to export (0-indexed) + * @param exportType The format in which to export + * @param out Where to export + */ + public void exportStateRewardsToFile(Model model, int r, int exportType, PrismLog out) throws PrismException + { + int numStates = model.getNumStates(); + int nonZeroRews = 0; + + Rewards modelRewards = constructRewards(model, r); + switch (model.getModelType()) { + case DTMC: + case CTMC: + MCRewards mcRewards = (MCRewards) modelRewards; + for (int s = 0; s < numStates; s++) { + double d = mcRewards.getStateReward(s); + if (d != 0) { + nonZeroRews++; + } + } + out.println(numStates + " " + nonZeroRews); + for (int s = 0; s < numStates; s++) { + double d = mcRewards.getStateReward(s); + if (d != 0) { + out.println(s + " " + PrismUtils.formatDouble(d)); + } + } + break; + case MDP: + case STPG: + MDPRewards mdpRewards = (MDPRewards) modelRewards; + for (int s = 0; s < numStates; s++) { + double d = mdpRewards.getStateReward(s); + if (d != 0) { + nonZeroRews++; + } + } + out.println(numStates + " " + nonZeroRews); + for (int s = 0; s < numStates; s++) { + double d = mdpRewards.getStateReward(s); + if (d != 0) { + out.println(s + " " + PrismUtils.formatDouble(d)); + } + } + break; + default: + throw new PrismNotSupportedException("Explicit engine does not yet export state rewards for " + model.getModelType() + "s"); + } + } } diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index a1ec0227..da47dad8 100644 --- a/prism/src/prism/Model.java +++ b/prism/src/prism/Model.java @@ -184,8 +184,30 @@ public interface Model public void printTransInfo(PrismLog log); public void printTransInfo(PrismLog log, boolean extra); void exportToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException; + + /** + * Export (non-zero) state rewards for one reward structure of the model. + * @param r Index of reward structure to export (0-indexed) + * @param exportType The format in which to export + * @param file File to export to (if null, print to the log instead) + */ + void exportStateRewardsToFile(int r, int exportType, File file) throws FileNotFoundException, PrismException; + + @Deprecated String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException; + + /** + * Export (non-zero) transition rewards for one reward structure of the model. + * @param r Index of reward structure to export (0-indexed) + * @param exportType The format in which to export + * @param ordered Do the entries need to be printed in order? + * @param file File to export to (if null, print to the log instead) + */ + void exportTransRewardsToFile(int r, int exportType, boolean ordered, File file) throws FileNotFoundException, PrismException; + + @Deprecated String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException; + void exportStates(int exportType, PrismLog log); void clear(); diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index b50ada32..f3ac6d23 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -421,33 +421,22 @@ public class NondetModel extends ProbModel } } - // export state rewards vector to a file - - // returns string containing files used if there were more than 1, null otherwise - - public String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException + @Override + public void exportTransRewardsToFile(int r, int exportType, boolean ordered, File file) throws FileNotFoundException, PrismException { - if (numRewardStructs == 0) - throw new PrismException("There are no state rewards to export"); - int i; - String filename, allFilenames = ""; - for (i = 0; i < numRewardStructs; i++) { - filename = (file != null) ? file.getPath() : null; - if (filename != null && numRewardStructs > 1) { - filename = PrismUtils.addCounterSuffixToFilename(filename, i + 1); - allFilenames += ((i > 0) ? ", " : "") + filename; - } - PrismMTBDD.ExportVector(stateRewards[i], "c" + (i + 1), allDDRowVars, odd, exportType, filename); + if (!ordered) { + // can only do explicit (sparse matrix based) export for mdps + } else { + PrismSparse.ExportSubMDP(trans, transRewards[r], "C" + (r + 1), allDDRowVars, allDDColVars, allDDNondetVars, odd, exportType, (file == null) ? null : file.getPath()); } - return (allFilenames.length() > 0) ? allFilenames : null; } - // export transition rewards matrix to a file - - // returns string containing files used if there were more than 1, null otherwise - + @Deprecated public String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException { + // export transition rewards matrix to a file + // returns string containing files used if there were more than 1, null otherwise + if (numRewardStructs == 0) throw new PrismException("There are no transition rewards to export"); int i; diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index bc512e86..0b1557f9 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2317,7 +2317,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener } /** - * Export the currently loaded model's state rewards to a file + * Export the currently loaded model's state rewards to a file (or files, or stdout). + * If there is more than 1 reward structure, then multiple files are generated + * (e.g. "rew.sta" becomes "rew1.sta", "rew2.sta", ...) * @param exportType Type of export; one of: