Browse Source

- changed %d to %ld where fox_glynn output is logged

- delete fgw.weights after it is used



git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1931 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Vojtech Forejt 16 years ago
parent
commit
93f250b941
  1. 7
      prism/src/hybrid/PH_StochBoundedUntil.cc
  2. 8
      prism/src/mtbdd/PM_StochBoundedUntil.cc
  3. 7
      prism/src/sparse/PS_StochBoundedUntil.cc

7
prism/src/hybrid/PH_StochBoundedUntil.cc

@ -212,7 +212,7 @@ jlong __jlongpointer mu // probs for multiplying
for (i = fgw.left; i <= fgw.right; i++) { for (i = fgw.left; i <= fgw.right; i++) {
fgw.weights[i-fgw.left] /= fgw.total_weight; fgw.weights[i-fgw.left] /= fgw.total_weight;
} }
PH_PrintToMainLog(env, "Fox-Glynn: left = %d, right = %d\n", fgw.left, fgw.right);
PH_PrintToMainLog(env, "Fox-Glynn: left = %ld, right = %ld\n", fgw.left, fgw.right);
// set up vectors // set up vectors
for (i = 0; i < n; i++) { for (i = 0; i < n; i++) {
@ -285,7 +285,7 @@ jlong __jlongpointer mu // probs for multiplying
} }
// add to sum // add to sum
for (i = 0; i < n; i++) sum[i] += weight * soln2[i]; for (i = 0; i < n; i++) sum[i] += weight * soln2[i];
PH_PrintToMainLog(env, "\nSteady state detected at iteration %d\n", iters);
PH_PrintToMainLog(env, "\nSteady state detected at iteration %ld\n", iters);
num_iters = iters; num_iters = iters;
break; break;
} }
@ -310,7 +310,7 @@ jlong __jlongpointer mu // probs for multiplying
// print iters/timing info // print iters/timing info
if (num_iters == -1) num_iters = fgw.right; if (num_iters == -1) num_iters = fgw.right;
PH_PrintToMainLog(env, "\nIterative method: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", num_iters, time_taken, time_for_iters/num_iters, time_for_setup);
PH_PrintToMainLog(env, "\nIterative method: %ld iterations in %.2f seconds (average %.6f, setup %.2f)\n", num_iters, time_taken, time_for_iters/num_iters, time_for_setup);
// catch exceptions: register error, free memory // catch exceptions: register error, free memory
} catch (std::bad_alloc e) { } catch (std::bad_alloc e) {
@ -330,6 +330,7 @@ jlong __jlongpointer mu // probs for multiplying
if (diags_dist) delete diags_dist; if (diags_dist) delete diags_dist;
if (soln) delete[] soln; if (soln) delete[] soln;
if (soln2) delete[] soln2; if (soln2) delete[] soln2;
if (fgw.weights) delete[] fgw.weights;
return ptr_to_jlong(sum); return ptr_to_jlong(sum);
} }

8
prism/src/mtbdd/PM_StochBoundedUntil.cc

