(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

@@ -37,7 +37,9 @@
 #include "PrismHybridGlob.h"
 #include "jnipointer.h"
 #include "prism.h"
+#include "ExportIterations.h"
 #include <new>
+#include <memory>
 
 // 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<ExportIterations> 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++) {

prism/src/hybrid/PH_NondetReachReward.cc

@@ -37,7 +37,9 @@
 #include "PrismHybridGlob.h"
 #include "jnipointer.h"
 #include "prism.h"
+#include "ExportIterations.h"
 #include <new>
+#include <memory>
 
 // 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<ExportIterations> 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++) {

prism/src/hybrid/PH_NondetUntil.cc

@@ -37,7 +37,9 @@
 #include "PrismHybridGlob.h"
 #include "jnipointer.h"
 #include "prism.h"
+#include "ExportIterations.h"
 #include <new>
+#include <memory>
 
 // 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<ExportIterations> 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++) {

prism/src/hybrid/PH_PSOR.cc

@@ -37,7 +37,9 @@
 #include "hybrid.h"
 #include "PrismHybridGlob.h"
 #include "jnipointer.h"
+#include "ExportIterations.h"
 #include <new>
+#include <memory>
 
 // 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<ExportIterations> 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;

prism/src/hybrid/PH_Power.cc

@@ -37,7 +37,9 @@
 #include "PrismHybridGlob.h"
 #include "jnipointer.h"
 #include "prism.h"
+#include "ExportIterations.h"
 #include <new>
+#include <memory>
 
 // 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<ExportIterations> 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++) {

prism/src/hybrid/PH_SOR.cc

@@ -38,7 +38,9 @@
 #include "PrismHybridGlob.h"
 #include "jnipointer.h"
 #include "prism.h"
+#include "ExportIterations.h"
 #include <new>
+#include <memory>
 
 // 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<ExportIterations> 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;