From 52e3d712e7ecbf789240622e726dbb35de139ba3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 15 Oct 2010 17:08:27 +0000 Subject: [PATCH] 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 | 9 +++++++++ prism/src/sparse/PS_NondetReachReward.cc | 7 ++++++- prism/src/sparse/PS_NondetUntil.cc | 7 ++++++- 3 files changed, 21 insertions(+), 2 deletions(-) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 09656f52..e82bb5af 100644 --- a/prism/src/prism/PrismCL.java +++ b/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) { diff --git a/prism/src/sparse/PS_NondetReachReward.cc b/prism/src/sparse/PS_NondetReachReward.cc index e4aa9f95..12372b54 100644 --- a/prism/src/sparse/PS_NondetReachReward.cc +++ b/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"); } diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index 1c1b0576..986c4233 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/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"); }