Browse Source

Add intermittent progress updates to numerical solution (hybrid engine).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5265 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
commit
5cb3822798
  1. 44
      prism/src/hybrid/PH_JOR.cc
  2. 14
      prism/src/hybrid/PH_NondetBoundedUntil.cc
  3. 43
      prism/src/hybrid/PH_NondetReachReward.cc
  4. 43
      prism/src/hybrid/PH_NondetUntil.cc
  5. 44
      prism/src/hybrid/PH_Power.cc
  6. 14
      prism/src/hybrid/PH_ProbBoundedUntil.cc
  7. 14
      prism/src/hybrid/PH_ProbCumulReward.cc
  8. 14
      prism/src/hybrid/PH_ProbInstReward.cc
  9. 39
      prism/src/hybrid/PH_ProbTransient.cc
  10. 12
      prism/src/hybrid/PH_SOR.cc
  11. 39
      prism/src/hybrid/PH_StochBoundedUntil.cc
  12. 31
      prism/src/hybrid/PH_StochCumulReward.cc
  13. 39
      prism/src/hybrid/PH_StochTransient.cc

44
prism/src/hybrid/PH_JOR.cc

@ -36,6 +36,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include <new>
// local prototypes
@ -98,7 +99,7 @@ jdouble omega // omega (over-relaxation parameter)
double time_taken, time_for_setup, time_for_iters;
// misc
int i, iters;
double kb, kbt;
double x, sup_norm, kb, kbt;
bool done;
// exception handling around whole function
@ -218,6 +219,7 @@ jdouble omega // omega (over-relaxation parameter)
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start iterations
iters = 0;
@ -228,9 +230,6 @@ jdouble omega // omega (over-relaxation parameter)
iters++;
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
// matrix multiply
// initialise vector
@ -260,36 +259,29 @@ jdouble omega // omega (over-relaxation parameter)
}
// check convergence
// (note: doing outside loop means may not need to check all elements)
switch (term_crit) {
case TERM_CRIT_ABSOLUTE:
done = true;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i]) > term_crit_param) {
done = false;
break;
}
sup_norm = 0.0;
for (i = 0; i < n; i++) {
x = fabs(soln2[i] - soln[i]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[i];
}
break;
case TERM_CRIT_RELATIVE:
if (x > sup_norm) sup_norm = x;
}
if (sup_norm < term_crit_param) {
done = true;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i])/soln2[i] > term_crit_param) {
done = false;
break;
}
}
break;
}
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d: max %sdiff=%f", iters, (term_crit == TERM_CRIT_RELATIVE)?"relative ":"", sup_norm);
PH_PrintToMainLog(env, ", %.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

14
prism/src/hybrid/PH_NondetBoundedUntil.cc

@ -36,6 +36,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include <new>
// local prototypes
@ -172,6 +173,7 @@ jboolean min // min or max probabilities (true = min, false = max)
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start iterations
PH_PrintToMainLog(env, "\nStarting iterations...\n");
@ -179,9 +181,6 @@ jboolean min // min or max probabilities (true = min, false = max)
// note that we ignore max_iters as we know how any iterations _should_ be performed
for (iters = 0; iters < bound; iters++) {
// PH_PrintToMainLog(env, "iter %d\n", iters);
// start3 = util_cpu_time();
// initialise array for storing mins/maxs to -1s
// (allows us to keep track of rows not visited)
for (i = 0; i < n; i++) {
@ -234,12 +233,17 @@ jboolean min // min or max probabilities (true = min, false = max)
}
}
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d (of %d): ", iters, bound);
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

43
prism/src/hybrid/PH_NondetReachReward.cc

@ -36,6 +36,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include <new>
// local prototypes
@ -104,7 +105,7 @@ jboolean min // min or max probabilities (true = min, false = max)
double time_taken, time_for_setup, time_for_iters;
// misc
int i, j, k, iters;
double d, kb, kbt;
double d, x, sup_norm, kb, kbt;
bool done;
// exception handling around whole function
@ -207,6 +208,7 @@ jboolean min // min or max probabilities (true = min, false = max)
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start iterations
iters = 0;
@ -217,9 +219,6 @@ jboolean min // min or max probabilities (true = min, false = max)
iters++;
// PH_PrintToMainLog(env, "iter %d\n", iters);
// start3 = util_cpu_time();
// initialise array for storing mins/maxs to -1s
// (allows us to keep track of rows not visited)
for (i = 0; i < n; i++) {
@ -287,35 +286,29 @@ jboolean min // min or max probabilities (true = min, false = max)
}
// check convergence
switch (term_crit) {
case TERM_CRIT_ABSOLUTE:
done = true;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i]) > term_crit_param) {
done = false;
break;
}
sup_norm = 0.0;
for (i = 0; i < n; i++) {
x = fabs(soln2[i] - soln[i]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[i];
}
break;
case TERM_CRIT_RELATIVE:
if (x > sup_norm) sup_norm = x;
}
if (sup_norm < term_crit_param) {
done = true;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i])/soln2[i] > term_crit_param) {
done = false;
break;
}
}
break;
}
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d: max %sdiff=%f", iters, (term_crit == TERM_CRIT_RELATIVE)?"relative ":"", sup_norm);
PH_PrintToMainLog(env, ", %.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

43
prism/src/hybrid/PH_NondetUntil.cc

@ -36,6 +36,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include <new>
// local prototypes
@ -98,7 +99,7 @@ jboolean min // min or max probabilities (true = min, false = max)
double time_taken, time_for_setup, time_for_iters;
// misc
int i, j, iters;
double kb, kbt;
double x, sup_norm, kb, kbt;
bool done;
// exception handling around whole function
@ -172,6 +173,7 @@ jboolean min // min or max probabilities (true = min, false = max)
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start iterations
iters = 0;
@ -182,9 +184,6 @@ jboolean min // min or max probabilities (true = min, false = max)
iters++;
// PH_PrintToMainLog(env, "iter %d\n", iters);
// start3 = util_cpu_time();
// initialise array for storing mins/maxs to -1s
// (allows us to keep track of rows not visited)
for (i = 0; i < n; i++) {
@ -238,35 +237,29 @@ jboolean min // min or max probabilities (true = min, false = max)
}
// check convergence
switch (term_crit) {
case TERM_CRIT_ABSOLUTE:
done = true;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i]) > term_crit_param) {
done = false;
break;
}
sup_norm = 0.0;
for (i = 0; i < n; i++) {
x = fabs(soln2[i] - soln[i]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[i];
}
break;
case TERM_CRIT_RELATIVE:
if (x > sup_norm) sup_norm = x;
}
if (sup_norm < term_crit_param) {
done = true;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i])/soln2[i] > term_crit_param) {
done = false;
break;
}
}
break;
}
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d: max %sdiff=%f", iters, (term_crit == TERM_CRIT_RELATIVE)?"relative ":"", sup_norm);
PH_PrintToMainLog(env, ", %.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

44
prism/src/hybrid/PH_Power.cc

@ -36,6 +36,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include <new>
// local prototypes
@ -95,7 +96,7 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?)
double time_taken, time_for_setup, time_for_iters;
// misc
int i, iters;
double kb, kbt;
double x, sup_norm, kb, kbt;
bool done;
// exception handling around whole function
@ -168,6 +169,7 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?)
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start iterations
iters = 0;
@ -178,9 +180,6 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?)
iters++;
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
// matrix multiply
// initialise vector
@ -196,36 +195,29 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?)
power_rec(hdd, 0, 0, 0, transpose);
// check convergence
// (note: doing outside loop means may not need to check all elements)
switch (term_crit) {
case TERM_CRIT_ABSOLUTE:
done = true;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i]) > term_crit_param) {
done = false;
break;
}
sup_norm = 0.0;
for (i = 0; i < n; i++) {
x = fabs(soln2[i] - soln[i]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[i];
}
break;
case TERM_CRIT_RELATIVE:
if (x > sup_norm) sup_norm = x;
}
if (sup_norm < term_crit_param) {
done = true;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i])/soln2[i] > term_crit_param) {
done = false;
break;
}
}
break;
}
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d: max %sdiff=%f", iters, (term_crit == TERM_CRIT_RELATIVE)?"relative ":"", sup_norm);
PH_PrintToMainLog(env, ", %.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

14
prism/src/hybrid/PH_ProbBoundedUntil.cc

@ -36,6 +36,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include <new>
// local prototypes
@ -174,6 +175,7 @@ jint bound // time bound
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start iterations
PH_PrintToMainLog(env, "\nStarting iterations...\n");
@ -181,9 +183,6 @@ jint bound // time bound
// note that we ignore max_iters as we know how any iterations _should_ be performed
for (iters = 0; iters < bound; iters++) {
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
// initialise vector
for (i = 0; i < n; i++) {
soln2[i] = 0;
@ -198,12 +197,17 @@ jint bound // time bound
for (i = 0; i < n; i++) { if (yes_dist->dist[yes_dist->ptrs[i]]) soln2[i] = 1.0; }
}
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d (of %d): ", iters, bound);
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

14
prism/src/hybrid/PH_ProbCumulReward.cc

@ -36,6 +36,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include <new>
// local prototypes
@ -175,6 +176,7 @@ jint bound // time bound
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start iterations
PH_PrintToMainLog(env, "\nStarting iterations...\n");
@ -182,9 +184,6 @@ jint bound // time bound
// note that we ignore max_iters as we know how any iterations _should_ be performed
for (iters = 0; iters < bound; iters++) {
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
// initialise vector
for (i = 0; i < n; i++) {
soln2[i] = (!compact_r) ? rew_vec[i] : rew_dist->dist[rew_dist->ptrs[i]];
@ -193,12 +192,17 @@ jint bound // time bound
// do matrix vector multiply bit
mult_rec(hdd, 0, 0, 0);
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d (of %d): ", iters, bound);
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

14
prism/src/hybrid/PH_ProbInstReward.cc

@ -36,6 +36,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include <new>
// local prototypes
@ -139,6 +140,7 @@ jint bound // time bound
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start iterations
PH_PrintToMainLog(env, "\nStarting iterations...\n");
@ -146,9 +148,6 @@ jint bound // time bound
// note that we ignore max_iters as we know how any iterations _should_ be performed
for (iters = 0; iters < bound; iters++) {
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
// initialise vector
for (i = 0; i < n; i++) {
soln2[i] = 0.0;
@ -157,12 +156,17 @@ jint bound // time bound
// do matrix vector multiply bit
mult_rec(hdd, 0, 0, 0);
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d (of %d): ", iters, bound);
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

39
prism/src/hybrid/PH_ProbTransient.cc

@ -85,7 +85,7 @@ jint time // time
double *tmpsoln = NULL, *sum = NULL;
// timing stuff
long start1, start2, start3, stop;
double time_taken, time_for_setup, time_for_iters;
double x, sup_norm, time_taken, time_for_setup, time_for_iters;
// misc
bool done;
int i, iters;
@ -143,6 +143,7 @@ jint time // time
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start transient analysis
iters = 0;
@ -152,9 +153,6 @@ jint time // time
// note that we ignore max_iters as we know how any iterations _should_ be performed
for (iters = 0; iters < time && !done; iters++) {
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
// initialise vector
for (i = 0; i < n; i++) soln2[i] = 0.0;
@ -162,33 +160,32 @@ jint time // time
mult_rec(hdd, 0, 0, 0);
// check for steady state convergence
if (do_ss_detect) switch (term_crit) {
case TERM_CRIT_ABSOLUTE:
done = true;
if (do_ss_detect) {
sup_norm = 0.0;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i]) > term_crit_param) {
done = false;
break;
x = fabs(soln2[i] - soln[i]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[i];
}
if (x > sup_norm) sup_norm = x;
}
break;
case TERM_CRIT_RELATIVE:
done = true;
for (i = 0; i < n; i++) {
if (fabs((soln2[i] - soln[i])/soln2[i]) > term_crit_param) {
done = false;
break;
}
if (sup_norm < term_crit_param) {
done = true;
}
break;
}
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d (of %d): ", iters, time);
if (do_ss_detect) PH_PrintToMainLog(env, "max %sdiff=%f, ", (term_crit == TERM_CRIT_RELATIVE)?"relative ":"", sup_norm);
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

12
prism/src/hybrid/PH_SOR.cc

@ -37,6 +37,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include <new>
// local prototypes
@ -241,6 +242,7 @@ jboolean fwds // forwards or backwards?
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start iterations
iters = 0;
@ -251,9 +253,6 @@ jboolean fwds // forwards or backwards?
iters++;
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
sup_norm = 0.0;
// stuff for block storage
@ -371,7 +370,12 @@ jboolean fwds // forwards or backwards?
done = true;
}
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d: max %sdiff=%f", iters, (term_crit == TERM_CRIT_RELATIVE)?"relative ":"", sup_norm);
PH_PrintToMainLog(env, ", %.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
}
// stop clocks

39
prism/src/hybrid/PH_StochBoundedUntil.cc

@ -100,7 +100,7 @@ jlong __jlongpointer mu // probs for multiplying
// misc
bool done;
long i, iters, num_iters;
double x, kb, kbt, max_diag, weight, term_crit_param_unif;
double x, sup_norm, kb, kbt, max_diag, weight, term_crit_param_unif;
// exception handling around whole function
try {
@ -223,6 +223,7 @@ jlong __jlongpointer mu // probs for multiplying
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start transient analysis
done = false;
@ -237,9 +238,6 @@ jlong __jlongpointer mu // probs for multiplying
// note that we ignore max_iters as we know how any iterations _should_ be performed
for (iters = 1; (iters <= fgw.right) && !done; iters++) {
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
// initialise vector
if (!compact_d) {
for (i = 0; i < n; i++) soln2[i] = diags[i] * soln[i];
@ -251,25 +249,18 @@ jlong __jlongpointer mu // probs for multiplying
mult_rec(hdd, 0, 0, 0);
// check for steady state convergence
if (do_ss_detect) switch (term_crit) {
case TERM_CRIT_ABSOLUTE:
done = true;
if (do_ss_detect) {
sup_norm = 0.0;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i]) > term_crit_param_unif) {
done = false;
break;
x = fabs(soln2[i] - soln[i]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[i];
}
if (x > sup_norm) sup_norm = x;
}
break;
case TERM_CRIT_RELATIVE:
done = true;
for (i = 0; i < n; i++) {
if (fabs((soln2[i] - soln[i])/soln2[i]) > term_crit_param_unif) {
done = false;
break;
}
if (sup_norm < term_crit_param_unif) {
done = true;
}
break;
}
// special case when finished early (steady-state detected)
@ -290,6 +281,14 @@ jlong __jlongpointer mu // probs for multiplying
break;
}
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d (of %d): ", iters, fgw.right);
if (do_ss_detect) PH_PrintToMainLog(env, "max %sdiff=%f, ", (term_crit == TERM_CRIT_RELATIVE)?"relative ":"", sup_norm);
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
@ -299,8 +298,6 @@ jlong __jlongpointer mu // probs for multiplying
if (iters >= fgw.left) {
for (i = 0; i < n; i++) sum[i] += fgw.weights[iters-fgw.left] * soln[i];
}
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

31
prism/src/hybrid/PH_StochCumulReward.cc

@ -99,7 +99,7 @@ jdouble time // time bound
// misc
bool done;
long i, iters, num_iters;
double max_diag, weight, kb, kbt, term_crit_param_unif;
double x, sup_norm, max_diag, weight, kb, kbt, term_crit_param_unif;
// exception handling around whole function
try {
@ -231,6 +231,7 @@ jdouble time // time bound
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start transient analysis
done = false;
@ -247,9 +248,6 @@ jdouble time // time bound
// note that we ignore max_iters as we know how any iterations _should_ be performed
for (iters = 1; (iters <= fgw.right) && !done; iters++) {
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
// initialise vector
if (!compact_d) {
for (i = 0; i < n; i++) soln2[i] = diags[i] * soln[i];
@ -283,6 +281,21 @@ jdouble time // time bound
break;
}
// check for steady state convergence
if (do_ss_detect) {
sup_norm = 0.0;
for (i = 0; i < n; i++) {
x = fabs(soln2[i] - soln[i]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[i];
}
if (x > sup_norm) sup_norm = x;
}
if (sup_norm < term_crit_param_unif) {
done = true;
}
}
// special case when finished early (steady-state detected)
if (done) {
// work out sum of remaining poisson probabilities
@ -302,6 +315,14 @@ jdouble time // time bound
break;
}
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d (of %d): ", iters, fgw.right);
if (do_ss_detect) PH_PrintToMainLog(env, "max %sdiff=%f, ", (term_crit == TERM_CRIT_RELATIVE)?"relative ":"", sup_norm);
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
@ -313,8 +334,6 @@ jdouble time // time bound
} else {
for (i = 0; i < n; i++) sum[i] += fgw.weights[iters-fgw.left] * soln[i];
}
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

39
prism/src/hybrid/PH_StochTransient.cc

@ -95,7 +95,7 @@ jdouble time // time bound
// misc
bool done;
long i, iters, num_iters;
double kb, kbt, max_diag, weight, term_crit_param_unif;
double x, sup_norm, kb, kbt, max_diag, weight, term_crit_param_unif;
// exception handling around whole function
try {
@ -204,6 +204,7 @@ jdouble time // time bound
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
start3 = stop;
// start transient analysis
done = false;
@ -218,9 +219,6 @@ jdouble time // time bound
// note that we ignore max_iters as we know how any iterations _should_ be performed
for (iters = 1; (iters <= fgw.right) && !done; iters++) {
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
// initialise vector
if (!compact_d) {
for (i = 0; i < n; i++) soln2[i] = diags[i] * soln[i];
@ -232,25 +230,18 @@ jdouble time // time bound
mult_rec(hdd, 0, 0, 0);
// check for steady state convergence
if (do_ss_detect) switch (term_crit) {
case TERM_CRIT_ABSOLUTE:
done = true;
if (do_ss_detect) {
sup_norm = 0.0;
for (i = 0; i < n; i++) {
if (fabs(soln2[i] - soln[i]) > term_crit_param_unif) {
done = false;
break;
x = fabs(soln2[i] - soln[i]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[i];
}
if (x > sup_norm) sup_norm = x;
}
break;
case TERM_CRIT_RELATIVE:
done = true;
for (i = 0; i < n; i++) {
if (fabs((soln2[i] - soln[i])/soln2[i]) > term_crit_param_unif) {
done = false;
break;
}
if (sup_norm < term_crit_param_unif) {
done = true;
}
break;
}
// special case when finished early (steady-state detected)
@ -271,6 +262,14 @@ jdouble time // time bound
break;
}
// print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PH_PrintToMainLog(env, "Iteration %d (of %d): ", iters, fgw.right);
if (do_ss_detect) PH_PrintToMainLog(env, "max %sdiff=%f, ", (term_crit == TERM_CRIT_RELATIVE)?"relative ":"", sup_norm);
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
@ -280,8 +279,6 @@ jdouble time // time bound
if (iters >= fgw.left) {
for (i = 0; i < n; i++) sum[i] += fgw.weights[iters-fgw.left] * soln[i];
}
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}
// stop clocks

Loading…
Cancel
Save