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

PH iteration methods: use MeasureSupNorm. 

Uses common code that was refactored to Measures.h


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12080 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
7c612640da
commit
522adb9b57
10 changed files with 100 additions and 133 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. 23
      prism/src/hybrid/PH_JOR.cc
  2. 23
      prism/src/hybrid/PH_NondetReachReward.cc
  3. 23
      prism/src/hybrid/PH_NondetUntil.cc
  4. 21
      prism/src/hybrid/PH_PSOR.cc
  5. 23
      prism/src/hybrid/PH_Power.cc
  6. 19
      prism/src/hybrid/PH_ProbTransient.cc
  7. 44
      prism/src/hybrid/PH_SOR.cc
  8. 19
      prism/src/hybrid/PH_StochBoundedUntil.cc
  9. 19
      prism/src/hybrid/PH_StochCumulReward.cc
  10. 19
      prism/src/hybrid/PH_StochTransient.cc

23
prism/src/hybrid/PH_JOR.cc
View File

@ -37,6 +37,7 @@
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include "Measures.h"
#include "ExportIterations.h"
#include <new>
#include <memory>
@ -101,9 +102,11 @@ jdouble omega // omega (over-relaxation parameter)
double time_taken, time_for_setup, time_for_iters;
// misc
int i, iters;
double x, sup_norm, kb, kbt;
double x, kb, kbt;
bool done;
// measure for convergence termination check
MeasureSupNorm measure(term_crit == TERM_CRIT_RELATIVE);
// exception handling around whole function
try {
@ -274,21 +277,15 @@ jdouble omega // omega (over-relaxation parameter)
iterationExport->exportVector(soln2, n, 0);
// check convergence
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) {
measure.reset();
measure.measure(soln, soln2, n);
if (measure.value() < term_crit_param) {
done = true;
}
// 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, "Iteration %d: max %sdiff=%f", iters, measure.isRelative()?"relative ":"", measure.value());
PH_PrintToMainLog(env, ", %.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}

23
prism/src/hybrid/PH_NondetReachReward.cc
View File

@ -37,6 +37,7 @@
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include "Measures.h"
#include "ExportIterations.h"
#include <new>
#include <memory>
@ -107,9 +108,11 @@ 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, x, sup_norm, kb, kbt;
double d, kb, kbt;
bool done;
// measure for convergence termination check
MeasureSupNorm measure(term_crit == TERM_CRIT_RELATIVE);
// exception handling around whole function
try {
@ -297,21 +300,15 @@ jboolean min // min or max probabilities (true = min, false = max)
iterationExport->exportVector(soln2, n, 0);
// check convergence
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) {
measure.reset();
measure.measure(soln, soln2, n);
if (measure.value() < term_crit_param) {
done = true;
}
// 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, "Iteration %d: max %sdiff=%f", iters, measure.isRelative()?"relative ":"", measure.value());
PH_PrintToMainLog(env, ", %.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}

23
prism/src/hybrid/PH_NondetUntil.cc
View File

@ -37,6 +37,7 @@
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include "Measures.h"
#include "ExportIterations.h"
#include <new>
#include <memory>
@ -101,9 +102,11 @@ 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 x, sup_norm, kb, kbt;
double x, kb, kbt;
bool done;
// measure for convergence termination check
MeasureSupNorm measure(term_crit == TERM_CRIT_RELATIVE);
// exception handling around whole function
try {
@ -248,21 +251,15 @@ jboolean min // min or max probabilities (true = min, false = max)
iterationExport->exportVector(soln2, n, 0);
// check convergence
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) {
measure.reset();
measure.measure(soln, soln2, n);
if (measure.value() < term_crit_param) {
done = true;
}
// 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, "Iteration %d: max %sdiff=%f", iters, measure.isRelative()?"relative ":"", measure.value());
PH_PrintToMainLog(env, ", %.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}

21
prism/src/hybrid/PH_PSOR.cc
View File

@ -37,6 +37,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "Measures.h"
#include "ExportIterations.h"
#include <new>
#include <memory>
@ -102,9 +103,11 @@ jboolean forwards // forwards or backwards?
double time_taken, time_for_setup, time_for_iters;
// misc
int i, j, fb, l, h, i2, h2, iters;
double x, sup_norm, kb, kbt;
double x, kb, kbt;
bool done;
// measure for convergence termination check
MeasureSupNorm measure(term_crit == TERM_CRIT_RELATIVE);
// exception handling around whole function
try {
@ -258,7 +261,7 @@ jboolean forwards // forwards or backwards?
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
sup_norm = 0.0;
measure.reset();
// stuff for block storage
int b_n = hddm->blocks->n;
@ -327,13 +330,9 @@ jboolean forwards // forwards or backwards?
// do over-relaxation if necessary
if (omega != 1) {
soln2[i2] = ((1-omega) * soln[row_offset + i2]) + (omega * soln2[i2]);
}
// compute norm for convergence
x = fabs(soln2[i2] - soln[row_offset + i2]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[i2];
}
if (x > sup_norm) sup_norm = x;
// compute norm for convergence
measure.measure(soln[row_offset + i2], soln2[i2]);
// set vector element
soln[row_offset + i2] = soln2[i2];
}
@ -343,10 +342,10 @@ jboolean forwards // forwards or backwards?
iterationExport->exportVector(soln, n, 0);
// check convergence
if (sup_norm < term_crit_param) {
if (measure.value() < term_crit_param) {
done = true;
}
// PH_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
}

23
prism/src/hybrid/PH_Power.cc
View File

@ -37,6 +37,7 @@
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include "Measures.h"
#include "ExportIterations.h"
#include <new>
#include <memory>
@ -98,9 +99,11 @@ 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 x, sup_norm, kb, kbt;
double x, kb, kbt;
bool done;
// measure for convergence termination check
MeasureSupNorm measure(term_crit == TERM_CRIT_RELATIVE);
// exception handling around whole function
try {
@ -206,21 +209,15 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?)
iterationExport->exportVector(soln2, n, 0);
// check convergence
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) {
measure.reset();
measure.measure(soln, soln2, n);
if (measure.value() < term_crit_param) {
done = true;
}
// 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, "Iteration %d: max %sdiff=%f", iters, measure.isRelative()?"relative ":"", measure.value());
PH_PrintToMainLog(env, ", %.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}

19
prism/src/hybrid/PH_ProbTransient.cc
View File

@ -37,6 +37,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "Measures.h"
#include <new>
// local prototypes
@ -85,11 +86,13 @@ jint time // time
double *tmpsoln = NULL, *sum = NULL;
// timing stuff
long start1, start2, start3, stop;
double x, sup_norm, time_taken, time_for_setup, time_for_iters;
double time_taken, time_for_setup, time_for_iters;
// misc
bool done;
int i, iters;
double kb, kbt;
// measure for convergence termination check
MeasureSupNorm measure(term_crit == TERM_CRIT_RELATIVE);
// exception handling around whole function
try {
@ -161,15 +164,9 @@ jint time // time
// 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) {
measure.reset();
measure.measure(soln, soln2, n);
if (measure.value() < term_crit_param) {
done = true;
}
}
@ -177,7 +174,7 @@ jint time // time
// 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);
if (do_ss_detect) PH_PrintToMainLog(env, "max %sdiff=%f, ", measure.isRelative()?"relative ":"", measure.value());
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}

44
prism/src/hybrid/PH_SOR.cc
View File

@ -38,6 +38,7 @@
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include "Measures.h"
#include "ExportIterations.h"
#include <new>
#include <memory>
@ -57,8 +58,9 @@ static int sm_dist_mask;
static double *diags_vec = NULL;
static DistVector *diags_dist = NULL;
static double *soln = NULL, *soln2 = NULL;
static double x, sup_norm, omega;
static double omega;
static bool forwards;
static MeasureSupNorm* measure = NULL;
//------------------------------------------------------------------------------
@ -112,7 +114,10 @@ jboolean fwds // forwards or backwards?
int i, j, fb, l, h, i2, h2, iters;
double kb, kbt;
bool done, diag_done;
// measure for convergence termination check
// dynamically allocated so sor_rm and sor_cmsr have access as well
measure = new MeasureSupNorm(term_crit == TERM_CRIT_RELATIVE);
// exception handling around whole function
try {
@ -265,7 +270,7 @@ jboolean fwds // forwards or backwards?
iters++;
sup_norm = 0.0;
measure->reset();
// stuff for block storage
int b_n = hddm->blocks->n;
@ -355,13 +360,9 @@ jboolean fwds // forwards or backwards?
// do over-relaxation if necessary
if (omega != 1) {
soln2[i2] = ((1-omega) * soln[row_offset + i2]) + (omega * soln2[i2]);
}
// compute norm for convergence
x = fabs(soln2[i2] - soln[row_offset + i2]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[i2];
}
if (x > sup_norm) sup_norm = x;
// compute norm for convergence
measure->measure(soln[row_offset + i2], soln2[i2]);
// set vector element
soln[row_offset + i2] = soln2[i2];
}
@ -370,9 +371,7 @@ jboolean fwds // forwards or backwards?
if (l_b_max) {
soln2[0] *= ((!compact_d)?(diags_vec[row_offset]):(diags_dist->dist[(int)diags_dist->ptrs[row_offset]]));
if (omega != 1) soln2[0] = ((1-omega) * soln[row_offset]) + (omega * soln2[0]);
x = fabs(soln2[0] - soln[row_offset]);
if (term_crit == TERM_CRIT_RELATIVE) x /= soln2[0];
if (x > sup_norm) sup_norm = x;
measure->measure(soln[row_offset], soln2[0]);
soln[row_offset] = soln2[0];
}
}
@ -381,13 +380,13 @@ jboolean fwds // forwards or backwards?
iterationExport->exportVector(soln, n, 0);
// check convergence
if (sup_norm < term_crit_param) {
if (measure->value() < term_crit_param) {
done = true;
}
// 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, "Iteration %d: max %sdiff=%f", iters, measure->isRelative()?"relative ":"", measure->value());
PH_PrintToMainLog(env, ", %.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}
@ -421,6 +420,7 @@ jboolean fwds // forwards or backwards?
if (b_vec) delete[] b_vec;
if (b_dist) delete b_dist;
if (soln2) delete[] soln2;
if (measure) delete measure;
return ptr_to_jlong(soln);
}
@ -513,13 +513,9 @@ static void sor_rm(RMSparseMatrix *rmsm, int row_offset, int col_offset, int r,
// do over-relaxation if necessary
if (omega != 1) {
soln2[r + i2] = ((1-omega) * soln[row_offset + r + i2]) + (omega * soln2[r + i2]);
}
// compute norm for convergence
x = fabs(soln2[r + i2] - soln[row_offset + r + i2]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[r + i2];
}
if (x > sup_norm) sup_norm = x;
// compute norm for convergence
measure->measure(soln[row_offset + r + i2], soln2[r + i2]);
// set vector element
soln[row_offset + r + i2] = soln2[r + i2];
}
@ -564,13 +560,9 @@ static void sor_cmsr(CMSRSparseMatrix *cmsrsm, int row_offset, int col_offset, i
// do over-relaxation if necessary
if (omega != 1) {
soln2[r + i2] = ((1-omega) * soln[row_offset + r + i2]) + (omega * soln2[r + i2]);
}
// compute norm for convergence
x = fabs(soln2[r + i2] - soln[row_offset + r + i2]);
if (term_crit == TERM_CRIT_RELATIVE) {
x /= soln2[r + i2];
}
if (x > sup_norm) sup_norm = x;
// compute norm for convergence
measure->measure(soln[row_offset + r + i2], soln2[r + i2]);
// set vector element
soln[row_offset + r + i2] = soln2[r + i2];
}

19
prism/src/hybrid/PH_StochBoundedUntil.cc
View File

@ -37,6 +37,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "Measures.h"
#include <new>
// local prototypes
@ -100,7 +101,9 @@ jlong __jlongpointer mu // probs for multiplying
// misc
bool done;
long i, iters, num_iters;
double x, sup_norm, kb, kbt, max_diag, weight, term_crit_param_unif;
double x, kb, kbt, max_diag, weight, term_crit_param_unif;
// measure for convergence termination check
MeasureSupNorm measure(term_crit == TERM_CRIT_RELATIVE);
// exception handling around whole function
try {
@ -250,15 +253,9 @@ jlong __jlongpointer mu // probs for multiplying
// 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) {
measure.reset();
measure.measure(soln, soln2, n);
if (measure.value() < term_crit_param_unif) {
done = true;
}
}
@ -284,7 +281,7 @@ jlong __jlongpointer mu // probs for multiplying
// 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);
if (do_ss_detect) PH_PrintToMainLog(env, "max %sdiff=%f, ", measure.isRelative()?"relative ":"", measure.value());
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}

19
prism/src/hybrid/PH_StochCumulReward.cc
View File

@ -37,6 +37,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "Measures.h"
#include <new>
// local prototypes
@ -99,7 +100,9 @@ jdouble time // time bound
// misc
bool done;
long i, iters, num_iters;
double x, sup_norm, max_diag, weight, kb, kbt, term_crit_param_unif;
double max_diag, weight, kb, kbt, term_crit_param_unif;
// measure for convergence termination check
MeasureSupNorm measure(term_crit == TERM_CRIT_RELATIVE);
// exception handling around whole function
try {
@ -260,15 +263,9 @@ jdouble time // time bound
// 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) {
measure.reset();
measure.measure(soln, soln2, n);
if (measure.value() < term_crit_param_unif) {
done = true;
}
}
@ -295,7 +292,7 @@ jdouble time // time bound
// 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);
if (do_ss_detect) PH_PrintToMainLog(env, "max %sdiff=%f, ", measure.isRelative()?"relative ":"", measure.value());
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}

19
prism/src/hybrid/PH_StochTransient.cc
View File

@ -37,6 +37,7 @@
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
#include "Measures.h"
#include <new>
// local prototypes
@ -95,7 +96,9 @@ jdouble time // time bound
// misc
bool done;
long i, iters, num_iters;
double x, sup_norm, kb, kbt, max_diag, weight, term_crit_param_unif;
double kb, kbt, max_diag, weight, term_crit_param_unif;
// measure for convergence termination check
MeasureSupNorm measure(term_crit == TERM_CRIT_RELATIVE);
// exception handling around whole function
try {
@ -231,15 +234,9 @@ jdouble time // time bound
// 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) {
measure.reset();
measure.measure(soln, soln2, n);
if (measure.value() < term_crit_param_unif) {
done = true;
}
}
@ -265,7 +262,7 @@ jdouble time // time bound
// 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);
if (do_ss_detect) PH_PrintToMainLog(env, "max %sdiff=%f, ", measure.isRelative()?"relative ":"", measure.value());
PH_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time();
}

Write Preview
Loading…
Cancel
Save