Added -exportmecs switch.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7048 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/Prism.java

@@ -1002,6 +1002,22 @@ public class Prism implements PrismSettingsListener
 		return sccComputer;
 	}
 
+	/**
+	 * Get an ECComputer object.
+	 */
+	public ECComputer getECComputer(NondetModel model)
+	{
+		return getECComputer(model.getReach(), model.getTrans(), model.getTrans01(), model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars());
+	}
+
+	/**
+	 * Get an ECComputer object.
+	 */
+	public ECComputer getECComputer(JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars allDDNondetVars)
+	{
+		return new ECComputerDefault(this, reach, trans, trans01, allDDRowVars, allDDColVars, allDDNondetVars);
+	}
+
 	//------------------------------------------------------------------------------
 	// Utility methods
 	//------------------------------------------------------------------------------
@@ -2296,6 +2312,88 @@ public class Prism implements PrismSettingsListener
 			tmpLog.close();
 	}
 
+	/**
+	 * Export the (states of the) currently loaded model's maximal end components (MECs) to a file
+	 * @param exportType Type of export; one of: <ul>
+	 * <li> {@link #EXPORT_PLAIN} 
+	 * <li> {@link #EXPORT_MATLAB}
+	 * </ul>
+	 * @param file File to export to (if null, print to the log instead)
+	 */
+	public void exportMECsToFile(int exportType, File file) throws FileNotFoundException, PrismException
+	{
+		int i, n;
+		long l; // timer
+		PrismLog tmpLog;
+		ECComputer ecComputer;
+		Vector<JDDNode> mecs;
+		JDDNode mec;
+
+		if (getExplicit())
+			throw new PrismException("Export of MECs not yet supported by explicit engine");
+
+		// no specific states format for MRMC
+		if (exportType == EXPORT_MRMC)
+			exportType = EXPORT_PLAIN;
+		// rows format does not apply to states output
+		if (exportType == EXPORT_ROWS)
+			exportType = EXPORT_PLAIN;
+
+		// Build model, if necessary
+		buildModelIfRequired();
+
+		// Compute MECs
+		mainLog.println("\nComputing MECs...");
+		ecComputer = getECComputer((NondetModel) currentModel);
+		l = System.currentTimeMillis();
+		ecComputer.computeECs();
+		l = System.currentTimeMillis() - l;
+		mecs = ecComputer.getVectECs();
+		mainLog.println("\nTime for MEC computation: " + l / 1000.0 + " seconds.");
+
+		// print message
+		mainLog.print("\nExporting MECs ");
+		mainLog.print(getStringForExportType(exportType) + " ");
+		mainLog.println(getDestinationStringForFile(file));
+
+		// 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("Variables: (");
+		for (i = 0; i < currentModel.getNumVars(); i++) {
+			tmpLog.print(currentModel.getVarName(i));
+			if (i < currentModel.getNumVars() - 1)
+				tmpLog.print(",");
+		}
+		tmpLog.println(")");
+
+		// print states for each mec
+		n = mecs.size();
+		for (i = 0; i < n; i++) {
+			tmpLog.println();
+			if (exportType == EXPORT_MATLAB)
+				tmpLog.print("% ");
+			tmpLog.println("MEC " + (i + 1) + "/" + n + ":");
+			if (exportType == EXPORT_MATLAB)
+				tmpLog.println("mec" + (i + 1) + "=[");
+			mec = mecs.get(i);
+			if (exportType != EXPORT_MATLAB)
+				new StateListMTBDD(mec, currentModel).print(tmpLog);
+			else
+				new StateListMTBDD(mec, currentModel).printMatlab(tmpLog);
+			if (exportType == EXPORT_MATLAB)
+				tmpLog.println("];");
+			JDD.Deref(mec);
+		}
+
+		// tidy up
+		if (file != null)
+			tmpLog.close();
+	}
+
 	/**
 	 * Export the states satisfying labels from the currently loaded model and a properties file to a file.
 	 * The PropertiesFile should correspond to the currently loaded model. 

prism/src/prism/PrismCL.java

@@ -74,6 +74,7 @@ public class PrismCL implements PrismModelListener
 	private boolean exporttransdot = false;
 	private boolean exporttransdotstates = false;
 	private boolean exportbsccs = false;
+	private boolean exportmecs = false;
 	private boolean exportresults = false;
 	private boolean exportresultsmatrix = false;
 	private boolean exportresultscsv = false;
@@ -128,6 +129,7 @@ public class PrismCL implements PrismModelListener
 	private String exportTransDotFilename = null;
 	private String exportTransDotStatesFilename = null;
 	private String exportBSCCsFilename = null;
+	private String exportMECsFilename = null;
 	private String exportResultsFilename = null;
 	private String exportSteadyStateFilename = null;
 	private String exportTransientFilename = null;
@@ -771,6 +773,20 @@ public class PrismCL implements PrismModelListener
 				error(e.getMessage());
 			}
 		}
+
+		// export MECs to a file
+		if (exportmecs) {
+			try {
+				File f = (exportMECsFilename.equals("stdout")) ? null : new File(exportMECsFilename);
+				prism.exportMECsToFile(exportType, f);
+			}
+			// in case of error, report it and proceed
+			catch (FileNotFoundException e) {
+				error("Couldn't open file \"" + exportMECsFilename + "\" for output");
+			} catch (PrismException e) {
+				error(e.getMessage());
+			}
+		}
 	}
 
 	/**
@@ -1234,6 +1250,15 @@ public class PrismCL implements PrismModelListener
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
+				// export mecs to file
+				else if (sw.equals("exportmecs")) {
+					if (i < args.length - 1) {
+						exportmecs = true;
+						exportMECsFilename = args[++i];
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
 				// export steady-state probs (as opposed to displaying on screen) 
 				else if (sw.equals("exportsteadystate") || sw.equals("exportss")) {
 					if (i < args.length - 1) {