Ability to export target state info (currently only at code level, not even from PRISM command-line).

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

prism/src/prism/NondetModelChecker.java

@@ -27,6 +27,7 @@
 
 package prism;
 
+import java.io.FileNotFoundException;
 import java.util.*;
 
 import jdd.*;
@@ -942,6 +943,18 @@ public class NondetModelChecker extends NonProbModelChecker
 		DoubleVector probsDV;
 		StateProbs probs = null;
 		
+		// If required, export info about target states 
+		if (prism.getExportTarget()) {
+			JDDNode labels[] = { model.getStart(), b2 };
+			String labelNames[] = { "init", "target" };
+			try {
+				mainLog.print("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"...");
+				PrismMTBDD.ExportLabels(labels, labelNames, "l", model.getAllDDRowVars(), model.getODD(), Prism.EXPORT_PLAIN, prism.getExportTargetFilename());
+			} catch (FileNotFoundException e) {
+				mainLog.println("\nWarning: Could not export target to file \"" + prism.getExportTargetFilename() + "\"");
+			}
+		}
+		
 		// compute yes/no/maybe states
 		if (b2.equals(JDD.ZERO)) {
 			yes = JDD.Constant(0);

prism/src/prism/Prism.java

@@ -96,6 +96,11 @@ public class Prism implements PrismSettingsListener
 	// Main PRISM settings
 	private PrismSettings settings;
 	
+	// Some additional settings (here because not available from main options panel in GUI) 
+	// Export target state info?
+	protected boolean exportTarget;
+	protected String exportTargetFilename;
+	
 	// A few miscellaneous options (i.e. defunct/hidden/undocumented/etc.)
 	// See constructor below for default values
 	
@@ -182,6 +187,8 @@ public class Prism implements PrismSettingsListener
 		settings.addSettingsListener(this);
 		
 		// default values for miscellaneous options 
+		exportTarget = false;
+		exportTargetFilename = null;
 		doReach = true;
 		bsccComp = true;
 		checkZeroLoops = false;
@@ -323,6 +330,16 @@ public class Prism implements PrismSettingsListener
 	
 	// set methods for miscellaneous options
 	
+	public void setExportTarget(boolean b) throws PrismException
+	{
+		exportTarget = b;
+	}
+	
+	public void setExportTargetFilename(String s) throws PrismException
+	{
+		exportTargetFilename = s;
+	}
+	
 	public void setDoReach(boolean b) throws PrismException
 	{
 		doReach = b;
@@ -427,6 +444,12 @@ public class Prism implements PrismSettingsListener
 	
 	// get methods for miscellaneous options
 	
+	public boolean getExportTarget()
+	{return exportTarget; }
+	
+	public String getExportTargetFilename()
+	{ return exportTargetFilename; }
+	
 	public boolean getDoReach()
 	{ return doReach; }
 	

prism/src/prism/ProbModelChecker.java

@@ -27,6 +27,7 @@
 package prism;
 
 import java.io.File;
+import java.io.FileNotFoundException;
 import java.util.Vector;
 
 import jdd.*;
@@ -1479,6 +1480,18 @@ public class ProbModelChecker extends NonProbModelChecker
 		DoubleVector probsDV;
 		StateProbs probs = null;
 
+		// If required, export info about target states 
+		if (prism.getExportTarget()) {
+			JDDNode labels[] = { model.getStart(), b2 };
+			String labelNames[] = { "init", "target" };
+			try {
+				mainLog.print("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"...");
+				PrismMTBDD.ExportLabels(labels, labelNames, "l", model.getAllDDRowVars(), model.getODD(), Prism.EXPORT_PLAIN, prism.getExportTargetFilename());
+			} catch (FileNotFoundException e) {
+				mainLog.println("\nWarning: Could not export target to file \"" + prism.getExportTargetFilename() + "\"");
+			}
+		}
+		
 		// compute yes/no/maybe states
 		if (b2.equals(JDD.ZERO)) {
 			yes = JDD.Constant(0);