diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index a1a5cd50..79d815c6 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -31,6 +31,7 @@ import java.util.*; import parser.State; import parser.Values; +import parser.VarList; import prism.ModelType; import prism.PrismException; import prism.PrismLog; @@ -179,6 +180,11 @@ public interface Model */ public void exportToPrismLanguage(String filename) throws PrismException; + /** + * Export states list. + */ + public void exportStates(int exportType, VarList varList, PrismLog log) throws PrismException; + /** * Report info/stats about the model as a string. */ diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index 12c18f8f..0e7320e5 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -31,7 +31,9 @@ import java.util.*; import parser.State; import parser.Values; +import parser.VarList; import prism.ModelType; +import prism.Prism; import prism.PrismException; import prism.PrismLog; import prism.PrismFileLog; @@ -251,6 +253,40 @@ public abstract class ModelExplicit implements Model @Override public abstract void exportToPrismLanguage(String filename) throws PrismException; + @Override + public void exportStates(int exportType, VarList varList, PrismLog log) throws PrismException + { + if (statesList == null) + return; + + // Print header: list of model vars + if (exportType == Prism.EXPORT_MATLAB) + log.print("% "); + log.print("("); + int numVars = varList.getNumVars(); + for (int i = 0; i < numVars; i++) { + log.print(varList.getName(i)); + if (i < numVars - 1) + log.print(","); + } + log.println(")"); + if (exportType == Prism.EXPORT_MATLAB) + log.println("states=["); + + // Print states + int numStates = statesList.size(); + for (int i = 0; i < numStates; i++) { + if (exportType != Prism.EXPORT_MATLAB) + log.println(i + ":" + statesList.get(i).toString()); + else + log.println(statesList.get(i).toStringNoParentheses()); + } + + // Print footer + if (exportType == Prism.EXPORT_MATLAB) + log.println("];"); + } + @Override public abstract String infoString(); diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index 415f2cf1..4dbfee8a 100644 --- a/prism/src/prism/Model.java +++ b/prism/src/prism/Model.java @@ -135,6 +135,7 @@ public interface Model void exportToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException; String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException; String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException; + void exportStates(int exportType, PrismLog log) throws PrismException; void clear(); } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 5be174ce..d56979d9 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2179,61 +2179,32 @@ public class Prism implements PrismSettingsListener int i; PrismLog tmpLog; - // no specific states format for MRMC + // No specific states format for MRMC if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; - // rows format does not apply to states output + // Rows format does not apply to states output if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; // Build model, if necessary buildModelIfRequired(); - // print message + // Print message mainLog.print("\nExporting list of reachable states "); mainLog.print(getStringForExportType(exportType) + " "); mainLog.println(getDestinationStringForFile(file)); - // create new file log or use main log + // Create new file log or use main log tmpLog = getPrismLogForFile(file); - // print header: list of model vars - if (exportType == EXPORT_MATLAB) - tmpLog.print("% "); - tmpLog.print("("); - for (i = 0; i < currentModulesFile.getNumVars(); i++) { - tmpLog.print(currentModulesFile.getVarName(i)); - if (i < currentModulesFile.getNumVars() - 1) - tmpLog.print(","); - } - tmpLog.println(")"); - if (exportType == EXPORT_MATLAB) - tmpLog.println("states=["); - - // print states + // Export if (!getExplicit()) { - if (exportType != EXPORT_MATLAB) - currentModel.getReachableStates().print(tmpLog); - else - currentModel.getReachableStates().printMatlab(tmpLog); + currentModel.exportStates(exportType, tmpLog); } else { - explicit.StateValues statesList = null; - try { - statesList = new explicit.StateValues(TypeBool.getInstance(), new Boolean(true), currentModelExpl); - } catch (PrismLangException e) { - // Can't go wrong - type always fine - } - if (exportType != Prism.EXPORT_MATLAB) - statesList.print(tmpLog); - else - statesList.print(tmpLog, true, true, true, true); + currentModelExpl.exportStates(exportType, currentModulesFile.createVarList(), tmpLog); } - - // print footer - if (exportType == EXPORT_MATLAB) - tmpLog.println("];"); - - // tidy up + + // Tidy up if (file != null) tmpLog.close(); } diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index e1f78569..a3540eb4 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -759,6 +759,34 @@ public class ProbModel implements Model return (allFilenames.length() > 0) ? allFilenames : null; } + @Override + public void exportStates(int exportType, PrismLog log) throws PrismException + { + // Print header: list of model vars + if (exportType == Prism.EXPORT_MATLAB) + log.print("% "); + log.print("("); + int numVars = getNumVars(); + for (int i = 0; i < numVars; i++) { + log.print(getVarName(i)); + if (i < numVars - 1) + log.print(","); + } + log.println(")"); + if (exportType == Prism.EXPORT_MATLAB) + log.println("states=["); + + // Print states + if (exportType != Prism.EXPORT_MATLAB) + getReachableStates().print(log); + else + getReachableStates().printMatlab(log); + + // Print footer + if (exportType == Prism.EXPORT_MATLAB) + log.println("];"); + } + // convert global state index to local indices public String globalToLocal(long x)