s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Dave Parker 11 years ago
parent
9589a14c14
commit
913f80a8e9
2 changed files with 12 additions and 34 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 19
      prism/src/sparse/PS_NondetMultiReach.cc
  2. 27
      prism/src/sparse/PS_NondetMultiReach1.cc

19
prism/src/sparse/PS_NondetMultiReach.cc
View File

@ -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<num_lp_vars; i++) {
if(lp_soln[i] != 0) {
@ -537,7 +530,6 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti
if(count)
PS_PrintToMainLog(env, "\n");*/
}
// Modify result based on type
if (relops[0] > 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;

27
prism/src/sparse/PS_NondetMultiReach1.cc
View File

@ -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; i<num_lp_vars; i++) {
if(lp_soln[i] != 0) {
PS_PrintToMainLog(env, "X%d = %g ", i, lp_soln[i]);
@ -606,13 +601,6 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti
}
if(count)
PS_PrintToMainLog(env, "\n");*/
// 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);
}
}
// 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;

Write Preview
Loading…
Cancel
Save