From 913f80a8e9ec291c95db1f592abee9d200eb1412 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 16 Jan 2015 15:18:22 +0000 Subject: [PATCH] Minor refactoring and alignment between PS_NondetMultiReach.cc and PS_NondetMultiReach1.cc. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9528 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/sparse/PS_NondetMultiReach.cc | 19 +++++------------ prism/src/sparse/PS_NondetMultiReach1.cc | 27 ++++++------------------ 2 files changed, 12 insertions(+), 34 deletions(-) diff --git a/prism/src/sparse/PS_NondetMultiReach.cc b/prism/src/sparse/PS_NondetMultiReach.cc index d00cc5e3..5c412d1c 100644 --- a/prism/src/sparse/PS_NondetMultiReach.cc +++ b/prism/src/sparse/PS_NondetMultiReach.cc @@ -63,12 +63,6 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti jdoubleArray _bounds, // target probability bounds jlong __jlongpointer m, // 'maybe' states jlong __jlongpointer _start // initial state(s) - //jlong __jlongpointer m_r, // 'maybe' states for the reward formula - //jlong __jlongpointer trr // transition rewards - // Reward paramters for more complicated cases - //jlongArray _rewards, // sets of rewards for reward formulas - //jlongArray _targets_r, // target state sets for reward formulas - //jdoubleArray _bounds_r, // target probability bounds for reward formulas ) { // cast function parameters @@ -80,7 +74,6 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti DdNode **ndvars = jlong_to_DdNode_array(ndv); // nondet vars DdNode *maybe = jlong_to_DdNode(m); // 'maybe' states DdNode *start = jlong_to_DdNode(_start); // initial state(s) - DdNode *trans_rewards = NULL; // transition rewards // target info jlong *target_ptrs = NULL; @@ -519,10 +512,10 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti 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); + 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 0) { @@ -550,8 +542,8 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti if (!lp_solved) lp_result = NAN; } - time_taken = time_for_setup + time_for_lp; // Print timing info + time_taken = time_for_setup + time_for_lp; PS_PrintToMainLog(env, "\nLP problem solved in %.2f seconds (setup %.2f, lpsolve %.2f)\n", time_taken, time_for_setup, time_for_lp); delete yes_vec; @@ -567,7 +559,6 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti if (lp) delete_lp(lp); if (a) Cudd_RecursiveDeref(ddman, a); if (maybe_yes) Cudd_RecursiveDeref(ddman, maybe_yes); - if (trans_rewards) Cudd_RecursiveDeref(ddman, trans_rewards); if (loops) Cudd_RecursiveDeref(ddman, loops); if (ndsm) delete ndsm; if (ndsm_r) delete ndsm_r; diff --git a/prism/src/sparse/PS_NondetMultiReach1.cc b/prism/src/sparse/PS_NondetMultiReach1.cc index 783510ad..30cc088f 100644 --- a/prism/src/sparse/PS_NondetMultiReach1.cc +++ b/prism/src/sparse/PS_NondetMultiReach1.cc @@ -65,12 +65,6 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti jdoubleArray _bounds, // target probability bounds jlong __jlongpointer m, // 'maybe' states jlong __jlongpointer _start // initial state(s) - //jlong __jlongpointer m_r, // 'maybe' states for the reward formula - //jlong __jlongpointer trr // transition rewards - // Reward paramters for more complicated cases - //jlongArray _rewards, // sets of rewards for reward formulas - //jlongArray _targets_r, // target state sets for reward formulas - //jdoubleArray _bounds_r, // target probability bounds for reward formulas ) { // cast function parameters @@ -82,7 +76,6 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti DdNode **ndvars = jlong_to_DdNode_array(ndv); // nondet vars DdNode *maybe = jlong_to_DdNode(m); // 'maybe' states DdNode *start = jlong_to_DdNode(_start); // initial state(s) - DdNode *trans_rewards = NULL; // transition rewards // target info jlong *target_ptrs = NULL; @@ -99,7 +92,6 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti // sparse matrix NDSparseMatrix *ndsm = NULL, *ndsm_r = NULL; // action info - int *actions; jstring *action_names_jstrings; const char** action_names = NULL; int num_actions; @@ -385,15 +377,11 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti } } - //int *constraints_ints[n]; - //double *constraints_reals[n]; int *constraints_sp; - //int constraints_sp[n]; int *constraints_ints; double *constraints_reals; unsigned long *constraints_int_ptr; unsigned long *constraints_real_ptr; - //PS_PrintToMainLog(env, "Allocating memory space \n"); constraints_sp = new int[n]; constraints_int_ptr = new unsigned long[n]; constraints_real_ptr = new unsigned long[n]; @@ -594,6 +582,13 @@ 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; iactions, 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); - } } // Modify result based on type @@ -643,7 +631,6 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti if (lp) delete_lp(lp); if (a) Cudd_RecursiveDeref(ddman, a); if (maybe_yes) Cudd_RecursiveDeref(ddman, maybe_yes); - if (trans_rewards) Cudd_RecursiveDeref(ddman, trans_rewards); if (loops) Cudd_RecursiveDeref(ddman, loops); if (ndsm) delete ndsm; if (ndsm_r) delete ndsm_r;