From 2f0c968ff5f256cf38cc5f9ea39188f2fe7327a9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 10 Feb 2012 18:47:38 +0000 Subject: [PATCH] Push "export states" functionality into models (symbolic/explicit), use from Prism. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4585 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/Model.java | 6 ++++ prism/src/explicit/ModelExplicit.java | 36 ++++++++++++++++++++ prism/src/prism/Model.java | 1 + prism/src/prism/Prism.java | 47 +++++---------------------- prism/src/prism/ProbModel.java | 28 ++++++++++++++++ 5 files changed, 80 insertions(+), 38 deletions(-) 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)