diff --git a/prism/src/hybrid/PH_JOR.cc b/prism/src/hybrid/PH_JOR.cc index 7a9e221d..69015339 100644 --- a/prism/src/hybrid/PH_JOR.cc +++ b/prism/src/hybrid/PH_JOR.cc @@ -81,10 +81,9 @@ jdouble omega // omega (over-relaxation parameter) DdNode *init = jlong_to_DdNode(_init); // init soln // mtbdds - DdNode *reach, *diags, *id, *tmp; + DdNode *reach, *diags, *id; // model stats int n; - long nnz; // flags bool compact_d, compact_b; // matrix mtbdd @@ -97,8 +96,8 @@ jdouble omega // omega (over-relaxation parameter) long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int i, j, l, h, iters; - double d, kb, kbt; + int i, iters; + double kb, kbt; bool done; // start clocks diff --git a/prism/src/hybrid/PH_NondetBoundedUntil.cc b/prism/src/hybrid/PH_NondetBoundedUntil.cc index b840ac65..3508b232 100644 --- a/prism/src/hybrid/PH_NondetBoundedUntil.cc +++ b/prism/src/hybrid/PH_NondetBoundedUntil.cc @@ -97,8 +97,8 @@ jboolean min // min or max probabilities (true = min, false = max) long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int i, j, k, iters; - double d, kb, kbt; + int i, j, iters; + double kb, kbt; // start clocks start1 = start2 = util_cpu_time(); diff --git a/prism/src/hybrid/PH_NondetUntil.cc b/prism/src/hybrid/PH_NondetUntil.cc index 01b672f6..dabdaa57 100644 --- a/prism/src/hybrid/PH_NondetUntil.cc +++ b/prism/src/hybrid/PH_NondetUntil.cc @@ -96,8 +96,8 @@ jboolean min // min or max probabilities (true = min, false = max) long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int i, j, k, iters; - double d, kb, kbt; + int i, j, iters; + double kb, kbt; bool done; // start clocks diff --git a/prism/src/hybrid/PH_PSOR.cc b/prism/src/hybrid/PH_PSOR.cc index 9e18ad91..30e0aa26 100644 --- a/prism/src/hybrid/PH_PSOR.cc +++ b/prism/src/hybrid/PH_PSOR.cc @@ -83,10 +83,9 @@ jboolean forwards // forwards or backwards? DdNode *init = jlong_to_DdNode(_init); // init soln // mtbdds - DdNode *reach, *diags, *id, *tmp; + DdNode *reach, *diags, *id; // model stats int n; - long nnz; // flags bool compact_d, compact_b; // matrix mtbdd @@ -99,8 +98,8 @@ jboolean forwards // forwards or backwards? long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int i, j, fb, l, h, i2, j2, fb2, l2, h2, iters; - double d, x, sup_norm, kb, kbt; + int i, j, fb, l, h, i2, h2, iters; + double x, sup_norm, kb, kbt; bool done; // start clocks diff --git a/prism/src/hybrid/PH_Power.cc b/prism/src/hybrid/PH_Power.cc index 0e4690ca..1e33cf93 100644 --- a/prism/src/hybrid/PH_Power.cc +++ b/prism/src/hybrid/PH_Power.cc @@ -81,7 +81,6 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?) DdNode *init = jlong_to_DdNode(_init); // init soln // model stats int n; - long nnz; // flags bool compact_b; // matrix mtbdd @@ -94,8 +93,8 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?) long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int i, j, l, h, iters; - double d, kb, kbt; + int i, iters; + double kb, kbt; bool done; // start clocks diff --git a/prism/src/hybrid/PH_ProbBoundedUntil.cc b/prism/src/hybrid/PH_ProbBoundedUntil.cc index eccfd5ce..caedffbb 100644 --- a/prism/src/hybrid/PH_ProbBoundedUntil.cc +++ b/prism/src/hybrid/PH_ProbBoundedUntil.cc @@ -80,7 +80,6 @@ jint bound // time bound DdNode *a; // model stats int n; - long nnz; // flags bool compact_y; // matrix mtbdd @@ -93,7 +92,7 @@ jint bound // time bound long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int i, j, iters; + int i, iters; double kb, kbt; // start clocks diff --git a/prism/src/hybrid/PH_ProbCumulReward.cc b/prism/src/hybrid/PH_ProbCumulReward.cc index cf306ea8..1113a021 100644 --- a/prism/src/hybrid/PH_ProbCumulReward.cc +++ b/prism/src/hybrid/PH_ProbCumulReward.cc @@ -80,7 +80,6 @@ jint bound // time bound DdNode *all_rewards; // model stats int n; - long nnz; // flags bool compact_r; // matrix mtbdd @@ -93,7 +92,7 @@ jint bound // time bound long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int i, j, iters; + int i, iters; double kb, kbt; // start clocks diff --git a/prism/src/hybrid/PH_ProbInstReward.cc b/prism/src/hybrid/PH_ProbInstReward.cc index ce16f648..f473b2cc 100644 --- a/prism/src/hybrid/PH_ProbInstReward.cc +++ b/prism/src/hybrid/PH_ProbInstReward.cc @@ -74,11 +74,8 @@ jint bound // time bound DdNode **rvars = jlong_to_DdNode_array(rv); // row vars DdNode **cvars = jlong_to_DdNode_array(cv); // col vars - // mtbdds - DdNode *tmp; // model stats int n; - long nnz; // matrix mtbdd HDDMatrix *hddm; HDDNode *hdd; @@ -88,7 +85,7 @@ jint bound // time bound long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int i, j, iters; + int i, iters; double kb, kbt; // start clocks diff --git a/prism/src/hybrid/PH_ProbUntil.cc b/prism/src/hybrid/PH_ProbUntil.cc index 4158f67f..de33ea88 100644 --- a/prism/src/hybrid/PH_ProbUntil.cc +++ b/prism/src/hybrid/PH_ProbUntil.cc @@ -62,7 +62,7 @@ jlong __pointer m // 'maybe' states DdNode *maybe = jlong_to_DdNode(m); // 'maybe' states // mtbdds - DdNode *reach, *transr, *a, *b, *tmp; + DdNode *reach, *a, *b, *tmp; // vectors double *soln; diff --git a/prism/src/hybrid/PH_SOR.cc b/prism/src/hybrid/PH_SOR.cc index dd96c4a3..a137ae13 100644 --- a/prism/src/hybrid/PH_SOR.cc +++ b/prism/src/hybrid/PH_SOR.cc @@ -90,10 +90,9 @@ jboolean fwds // forwards or backwards? forwards = fwds; // mtbdds - DdNode *reach, *diags, *id, *tmp; + DdNode *reach, *diags, *id; // model stats int n; - long nnz; // flags bool compact_b, l_b_max; // matrix mtbdd @@ -106,8 +105,8 @@ jboolean fwds // forwards or backwards? long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int i, j, fb, l, h, i2, j2, fb2, l2, h2, iters; - double d, kb, kbt; + int i, j, fb, l, h, i2, h2, iters; + double kb, kbt; bool done, diag_done; // start clocks diff --git a/prism/src/hybrid/PH_StochBoundedUntil.cc b/prism/src/hybrid/PH_StochBoundedUntil.cc index 54de69c4..1a2fc8f2 100644 --- a/prism/src/hybrid/PH_StochBoundedUntil.cc +++ b/prism/src/hybrid/PH_StochBoundedUntil.cc @@ -98,7 +98,7 @@ jlong __pointer mu // probs for multiplying double time_taken, time_for_setup, time_for_iters; // misc bool done; - int i, j, iters, num_iters; + int i, iters, num_iters; double x, kb, kbt, max_diag, weight, term_crit_param_unif; // start clocks diff --git a/prism/src/hybrid/PH_StochCumulReward.cc b/prism/src/hybrid/PH_StochCumulReward.cc index bfc62b06..d7cbb576 100644 --- a/prism/src/hybrid/PH_StochCumulReward.cc +++ b/prism/src/hybrid/PH_StochCumulReward.cc @@ -97,8 +97,8 @@ jdouble time // time bound double time_taken, time_for_setup, time_for_iters; // misc bool done; - int i, j, l, h, iters, num_iters; - double d, max_diag, weight, kb, kbt, term_crit_param_unif; + int i, iters, num_iters; + double max_diag, weight, kb, kbt, term_crit_param_unif; // start clocks start1 = start2 = util_cpu_time(); diff --git a/prism/src/hybrid/PH_StochTransient.cc b/prism/src/hybrid/PH_StochTransient.cc index 3a101c7a..631a9b4e 100644 --- a/prism/src/hybrid/PH_StochTransient.cc +++ b/prism/src/hybrid/PH_StochTransient.cc @@ -93,7 +93,7 @@ jdouble time // time bound double time_taken, time_for_setup, time_for_iters; // misc bool done; - int i, j, iters, num_iters; + int i, iters, num_iters; double kb, kbt, max_diag, weight, term_crit_param_unif; // start clocks diff --git a/prism/src/hybrid/hybrid.cc b/prism/src/hybrid/hybrid.cc index c29730e3..3e5aef36 100644 --- a/prism/src/hybrid/hybrid.cc +++ b/prism/src/hybrid/hybrid.cc @@ -81,7 +81,7 @@ HDDMatrix *build_hdd_matrix(DdNode *matrix, DdNode **rvars, DdNode **cvars, int HDDMatrix *build_hdd_matrix(DdNode *matrix, DdNode **rvars, DdNode **cvars, int num_vars, ODDNode *odd, bool row_major, bool transpose) { - int i, j, n; + int i, j; HDDMatrix *res; HDDNode *ptr; @@ -308,9 +308,7 @@ void split_hdd_matrix(HDDMatrix *hm, bool compact_b, bool meet) void split_hdd_matrix(HDDMatrix *hm, bool compact_b, bool meet, bool transpose) { - int i, n, nnz, max; - double mem_est; - bool mem_out; + int i, n, max; HDDBlocks *blocks; // store some info globally @@ -567,7 +565,6 @@ void add_sparse_matrices(HDDMatrix *hm, bool compact_sm, bool diags_meet, bool t unsigned char *b_counts = hddm->blocks->counts; int *b_starts = (int *)hddm->blocks->counts; bool b_use_counts = hddm->blocks->use_counts; - int *b_offsets = hddm->blocks->offsets; HDDNode **b_nodes = hddm->row_tables[hddm->l_b]; int b_dist_shift = hddm->blocks->dist_shift; int b_dist_mask = hddm->blocks->dist_mask; @@ -1131,7 +1128,7 @@ CMSCSparseMatrix *build_cmsc_sparse_matrix(HDDNode *hdd, int level, bool transpo HDDMatrices *build_hdd_matrices_mdp(DdNode *mdp, HDDMatrices *existing_mdp, DdNode **rvars, DdNode **cvars, int num_vars, DdNode **ndvars, int num_ndvars, ODDNode *odd) { - int i, j; + int i; DdNode *tmp; HDDMatrix *hddm; HDDMatrices *res; @@ -1293,7 +1290,6 @@ void rearrange_hdd_blocks(HDDMatrix *hddm, bool ooc) unsigned char *b_counts = hddm->blocks->counts; int *b_starts = (int *)hddm->blocks->counts; bool b_use_counts = hddm->blocks->use_counts; - int *b_offsets = hddm->blocks->offsets; int b_dist_shift = hddm->blocks->dist_shift; // go through each row/column of blocks @@ -1349,7 +1345,7 @@ double *hdd_negative_row_sums(HDDMatrix *hddm, int n) double *hdd_negative_row_sums(HDDMatrix *hddm, int n, bool transpose) { - int i, j, l, h, i2, j2, l2, h2; + int i, j, l, h; double *diags; bool compact_b = hddm->compact_b; compact_sm = hddm->compact_sm; @@ -1374,7 +1370,6 @@ double *hdd_negative_row_sums(HDDMatrix *hddm, int n, bool transpose) // stuff for block storage int b_n = hddm->blocks->n; - int b_nnz = hddm->blocks->nnz; HDDNode **b_blocks = hddm->blocks->blocks; unsigned int *b_rowscols = hddm->blocks->rowscols; unsigned char *b_counts = hddm->blocks->counts; diff --git a/prism/src/mtbdd/PM_ExportLabels.cc b/prism/src/mtbdd/PM_ExportLabels.cc index 3e65e7fa..947ec724 100644 --- a/prism/src/mtbdd/PM_ExportLabels.cc +++ b/prism/src/mtbdd/PM_ExportLabels.cc @@ -64,7 +64,6 @@ jstring fn // filename jobject *label_names; DdNode **vars = jlong_to_DdNode_array(v); ODDNode *odd = jlong_to_ODDNode(od); - const char *filename; int i; // unpack jni arrays diff --git a/prism/src/mtbdd/PM_NondetInstReward.cc b/prism/src/mtbdd/PM_NondetInstReward.cc index 741c4dca..02158004 100644 --- a/prism/src/mtbdd/PM_NondetInstReward.cc +++ b/prism/src/mtbdd/PM_NondetInstReward.cc @@ -71,7 +71,7 @@ jlong __pointer in long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int iters, i; + int iters; // start clocks start1 = start2 = util_cpu_time(); diff --git a/prism/src/mtbdd/PM_ProbCumulReward.cc b/prism/src/mtbdd/PM_ProbCumulReward.cc index 54a9b00f..297488ad 100644 --- a/prism/src/mtbdd/PM_ProbCumulReward.cc +++ b/prism/src/mtbdd/PM_ProbCumulReward.cc @@ -65,7 +65,7 @@ jint bound // time bound long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int iters, i; + int iters; // start clocks start1 = start2 = util_cpu_time(); diff --git a/prism/src/mtbdd/PM_ProbInstReward.cc b/prism/src/mtbdd/PM_ProbInstReward.cc index d753f053..b18d56bb 100644 --- a/prism/src/mtbdd/PM_ProbInstReward.cc +++ b/prism/src/mtbdd/PM_ProbInstReward.cc @@ -63,7 +63,7 @@ jint bound // time bound long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // misc - int iters, i; + int iters; // start clocks start1 = start2 = util_cpu_time(); diff --git a/prism/src/mtbdd/PM_ProbReachReward.cc b/prism/src/mtbdd/PM_ProbReachReward.cc index 55a08d81..c3472d06 100644 --- a/prism/src/mtbdd/PM_ProbReachReward.cc +++ b/prism/src/mtbdd/PM_ProbReachReward.cc @@ -66,15 +66,6 @@ jlong __pointer m // 'maybe' states // mtbdds DdNode *reach, *a, *sol, *tmp; - // timing stuff - long start1, start2, start3, stop; - double time_taken, time_for_setup, time_for_iters; - // misc - int i, iters; - bool done; - - // start clocks - start1 = start2 = util_cpu_time(); // get reachable states reach = odd->dd; diff --git a/prism/src/mtbdd/PM_StochCumulReward.cc b/prism/src/mtbdd/PM_StochCumulReward.cc index d6da847f..a28a5951 100644 --- a/prism/src/mtbdd/PM_StochCumulReward.cc +++ b/prism/src/mtbdd/PM_StochCumulReward.cc @@ -61,7 +61,7 @@ jdouble time // time bound DdNode **cvars = jlong_to_DdNode_array(cv); // col vars // mtbdds - DdNode *reach, *diags, *q, *r, *sol, *tmp, *sum; + DdNode *reach, *diags, *q, *sol, *tmp, *sum; // model stats // int n; // fox glynn stuff diff --git a/prism/src/mtbdd/PM_StochSteadyState.cc b/prism/src/mtbdd/PM_StochSteadyState.cc index 22bfd7ae..6b6922c6 100644 --- a/prism/src/mtbdd/PM_StochSteadyState.cc +++ b/prism/src/mtbdd/PM_StochSteadyState.cc @@ -56,10 +56,9 @@ jint num_cvars DdNode **rvars = jlong_to_DdNode_array(rv); // row vars DdNode **cvars = jlong_to_DdNode_array(cv); // col vars // mtbdds - DdNode *diags, *q, *a, *b, *soln, *tmp; + DdNode *diags, *q, *a, *b, *soln; // misc - int i; - double deltat, d; + double deltat; // compute diagonals Cudd_Ref(trans); diff --git a/prism/src/sparse/PS_JOR.cc b/prism/src/sparse/PS_JOR.cc index b716ce45..0c7a1e55 100644 --- a/prism/src/sparse/PS_JOR.cc +++ b/prism/src/sparse/PS_JOR.cc @@ -66,7 +66,7 @@ jdouble omega // omega (over-relaxation parameter) DdNode *init = jlong_to_DdNode(_init); // init soln // mtbdds - DdNode *reach, *diags, *id, *tmp; + DdNode *reach, *diags, *id; // model stats int n; long nnz; diff --git a/prism/src/sparse/PS_NondetInstReward.cc b/prism/src/sparse/PS_NondetInstReward.cc index cdb15839..bed682f1 100644 --- a/prism/src/sparse/PS_NondetInstReward.cc +++ b/prism/src/sparse/PS_NondetInstReward.cc @@ -65,8 +65,6 @@ jlong __pointer in DdNode **ndvars = jlong_to_DdNode_array(ndv); // nondet vars DdNode *init = jlong_to_DdNode(in); - // mtbdds - DdNode *tmp; // model stats int n, nc; long nnz; diff --git a/prism/src/sparse/PS_NondetReachReward.cc b/prism/src/sparse/PS_NondetReachReward.cc index e12d9a2d..1d872500 100644 --- a/prism/src/sparse/PS_NondetReachReward.cc +++ b/prism/src/sparse/PS_NondetReachReward.cc @@ -71,7 +71,7 @@ jboolean min // min or max probabilities (true = min, false = max) DdNode *maybe = jlong_to_DdNode(m); // 'maybe' states // mtbdds - DdNode *a, *tmp; + DdNode *a; // model stats int n, nc, nc_r; long nnz, nnz_r; @@ -182,9 +182,9 @@ jboolean min // min or max probabilities (true = min, false = max) bool use_counts = ndsm->use_counts; unsigned int *cols = ndsm->cols; // and then for transition rewards matrix + // (note: we don't need row_counts/row_starts for + // this since choice structure mirrors transition matrix) double *non_zeros_r = ndsm_r->non_zeros; - unsigned char *row_counts_r = ndsm_r->row_counts; - int *row_starts_r = (int *)ndsm_r->row_counts; unsigned char *choice_counts_r = ndsm_r->choice_counts; int *choice_starts_r = (int *)ndsm_r->choice_counts; bool use_counts_r = ndsm_r->use_counts; diff --git a/prism/src/sparse/PS_ProbInstReward.cc b/prism/src/sparse/PS_ProbInstReward.cc index 3bfeadfb..c82ebcb9 100644 --- a/prism/src/sparse/PS_ProbInstReward.cc +++ b/prism/src/sparse/PS_ProbInstReward.cc @@ -59,13 +59,11 @@ jint bound // time bound DdNode **rvars = jlong_to_DdNode_array(rv); // row vars DdNode **cvars = jlong_to_DdNode_array(cv); // col vars - // mtbdds - DdNode *tmp; // model stats int n; long nnz; // flags - bool compact_tr, compact_r; + bool compact_tr; // sparse matrix RMSparseMatrix *rmsm; CMSRSparseMatrix *cmsrsm; @@ -77,7 +75,6 @@ jint bound // time bound // misc int i, j, l, h, iters; double d, kb, kbt; - bool first; // start clocks start1 = start2 = util_cpu_time(); diff --git a/prism/src/sparse/PS_ProbUntil.cc b/prism/src/sparse/PS_ProbUntil.cc index 9d2249b6..91fa7afb 100644 --- a/prism/src/sparse/PS_ProbUntil.cc +++ b/prism/src/sparse/PS_ProbUntil.cc @@ -61,7 +61,7 @@ jlong __pointer m // 'maybe' states DdNode *maybe = jlong_to_DdNode(m); // 'maybe' states // mtbdds - DdNode *reach, *transr, *a, *b, *tmp; + DdNode *reach, *a, *b, *tmp; // vectors double *soln; diff --git a/prism/src/sparse/PS_SOR.cc b/prism/src/sparse/PS_SOR.cc index 7be34424..ccc5527e 100644 --- a/prism/src/sparse/PS_SOR.cc +++ b/prism/src/sparse/PS_SOR.cc @@ -67,7 +67,7 @@ jboolean forwards // forwards or backwards? DdNode *init = jlong_to_DdNode(_init); // init soln // mtbdds - DdNode *reach, *diags, *id, *tmp; + DdNode *reach, *diags, *id; // model stats int n; long nnz; @@ -77,7 +77,7 @@ jboolean forwards // forwards or backwards? RMSparseMatrix *rmsm; CMSRSparseMatrix *cmsrsm; // vectors - double *diags_vec, *b_vec, *soln, *tmpsoln; + double *diags_vec, *b_vec, *soln; DistVector *diags_dist, *b_dist; // timing stuff long start1, start2, start3, stop; diff --git a/prism/src/sparse/sparse.cc b/prism/src/sparse/sparse.cc index 517ca3bd..5d0ce367 100644 --- a/prism/src/sparse/sparse.cc +++ b/prism/src/sparse/sparse.cc @@ -179,7 +179,7 @@ RCSparseMatrix *build_rc_sparse_matrix(DdManager *ddman, DdNode *matrix, DdNode RCSparseMatrix *build_rc_sparse_matrix(DdManager *ddman, DdNode *matrix, DdNode **rvars, DdNode **cvars, int num_vars, ODDNode *odd, bool transpose) { - int i, n, nnz; + int n, nnz; // create new data structure rcsm = new RCSparseMatrix(); @@ -373,9 +373,8 @@ CMSCSparseMatrix *build_cmsc_sparse_matrix(DdManager *ddman, DdNode *matrix, DdN NDSparseMatrix *build_nd_sparse_matrix(DdManager *ddman, DdNode *mdp, DdNode **rvars, DdNode **cvars, int num_vars, DdNode **ndvars, int num_ndvars, ODDNode *odd) { - int i, j, n, nm, nc, nnz, max, max2; + int i, n, nm, nc, nnz, max, max2; DdNode *tmp, **matrices, **matrices_bdds; - NDSparseMatrix *res; // create new data structure ndsm = new NDSparseMatrix(); @@ -496,9 +495,8 @@ NDSparseMatrix *build_nd_sparse_matrix(DdManager *ddman, DdNode *mdp, DdNode **r NDSparseMatrix *build_sub_nd_sparse_matrix(DdManager *ddman, DdNode *mdp, DdNode *submdp, DdNode **rvars, DdNode **cvars, int num_vars, DdNode **ndvars, int num_ndvars, ODDNode *odd) { - int i, j, n, nm, nc, nnz, max, max2; + int i, n, nm, nc, nnz, max, max2; DdNode *tmp, **matrices, **submatrices, **matrices_bdds; - NDSparseMatrix *res; // create new data structure ndsm = new NDSparseMatrix();