From 4e09eb136f494bf74e319fabd6bb94a6a260463c Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sat, 28 Jan 2012 23:39:50 +0000
Subject: [PATCH] Added options to -exportresults switch for csv/matrix result
 export mode, and removed temporary switches -exportresultsmatrix,
 -exportresultscsv, etc.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4510 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/CHANGELOG.txt          | 15 +++++++----
 prism/src/prism/PrismCL.java | 49 +++++++++++-------------------------
 2 files changed, 25 insertions(+), 39 deletions(-)

diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt
index 130891a4..fe1bf693 100644
--- a/prism/CHANGELOG.txt
+++ b/prism/CHANGELOG.txt
@@ -7,17 +7,22 @@ Latest changes (mostly reverse chronological):
 
 Changes:
 
+* Property names
+  - properties can be named, by prefixing with "name":
+  - properties can appear as sub-formulae of other properties using name references
+  - command-line -prop switch allows selection of property to check by name
 * Added -pf as a command-line switch alias for -pctl/-csl
 * Add .props as a properties file extension (in GUI)
+
 * Export of results in matrix form, e.g. for surface plots (-exportresultsmatrix)
 * And export of results in CSV format (-exportresultscsv and -exportresultsmatrixcsv)
-* Can disable Prob0/Prob1 precomputation algorithms independently (-noprob0, -noprob1)
-* Bash completion scripts + additional syntax highlighters
-* Added PrismTest class to illustrate programmatic use of PRISM
-* GUI on Macs uses Cmd, not Ctrl
+
+* New switches -noprob0/-noprob1 to disable individual precomputation algorithms
 * Added prominence given to log warning messages in command-line/GUI
+* GUI on Macs uses Cmd, not Ctrl
+* Added PrismTest class to illustrate programmatic use of PRISM
 * Command-line scripts can signal termination via growlnotify/notify-send 
-* Properties can be named, by prefixing with "name":, and reference each other
+* Bash completion scripts + additional syntax highlighters
 
 Ongoing changes:
 
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index d3accd48..cea7b312 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -1088,7 +1088,7 @@ public class PrismCL
 	 */
 	private void parseArguments(String[] args) throws PrismException
 	{
-		int i,  j;
+		int i, j;
 		double d;
 		String sw, s;
 		PrismLog log;
@@ -1265,39 +1265,20 @@ public class PrismCL
 				else if (sw.equals("exportresults")) {
 					if (i < args.length - 1) {
 						exportresults = true;
-						exportResultsFilename = args[++i];
-					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
-					}
-				}
-				else if (sw.equals("exportresultscsv")) {
-					if (i < args.length - 1) {
-						exportresults = true;
-						exportresultscsv = true;
-						exportResultsFilename = args[++i];
-					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
-					}
-				}
-				// export results, in matrix form
-				else if (sw.equals("exportresultsmatrix")) {
-					if (i < args.length - 1) {
-						exportresults = true;
-						exportresultsmatrix = true;
-						exportResultsFilename = args[++i];
-					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
-					}
-				}
-				// export results, in matrix form
-				else if (sw.equals("exportresultsmatrixcsv")) {
-					if (i < args.length - 1) {
-						exportresults = true;
-						exportresultsmatrix = true;
-						exportresultscsv = true;
-						exportResultsFilename = args[++i];
+						// Parse filename/options
+						s = args[++i];
+						String ss[] = s.split(",");
+						exportResultsFilename = ss[0];
+						for (j = 1; j < ss.length; j++) {
+							if (ss[j].equals("csv"))
+								exportresultscsv = true;
+							else if (ss[j].equals("matrix"))
+								exportresultsmatrix = true;
+							else
+								errorAndExit("Unknown option \"" + ss[j] + "\" for -" + sw + " switch");
+						}
 					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
+						errorAndExit("No file/options specified for -" + sw + " switch");
 					}
 				}
 				// export transition matrix to file
@@ -1959,7 +1940,7 @@ public class PrismCL
 		mainLog.println("-mdp ........................... Force imported/built model to be an MDP");
 		mainLog.println();
 		mainLog.println("EXPORT OPTIONS:");
-		mainLog.println("-exportresults <file> .......... Export the results of model checking to a file");
+		mainLog.println("-exportresults <file[,options]>  Export the results of model checking to a file");
 		mainLog.println("-exporttrans <file> ............ Export the transition matrix to a file");
 		mainLog.println("-exportstaterewards <file> ..... Export the state rewards vector to a file");
 		mainLog.println("-exporttransrewards <file> ..... Export the transition rewards matrix to a file");