From 1d092742529c1e8fb01497f81a5f2def603b8126 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 14 Jan 2015 21:31:40 +0000
Subject: [PATCH] Add adversary export to reward-based multi-objective model
 checking (sparse engine) - not sure why it was not there.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9524 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/sparse/PS_NondetMultiReachReward.cc  | 9 +++++++++
 prism/src/sparse/PS_NondetMultiReachReward1.cc | 8 ++++++++
 2 files changed, 17 insertions(+)

diff --git a/prism/src/sparse/PS_NondetMultiReachReward.cc b/prism/src/sparse/PS_NondetMultiReachReward.cc
index f2e4f039..35b97894 100644
--- a/prism/src/sparse/PS_NondetMultiReachReward.cc
+++ b/prism/src/sparse/PS_NondetMultiReachReward.cc
@@ -34,6 +34,7 @@
 #include <odd.h>
 #include <dv.h>
 #include "sparse.h"
+#include "sparse_adv.h"
 #include "prism.h"
 #include "PrismSparseGlob.h"
 #include "PrismNativeGlob.h"
@@ -641,6 +642,14 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti
       lp_result = get_objective(lp);
       lp_soln = new double[num_lp_vars];
       get_ptr_variables(lp, &lp_soln);
+      
+      // Generate adversary from the solution, if required
+	  if (export_adv != EXPORT_ADV_NONE) {
+          // Adversary generation
+			export_adversary_ltl_tra(export_adv_filename, ndsm, ndsm->actions, action_names, yes_vec, maybe_vec, num_lp_vars, map_var, lp_soln, start_index);
+			//export_adversary_ltl_dot(env, ndsm, n, nnz, yes_vec, maybe_vec, num_lp_vars, map_var, lp_soln, start_index);
+      }
+      
       /*for (i=0; i<num_lp_vars; i++) {
         if(lp_soln[i] != 0) {
           PS_PrintToMainLog(env, "X%d = %g    ", i, lp_soln[i]);
diff --git a/prism/src/sparse/PS_NondetMultiReachReward1.cc b/prism/src/sparse/PS_NondetMultiReachReward1.cc
index c7115288..9b282601 100644
--- a/prism/src/sparse/PS_NondetMultiReachReward1.cc
+++ b/prism/src/sparse/PS_NondetMultiReachReward1.cc
@@ -718,6 +718,14 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti
       lp_result = get_objective(lp);
       lp_soln = new double[num_lp_vars];
       get_ptr_variables(lp, &lp_soln);
+
+		// Generate adversary from the solution, if required
+		if (export_adv != EXPORT_ADV_NONE) {
+			// Adversary generation
+			export_adversary_ltl_tra(export_adv_filename, ndsm, ndsm->actions, action_names, yes_vec, maybe_vec, num_lp_vars, map_var, lp_soln, start_index);
+			//export_adversary_ltl_dot(env, ndsm, n, nnz, yes_vec, maybe_vec, num_lp_vars, map_var, lp_soln, start_index);
+		}
+		
       /*for (i=0; i<num_lp_vars; i++) {
         if(lp_soln[i] != 0) {
           PS_PrintToMainLog(env, "X%d = %g    ", i, lp_soln[i]);