From 06e23c9b4f9b287530713a8dc2c0ffb649f81f79 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 21 Jul 2017 11:44:27 +0000 Subject: [PATCH] (export iterations) Hybrid engine: If enabled, export iterations to HTML file git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12075 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/hybrid/PH_JOR.cc | 21 ++++++++++++++++++--- prism/src/hybrid/PH_NondetReachReward.cc | 15 +++++++++++++-- prism/src/hybrid/PH_NondetUntil.cc | 15 +++++++++++++-- prism/src/hybrid/PH_PSOR.cc | 19 +++++++++++++++++-- prism/src/hybrid/PH_Power.cc | 15 +++++++++++++-- prism/src/hybrid/PH_SOR.cc | 19 +++++++++++++++++-- 6 files changed, 91 insertions(+), 13 deletions(-) diff --git a/prism/src/hybrid/PH_JOR.cc b/prism/src/hybrid/PH_JOR.cc index 93de2561..ba9ee266 100644 --- a/prism/src/hybrid/PH_JOR.cc +++ b/prism/src/hybrid/PH_JOR.cc @@ -37,7 +37,9 @@ #include "PrismHybridGlob.h" #include "jnipointer.h" #include "prism.h" +#include "ExportIterations.h" #include +#include // local prototypes static void jor_rec(HDDNode *hdd, int level, int row_offset, int col_offset, bool transpose); @@ -214,7 +216,17 @@ jdouble omega // omega (over-relaxation parameter) // print total memory usage PH_PrintMemoryToMainLog(env, "TOTAL: [", kbt, "]\n"); - + + std::unique_ptr iterationExport; + if (PH_GetFlagExportIterations()) { + std::string title("PH_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; @@ -256,8 +268,11 @@ jdouble omega // omega (over-relaxation parameter) for (i = 0; i < n; i++) { soln2[i] = ((1-omega) * soln[i]) + (omega * soln2[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/hybrid/PH_NondetReachReward.cc b/prism/src/hybrid/PH_NondetReachReward.cc index 58096a0f..af51e475 100644 --- a/prism/src/hybrid/PH_NondetReachReward.cc +++ b/prism/src/hybrid/PH_NondetReachReward.cc @@ -37,7 +37,9 @@ #include "PrismHybridGlob.h" #include "jnipointer.h" #include "prism.h" +#include "ExportIterations.h" #include +#include // local prototypes static void mult_rec(HDDNode *hdd, int level, int row_offset, int col_offset, int code); @@ -203,7 +205,13 @@ jboolean min // min or max probabilities (true = min, false = max) for (i = 0; i < n; i++) { soln[i] = 0; } - + + std::unique_ptr iterationExport; + if (PH_GetFlagExportIterations()) { + iterationExport.reset(new ExportIterations("PH_NondetReachReward")); + iterationExport->exportVector(soln, n, 0); + } + // get setup time stop = util_cpu_time(); time_for_setup = (double)(stop - start2)/1000; @@ -284,7 +292,10 @@ jboolean min // min or max probabilities (true = min, false = max) } else { for (i = 0; i < n; i++) { if(soln2[i] < 0) soln2[i] = 0; soln2[i] += rew_dist->dist[rew_dist->ptrs[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/hybrid/PH_NondetUntil.cc b/prism/src/hybrid/PH_NondetUntil.cc index 7c0409de..ba1b5bdf 100644 --- a/prism/src/hybrid/PH_NondetUntil.cc +++ b/prism/src/hybrid/PH_NondetUntil.cc @@ -37,7 +37,9 @@ #include "PrismHybridGlob.h" #include "jnipointer.h" #include "prism.h" +#include "ExportIterations.h" #include +#include // local prototypes static void mult_rec(HDDNode *hdd, int level, int row_offset, int col_offset); @@ -168,7 +170,13 @@ jboolean min // min or max probabilities (true = min, false = max) } else { for (i = 0; i < n; i++) { soln[i] = yes_dist->dist[yes_dist->ptrs[i]]; } } - + + std::unique_ptr iterationExport; + if (PH_GetFlagExportIterations()) { + iterationExport.reset(new ExportIterations("PH_NondetUntil")); + iterationExport->exportVector(soln, n, 0); + } + // get setup time stop = util_cpu_time(); time_for_setup = (double)(stop - start2)/1000; @@ -235,7 +243,10 @@ jboolean min // min or max probabilities (true = min, false = max) soln2[i] = (!compact_y) ? (yes_vec[i]) : (yes_dist->dist[yes_dist->ptrs[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/hybrid/PH_PSOR.cc b/prism/src/hybrid/PH_PSOR.cc index fb9aaa31..5db4e821 100644 --- a/prism/src/hybrid/PH_PSOR.cc +++ b/prism/src/hybrid/PH_PSOR.cc @@ -37,7 +37,9 @@ #include "hybrid.h" #include "PrismHybridGlob.h" #include "jnipointer.h" +#include "ExportIterations.h" #include +#include // local prototypes static void psor_rec(HDDNode *hdd, int level, int row_offset, int col_offset, bool transpose); @@ -228,7 +230,17 @@ jboolean forwards // forwards or backwards? // print total memory usage PH_PrintMemoryToMainLog(env, "TOTAL: [", kbt, "]\n"); - + + std::unique_ptr iterationExport; + if (PH_GetFlagExportIterations()) { + std::string title("PH_PSOR ("); + title += (omega == 1.0)?"Pseudo Gauss-Seidel": ("Pseudo 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; @@ -326,7 +338,10 @@ jboolean forwards // forwards or backwards? soln[row_offset + i2] = soln2[i2]; } } - + + if (iterationExport) + iterationExport->exportVector(soln, n, 0); + // check convergence if (sup_norm < term_crit_param) { done = true; diff --git a/prism/src/hybrid/PH_Power.cc b/prism/src/hybrid/PH_Power.cc index 42ac719d..b7df7af0 100644 --- a/prism/src/hybrid/PH_Power.cc +++ b/prism/src/hybrid/PH_Power.cc @@ -37,7 +37,9 @@ #include "PrismHybridGlob.h" #include "jnipointer.h" #include "prism.h" +#include "ExportIterations.h" #include +#include // local prototypes static void power_rec(HDDNode *hdd, int level, int row_offset, int col_offset, bool transpose); @@ -164,7 +166,13 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?) // print total memory usage PH_PrintMemoryToMainLog(env, "TOTAL: [", kbt, "]\n"); - + + std::unique_ptr iterationExport; + if (PH_GetFlagExportIterations()) { + iterationExport.reset(new ExportIterations("PH_Power")); + iterationExport->exportVector(soln, n, 0); + } + // get setup time stop = util_cpu_time(); time_for_setup = (double)(stop - start2)/1000; @@ -193,7 +201,10 @@ jboolean transpose // transpose A? (i.e. solve xA=x not Ax=x?) // do matrix vector multiply bit power_rec(hdd, 0, 0, 0, transpose); - + + if (iterationExport) + iterationExport->exportVector(soln2, n, 0); + // check convergence sup_norm = 0.0; for (i = 0; i < n; i++) { diff --git a/prism/src/hybrid/PH_SOR.cc b/prism/src/hybrid/PH_SOR.cc index 49f6cf54..b9663621 100644 --- a/prism/src/hybrid/PH_SOR.cc +++ b/prism/src/hybrid/PH_SOR.cc @@ -38,7 +38,9 @@ #include "PrismHybridGlob.h" #include "jnipointer.h" #include "prism.h" +#include "ExportIterations.h" #include +#include // local prototypes static void sor_rec(HDDNode *hdd, int level, int row_offset, int col_offset, int r, int c, bool transpose); @@ -237,7 +239,17 @@ jboolean fwds // forwards or backwards? // print total memory usage PH_PrintMemoryToMainLog(env, "TOTAL: [", kbt, "]\n"); - + + std::unique_ptr iterationExport; + if (PH_GetFlagExportIterations()) { + std::string title("PH_SOR ("); + 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; @@ -364,7 +376,10 @@ jboolean fwds // forwards or backwards? soln[row_offset] = soln2[0]; } } - + + if (iterationExport) + iterationExport->exportVector(soln, n, 0); + // check convergence if (sup_norm < term_crit_param) { done = true;