Browse Source

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
master
Dave Parker 11 years ago
parent
commit
1d09274252
  1. 9
      prism/src/sparse/PS_NondetMultiReachReward.cc
  2. 8
      prism/src/sparse/PS_NondetMultiReachReward1.cc

9
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]);

8
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]);

Loading…
Cancel
Save