Browse Source

(export-iterations) Sparse engine: If enabled, export iterations to HTML file

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12074 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
commit
3c2a2232e1
  1. 19
      prism/src/sparse/PS_JOR.cc
  2. 13
      prism/src/sparse/PS_NondetReachReward.cc
  3. 15
      prism/src/sparse/PS_NondetUntil.cc
  4. 15
      prism/src/sparse/PS_Power.cc
  5. 19
      prism/src/sparse/PS_SOR.cc

19
prism/src/sparse/PS_JOR.cc

@ -36,6 +36,8 @@
#include "PrismSparseGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include "ExportIterations.h"
#include <memory>
#include <new>
//------------------------------------------------------------------------------
@ -196,7 +198,17 @@ jdouble omega // omega (over-relaxation parameter)
// print total memory usage
PS_PrintMemoryToMainLog(env, "TOTAL: [", kbt, "]\n");
std::unique_ptr<ExportIterations> iterationExport;
if (PS_GetFlagExportIterations()) {
std::string title("PS_JOR (");
title += (omega == 1.0)?"Jacobi": ("JOR omega=" + std::to_string(omega));
title += ")";
iterationExport.reset(new ExportIterations(title.c_str()));
iterationExport->exportVector(soln, n, 0);
}
// get setup time
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
@ -264,7 +276,10 @@ jdouble omega // omega (over-relaxation parameter)
// set vector element
soln2[i] = d;
}
if (iterationExport)
iterationExport->exportVector(soln2, n, 0);
// check convergence
sup_norm = 0.0;
for (i = 0; i < n; i++) {

13
prism/src/sparse/PS_NondetReachReward.cc

@ -37,6 +37,8 @@
#include "PrismNativeGlob.h"
#include "PrismSparseGlob.h"
#include "jnipointer.h"
#include "ExportIterations.h"
#include <memory>
#include <new>
//------------------------------------------------------------------------------
@ -214,6 +216,12 @@ jboolean min // min or max probabilities (true = min, false = max)
soln[i] = (inf_vec[i] > 0) ? HUGE_VAL : 0.0;
}
std::unique_ptr<ExportIterations> iterationExport;
if (PS_GetFlagExportIterations()) {
iterationExport.reset(new ExportIterations("PS_NondetReachReward"));
iterationExport->exportVector(soln, n, 0);
}
// get setup time
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
@ -310,7 +318,10 @@ jboolean min // min or max probabilities (true = min, false = max)
// (if there were no choices from this state, reward is zero/infinity)
soln2[i] = (h1 > l1) ? d1 : inf_vec[i] > 0 ? HUGE_VAL : 0;
}
if (iterationExport)
iterationExport->exportVector(soln2, n, 0);
// check convergence
sup_norm = 0.0;
for (i = 0; i < n; i++) {

15
prism/src/sparse/PS_NondetUntil.cc

@ -37,7 +37,9 @@
#include "PrismNativeGlob.h"
#include "PrismSparseGlob.h"
#include "jnipointer.h"
#include "ExportIterations.h"
#include <new>
#include <memory>
//------------------------------------------------------------------------------
@ -198,7 +200,13 @@ jlong _strat // strategy storage
soln[i] = yes_vec[i];
// if (soln[i]) printf("yes[%d] := %f;\n", i+1, yes[i]);
}
std::unique_ptr<ExportIterations> iterationExport;
if (PS_GetFlagExportIterations()) {
iterationExport.reset(new ExportIterations("PS_NondetUntil"));
iterationExport->exportVector(soln, n, 0);
}
// get setup time
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
@ -270,7 +278,10 @@ jlong _strat // strategy storage
// (if no choices, use value of yes)
soln2[i] = (h1 > l1) ? d1 : yes_vec[i];
}
if (iterationExport)
iterationExport->exportVector(soln2, n, 0);
// check convergence
sup_norm = 0.0;
for (i = 0; i < n; i++) {

15
prism/src/sparse/PS_Power.cc

@ -36,6 +36,8 @@
#include "PrismSparseGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include "ExportIterations.h"
#include <memory>
#include <new>
//------------------------------------------------------------------------------
@ -148,7 +150,13 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?)
// print total memory usage
PS_PrintMemoryToMainLog(env, "TOTAL: [", kbt, "]\n");
std::unique_ptr<ExportIterations> iterationExport;
if (PS_GetFlagExportIterations()) {
iterationExport.reset(new ExportIterations("PS_Power"));
iterationExport->exportVector(soln, n, 0);
}
// get setup time
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
@ -210,7 +218,10 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?)
// set vector element
soln2[i] = d;
}
if (iterationExport)
iterationExport->exportVector(soln2, n, 0);
// check convergence
sup_norm = 0.0;
for (i = 0; i < n; i++) {

19
prism/src/sparse/PS_SOR.cc

@ -36,6 +36,8 @@
#include "PrismSparseGlob.h"
#include "jnipointer.h"
#include "prism.h"
#include "ExportIterations.h"
#include <memory>
#include <new>
//------------------------------------------------------------------------------
@ -196,7 +198,17 @@ jboolean forwards // forwards or backwards?
// print total memory usage
PS_PrintMemoryToMainLog(env, "TOTAL: [", kbt, "]\n");
std::unique_ptr<ExportIterations> iterationExport;
if (PS_GetFlagExportIterations()) {
std::string title("PS_SOR (");
title += forwards?"":"Backwards ";
title += (omega == 1.0)?"Gauss-Seidel":("SOR omega=" + std::to_string(omega));
title += ")";
iterationExport.reset(new ExportIterations(title.c_str()));
iterationExport->exportVector(soln, n, 0);
}
// get setup time
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
@ -278,7 +290,10 @@ jboolean forwards // forwards or backwards?
// set vector element
soln[i] = d;
}
if (iterationExport)
iterationExport->exportVector(soln, n, 0);
// check convergence
if (sup_norm < term_crit_param) {
done = true;

Loading…
Cancel
Save