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

@@ -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.
 	 */

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();
 

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();
 }

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();
 	}

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)