Memory Optimization

TAPAAL · Aug 15, 2024 · a07df2f · a07df2f
1 parent 1964250
commit a07df2f
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 11 deletions.
diff --git a/include/Core/VerificationOptions.hpp b/include/Core/VerificationOptions.hpp
@@ -303,6 +303,7 @@ namespace VerifyTAPN {
         unsigned int cumulativeRoundingDigits = 2;
         unsigned int stepsStatsScale = 0;
         unsigned int timeStatsScale = 0;
+        bool timeStdDev = false;
         unsigned int smcTraces = 0;
         SMCTracesToSave smcTracesToSave = ANY_TRACE;
         friend class ArgsParser;

diff --git a/include/DiscreteVerification/VerificationTypes/ProbabilityEstimation.hpp b/include/DiscreteVerification/VerificationTypes/ProbabilityEstimation.hpp
@@ -45,7 +45,8 @@ class ProbabilityEstimation : public SMCVerification {
         unsigned long validRunsSteps = 0;
 
         std::vector<int> validPerStep;
-        std::vector<double> validPerDelay;
+        std::vector<float> validPerDelay;
+        float maxValidDuration = 0.0f;
 
 };
 

diff --git a/src/Core/ArgsParser.cpp b/src/Core/ArgsParser.cpp
@@ -174,7 +174,7 @@ namespace VerifyTAPN {
             ("strategy-output", po::value<std::string>(), "File to write synthesized strategy to, use '_' (an underscore) for stdout")
             ("smc-benchmark", po::value<unsigned int>(), "Benchmark mode for SMC, runs the number of runs specified to estimate performance")
             ("smc-parallel", po::bool_switch()->default_value(false), "Enable parallel verification for SMC.")
-            ("smc-print-cumulative-stats", po::value<unsigned int>(), "Prints the cumulative probability stats for SMC quantitative estimation")
+            ("smc-print-cumulative-stats", po::value<unsigned int>(), "Prints the cumulative probability stats for SMC quantitative estimation, specifying the rounding precision")
             ("smc-steps-scale", po::value<unsigned int>(), "Specify the number of slices to use to print steps cumulative stats (scale = 0 means every step)")
             ("smc-time-scale", po::value<unsigned int>(), "Specify the number of slices to use to print time cumulative stats (scale = 0 means every 1 unit)")
             ("smc-traces", po::value<unsigned int>(), "Specify the number of SMC run traces to print (default : 0)")

diff --git a/src/DiscreteVerification/VerificationTypes/ProbabilityEstimation.cpp b/src/DiscreteVerification/VerificationTypes/ProbabilityEstimation.cpp
@@ -34,6 +34,7 @@ void ProbabilityEstimation::handleRunResult(const bool res, int steps, double de
     }
     validPerStep[steps] += 1;
     validPerDelay.push_back(delay);
+    if(delay > maxValidDuration) maxValidDuration = delay;
 }
 
 bool ProbabilityEstimation::handleSuccessor(RealMarking* marking) {
@@ -102,23 +103,26 @@ void ProbabilityEstimation::printCumulativeStats() {
         }
         acc += validPerStep[i] / (double) numberOfRuns;    
     }
-    std::cout << std::endl << "  cumulative probability / delay :" << std::endl;
-    std::sort(validPerDelay.begin(), validPerDelay.end());
+    std::cout << (validPerStep.size() - 1) << ":" << getEstimation() << ";" << std::endl;
+    std::cout << "  cumulative probability / delay :" << std::endl;
     acc = 0;
-    binSize = timeScale == 0 ? 1 : validPerDelay.back() / (double) timeScale;
-    bin = 0;
+    binSize = timeScale == 0 ? 1 : maxValidDuration / (double) timeScale;
+    std::vector<double> bins(round(maxValidDuration / binSize), 0);
     lastAcc = -1;
     for(int i = 0 ; i < validPerDelay.size() ; i++) {
         double delay = validPerDelay[i];
+        int binIndex = (int) round(delay / binSize);
+        bins[binIndex] += 1;
+    }
+    for(int i = 0 ; i < bins.size() ; i++) {
+        acc += bins[i] / (double) numberOfRuns;
         double toPrint = round(acc * mult) / mult;
-        if((delay >= bin + binSize || i == (validPerDelay.size() - 1)) && toPrint != lastAcc) {
-            bin += binSize;
-            std::cout << bin << ":" << toPrint << ";";
+        if(toPrint != lastAcc) {
+            std::cout << ((i + 1) * binSize) << ":" << toPrint << ";";
             lastAcc = toPrint;
         }
-        acc += 1 / (double) numberOfRuns;
     }
-    std::cout << std::endl;
+    std::cout << maxValidDuration << ":" << getEstimation() << ";" << std::endl;
 }
 
 void ProbabilityEstimation::printResult() {