Add -exportpropaut option (hidden) to export DRA(s) in textual form.

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

prism/src/explicit/DTMCModelChecker.java

@@ -38,6 +38,8 @@ import prism.DRA;
 import prism.Pair;
 import prism.PrismComponent;
 import prism.PrismException;
+import prism.PrismFileLog;
+import prism.PrismLog;
 import prism.PrismUtils;
 import explicit.rewards.MCRewards;
 
@@ -84,10 +86,17 @@ public class DTMCModelChecker extends ProbModelChecker
 		time = System.currentTimeMillis();
 		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
 		int draSize = dra.size();
-		mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
-		// dra.print(System.out);
+		mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
 		time = System.currentTimeMillis() - time;
-		mainLog.println("\nTime for Rabin translation: " + time / 1000.0 + " seconds.");
+		mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
+		// If required, export DRA 
+		if (settings.getExportPropAut()) {
+			mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"...");
+			PrismLog out = new PrismFileLog(settings.getExportPropAutFilename());
+			out.println(dra);
+			out.close();
+			//dra.printDot(new java.io.PrintStream("dra.dot"));
+		}
 
 		// Build product of Markov chain and automaton
 		mainLog.println("\nConstructing MC-DRA product...");

prism/src/explicit/MDPModelChecker.java

@@ -94,10 +94,17 @@ public class MDPModelChecker extends ProbModelChecker
 		time = System.currentTimeMillis();
 		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
 		int draSize = dra.size();
-		mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
-		// dra.print(System.out);
+		mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
 		time = System.currentTimeMillis() - time;
-		mainLog.println("\nTime for Rabin translation: " + time / 1000.0 + " seconds.");
+		mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
+		// If required, export DRA 
+		if (settings.getExportPropAut()) {
+			mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"...");
+			PrismLog out = new PrismFileLog(settings.getExportPropAutFilename());
+			out.println(dra);
+			out.close();
+			//dra.printDot(new java.io.PrintStream("dra.dot"));
+		}
 
 		// Build product of MDP and automaton
 		mainLog.println("\nConstructing MDP-DRA product...");

prism/src/prism/NondetModelChecker.java

@@ -673,10 +673,18 @@ public class NondetModelChecker extends NonProbModelChecker
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		long l = System.currentTimeMillis();
 		dra[i] = LTLModelChecker.convertLTLFormulaToDRA(ltl);
-		mainLog.print("\nDRA has " + dra[i].size() + " states, " + ", " + dra[i].getNumAcceptancePairs() + " pairs.");
-		//dra[i].print(System.out);
+		mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getNumAcceptancePairs() + " pairs.");
 		l = System.currentTimeMillis() - l;
-		mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds.");
+		mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");
+		// If required, export DRA 
+		if (prism.getSettings().getExportPropAut()) {
+			String exportPropAutFilename = PrismUtils.addCounterSuffixToFilename(prism.getSettings().getExportPropAutFilename(), i);
+			mainLog.println("Exporting DRA to file \"" + exportPropAutFilename + "\"...");
+			PrismLog out = new PrismFileLog(exportPropAutFilename);
+			out.println(dra);
+			out.close();
+			//dra.printDot(new java.io.PrintStream("dra.dot"));
+		}
 
 		// Build product of MDP and automaton
 		mainLog.println("\nConstructing MDP-DRA product...");
@@ -1469,13 +1477,17 @@ public class NondetModelChecker extends NonProbModelChecker
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		l = System.currentTimeMillis();
 		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
-		mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
-		/*try {
-			mainLog.print(dra);
-			dra.printDot(new java.io.PrintStream("dra.dot"));
-		} catch(Exception e) {}*/
+		mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
 		l = System.currentTimeMillis() - l;
-		mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds.");
+		mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");
+		// If required, export DRA 
+		if (prism.getSettings().getExportPropAut()) {
+			mainLog.println("Exporting DRA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"...");
+			PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename());
+			out.println(dra);
+			out.close();
+			//dra.printDot(new java.io.PrintStream("dra.dot"));
+		}
 
 		// Build product of MDP and automaton
 		mainLog.println("\nConstructing MDP-DRA product...");

prism/src/prism/PrismCL.java

@@ -31,7 +31,6 @@ import java.io.FileNotFoundException;
 import java.util.ArrayList;
 import java.util.List;
 
-import param.ParamModelChecker;
 import parser.Values;
 import parser.ast.Expression;
 import parser.ast.ExpressionReward;

prism/src/prism/PrismSettings.java

@@ -803,7 +803,33 @@ public class PrismSettings implements Observer
 		
 		notifySettingsListeners();
 	}
+
+	// HIDDEN OPTIONS
+	
+	// Export property automaton info?
+	protected boolean exportPropAut = false;
+	protected String exportPropAutFilename = null;
 	
+	public void setExportPropAut(boolean b) throws PrismException
+	{
+		exportPropAut = b;
+	}
+
+	public void setExportPropAutFilename(String s) throws PrismException
+	{
+		exportPropAutFilename = s;
+	}
+
+	public boolean getExportPropAut()
+	{
+		return exportPropAut;
+	}
+
+	public String getExportPropAutFilename()
+	{
+		return exportPropAutFilename;
+	}
+
 	/**
 	 * Set an option by parsing one or more command-line arguments.
 	 * Reads the ith argument (assumed to be in the form "-switch")
@@ -1403,6 +1429,18 @@ public class PrismSettings implements Observer
 			}
 		}
 
+		// HIDDEN OPTIONS
+		
+		// export property automaton to file (hidden option)
+		else if (sw.equals("exportpropaut")) {
+			if (i < args.length - 1) {
+				setExportPropAut(true);
+				setExportPropAutFilename(args[++i]);
+			} else {
+				throw new PrismException("No file specified for -" + sw + " switch");
+			}
+		}
+		
 		// unknown switch - error
 		else {
 			throw new PrismException("Invalid switch -" + sw + " (type \"prism -help\" for full list)");

prism/src/prism/ProbModelChecker.java

@@ -579,10 +579,17 @@ public class ProbModelChecker extends NonProbModelChecker
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		l = System.currentTimeMillis();
 		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
-		mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
-		// dra.print(System.out);
+		mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
 		l = System.currentTimeMillis() - l;
-		mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds.");
+		mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");
+		// If required, export DRA 
+		if (prism.getExportPropAut()) {
+			mainLog.println("Exporting DRA to file \"" + prism.getExportPropAutFilename() + "\"...");
+			PrismLog out = new PrismFileLog(prism.getExportPropAutFilename());
+			out.println(dra);
+			out.close();
+			//dra.printDot(new java.io.PrintStream("dra.dot"));
+		}
 
 		// Build product of Markov chain and automaton
 		// (note: might be a CTMC - StochModelChecker extends this class)