Added -exportadvmdp switch.

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

prism/src/prism/PrismCL.java

@@ -1028,6 +1028,15 @@ public class PrismCL
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
+				// export adversary to file, as an mdp
+				else if (sw.equals("exportadvmdp")) {
+					if (i < args.length - 1) {
+						prism.setExportAdv(Prism.EXPORT_ADV_MDP);
+						prism.setExportAdvFilename(args[++i]);
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
 				// export reachability target info to file
 				else if (sw.equals("exporttarget")) {
 					if (i < args.length - 1) {

prism/src/sparse/PS_NondetReachReward.cc

@@ -369,7 +369,12 @@ jboolean min				// min or max probabilities (true = min, false = max)
 				// But only output a choice if it is in the adversary
 				if (j == adv[i]) {
 					for (k = l2; k < h2; k++) {
-						fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]);
+						switch (export_adv_enabled) {
+						case EXPORT_ADV_DTMC:
+							fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]); break;
+						case EXPORT_ADV_MDP:
+							fprintf(fp_adv, "%d 0 %d %g", i, cols[k], non_zeros[k]); break;
+						}
 						if (actions != NULL) fprintf(fp_adv, " %s", actions[j]>0?action_names[actions[j]-1]:"");
 						fprintf(fp_adv, "\n");
 					}

prism/src/sparse/PS_NondetUntil.cc

@@ -319,7 +319,12 @@ jboolean min				// min or max probabilities (true = min, false = max)
 				// But only output a choice if it is in the adversary
 				if (j == adv[i]) {
 					for (k = l2; k < h2; k++) {
-						fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]);
+						switch (export_adv_enabled) {
+						case EXPORT_ADV_DTMC:
+							fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]); break;
+						case EXPORT_ADV_MDP:
+							fprintf(fp_adv, "%d 0 %d %g", i, cols[k], non_zeros[k]); break;
+						}
 						if (actions != NULL) fprintf(fp_adv, " %s", actions[j]>0?action_names[actions[j]-1]:"");
 						fprintf(fp_adv, "\n");
 					}