diff --git a/include/Core/VerificationOptions.hpp b/include/Core/VerificationOptions.hpp index ae11266f..0316298e 100755 --- 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 index 3386007b..3f6a3e37 100644 --- 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 validPerStep; - std::vector validPerDelay; + std::vector validPerDelay; + float maxValidDuration = 0.0f; }; diff --git a/src/Core/ArgsParser.cpp b/src/Core/ArgsParser.cpp index 03f74eed..9e7765b9 100755 --- a/src/Core/ArgsParser.cpp +++ b/src/Core/ArgsParser.cpp @@ -174,7 +174,7 @@ namespace VerifyTAPN { ("strategy-output", po::value(), "File to write synthesized strategy to, use '_' (an underscore) for stdout") ("smc-benchmark", po::value(), "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(), "Prints the cumulative probability stats for SMC quantitative estimation") + ("smc-print-cumulative-stats", po::value(), "Prints the cumulative probability stats for SMC quantitative estimation, specifying the rounding precision") ("smc-steps-scale", po::value(), "Specify the number of slices to use to print steps cumulative stats (scale = 0 means every step)") ("smc-time-scale", po::value(), "Specify the number of slices to use to print time cumulative stats (scale = 0 means every 1 unit)") ("smc-traces", po::value(), "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 index f34664f5..28d7e312 100644 --- 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 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() {