@ -187,7 +187,7 @@ jlong __jlongpointer mu // probs for multiplying
for (i = fgw.left; i <= fgw.right; i++) { for (i = fgw.left; i <= fgw.right; i++) {
fgw.weights[i-fgw.left] /= fgw.total_weight; fgw.weights[i-fgw.left] /= fgw.total_weight;
} }
PM_PrintToMainLog(env, "Fox-Glynn: left = %d, right = %d\n", fgw.left, fgw.right);
PM_PrintToMainLog(env, "Fox-Glynn: left = %ld, right = %ld\n", fgw.left, fgw.right);
// PM_PrintToMainLog(env, "right-left = %d\n", fgw.right-fgw.left); // PM_PrintToMainLog(env, "right-left = %d\n", fgw.right-fgw.left);
// PM_PrintToMainLog(env, "total_weight = %f\n", fgw.total_weight); // PM_PrintToMainLog(env, "total_weight = %f\n", fgw.total_weight);
@ -288,7 +288,7 @@ jlong __jlongpointer mu // probs for multiplying
// add to sum // add to sum
Cudd_Ref(tmp); Cudd_Ref(tmp);
sum = DD_Apply(ddman, APPLY_PLUS, sum, DD_Apply(ddman, APPLY_TIMES, tmp, DD_Constant(ddman, weight))); sum = DD_Apply(ddman, APPLY_PLUS, sum, DD_Apply(ddman, APPLY_TIMES, tmp, DD_Constant(ddman, weight)));
PM_PrintToMainLog(env, "\nSteady state detected at iteration %d\n", iters);
PM_PrintToMainLog(env, "\nSteady state detected at iteration %ld\n", iters);
num_iters = iters; num_iters = iters;
Cudd_RecursiveDeref(ddman, tmp); Cudd_RecursiveDeref(ddman, tmp);
break; break;
@ -314,7 +314,7 @@ jlong __jlongpointer mu // probs for multiplying
// print iterations/timing info // print iterations/timing info
if (num_iters == -1) num_iters = fgw.right; if (num_iters == -1) num_iters = fgw.right;
PM_PrintToMainLog(env, "\nIterative method: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", num_iters, time_taken, time_for_iters/num_iters, time_for_setup);
PM_PrintToMainLog(env, "\nIterative method: %ld iterations in %.2f seconds (average %.6f, setup %.2f)\n", num_iters, time_taken, time_for_iters/num_iters, time_for_setup);
// free memory // free memory
if (combine) { if (combine) {
@ -328,6 +328,8 @@ jlong __jlongpointer mu // probs for multiplying
} }
Cudd_RecursiveDeref(ddman, diags); Cudd_RecursiveDeref(ddman, diags);
Cudd_RecursiveDeref(ddman, sol); Cudd_RecursiveDeref(ddman, sol);
if (fgw.weights) delete[] fgw.weights;
return ptr_to_jlong(sum); return ptr_to_jlong(sum);
} }

7
prism/src/sparse/PS_StochBoundedUntil.cc

@ -201,7 +201,7 @@ jlong __jlongpointer mu // probs for multiplying
for (i = fgw.left; i <= fgw.right; i++) { for (i = fgw.left; i <= fgw.right; i++) {
fgw.weights[i-fgw.left] /= fgw.total_weight; fgw.weights[i-fgw.left] /= fgw.total_weight;
} }
PS_PrintToMainLog(env, "Fox-Glynn: left = %d, right = %d\n", fgw.left, fgw.right);
PS_PrintToMainLog(env, "Fox-Glynn: left = %ld, right = %ld\n", fgw.left, fgw.right);
// set up vectors // set up vectors
for (i = 0; i < n; i++) { for (i = 0; i < n; i++) {
@ -311,7 +311,7 @@ jlong __jlongpointer mu // probs for multiplying
} }
// add to sum // add to sum
for (i = 0; i < n; i++) sum[i] += weight * soln2[i]; for (i = 0; i < n; i++) sum[i] += weight * soln2[i];
PS_PrintToMainLog(env, "\nSteady state detected at iteration %d\n", iters);
PS_PrintToMainLog(env, "\nSteady state detected at iteration %ld\n", iters);
num_iters = iters; num_iters = iters;
break; break;
} }
@ -336,7 +336,7 @@ jlong __jlongpointer mu // probs for multiplying
// print iters/timing info // print iters/timing info
if (num_iters == -1) num_iters = fgw.right; if (num_iters == -1) num_iters = fgw.right;
PS_PrintToMainLog(env, "\nIterative method: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", num_iters, time_taken, time_for_iters/num_iters, time_for_setup);
PS_PrintToMainLog(env, "\nIterative method: %ld iterations in %.2f seconds (average %.6f, setup %.2f)\n", num_iters, time_taken, time_for_iters/num_iters, time_for_setup);
// catch exceptions: register error, free memory // catch exceptions: register error, free memory
} catch (std::bad_alloc e) { } catch (std::bad_alloc e) {
@ -357,6 +357,7 @@ jlong __jlongpointer mu // probs for multiplying
if (diags_dist) delete diags_dist; if (diags_dist) delete diags_dist;
if (soln) delete[] soln; if (soln) delete[] soln;
if (soln2) delete[] soln2; if (soln2) delete[] soln2;
if (fgw.weights) delete[] fgw.weights;
return ptr_to_jlong(sum); return ptr_to_jlong(sum);
} }

Loading…
Cancel
Save