From 3c2a2232e159c4846c2f8aac1ea6e55f0c4e9d08 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 21 Jul 2017 11:44:12 +0000 Subject: [PATCH] (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 --- prism/src/sparse/PS_JOR.cc | 19 +++++++++++++++++-- prism/src/sparse/PS_NondetReachReward.cc | 13 ++++++++++++- prism/src/sparse/PS_NondetUntil.cc | 15 +++++++++++++-- prism/src/sparse/PS_Power.cc | 15 +++++++++++++-- prism/src/sparse/PS_SOR.cc | 19 +++++++++++++++++-- 5 files changed, 72 insertions(+), 9 deletions(-) diff --git a/prism/src/sparse/PS_JOR.cc b/prism/src/sparse/PS_JOR.cc index 0bf2567b..a02b8b5e 100644 --- a/prism/src/sparse/PS_JOR.cc +++ b/prism/src/sparse/PS_JOR.cc @@ -36,6 +36,8 @@ #include "PrismSparseGlob.h" #include "jnipointer.h" #include "prism.h" +#include "ExportIterations.h" +#include #include //------------------------------------------------------------------------------ @@ -196,7 +198,17 @@ jdouble omega // omega (over-relaxation parameter) // print total memory usage PS_PrintMemoryToMainLog(env, "TOTAL: [", kbt, "]\n"); - + + std::unique_ptr 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++) { diff --git a/prism/src/sparse/PS_NondetReachReward.cc b/prism/src/sparse/PS_NondetReachReward.cc index cca80bd4..db2cf467 100644 --- a/prism/src/sparse/PS_NondetReachReward.cc +++ b/prism/src/sparse/PS_NondetReachReward.cc @@ -37,6 +37,8 @@ #include "PrismNativeGlob.h" #include "PrismSparseGlob.h" #include "jnipointer.h" +#include "ExportIterations.h" +#include #include //------------------------------------------------------------------------------ @@ -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 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++) { diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index b9ba4eb5..957a8258 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/prism/src/sparse/PS_NondetUntil.cc @@ -37,7 +37,9 @@ #include "PrismNativeGlob.h" #include "PrismSparseGlob.h" #include "jnipointer.h" +#include "ExportIterations.h" #include +#include //------------------------------------------------------------------------------ @@ -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 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++) { diff --git a/prism/src/sparse/PS_Power.cc b/prism/src/sparse/PS_Power.cc index dfce25ff..352d2203 100644 --- a/prism/src/sparse/PS_Power.cc +++ b/prism/src/sparse/PS_Power.cc @@ -36,6 +36,8 @@ #include "PrismSparseGlob.h" #include "jnipointer.h" #include "prism.h" +#include "ExportIterations.h" +#include #include //------------------------------------------------------------------------------ @@ -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 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++) { diff --git a/prism/src/sparse/PS_SOR.cc b/prism/src/sparse/PS_SOR.cc index bbb3a806..a0d7fe76 100644 --- a/prism/src/sparse/PS_SOR.cc +++ b/prism/src/sparse/PS_SOR.cc @@ -36,6 +36,8 @@ #include "PrismSparseGlob.h" #include "jnipointer.h" #include "prism.h" +#include "ExportIterations.h" +#include #include //------------------------------------------------------------------------------ @@ -196,7 +198,17 @@ jboolean forwards // forwards or backwards? // print total memory usage PS_PrintMemoryToMainLog(env, "TOTAL: [", kbt, "]\n"); - + + std::unique_ptr 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;