From abf1bc98d8964ce2486a43df3649eb9d5d2c37af Mon Sep 17 00:00:00 2001 From: TanguyDubois Date: Fri, 6 Sep 2024 13:47:36 +0200 Subject: [PATCH] SMC Numeric Precision --- include/Core/TAPN/StochasticStructure.hpp | 7 +++++-- include/Core/VerificationOptions.hpp | 9 +++++++++ .../Generators/SMCRunGenerator.h | 5 ++++- .../VerificationTypes/SMCVerification.hpp | 2 +- src/Core/ArgsParser.cpp | 7 ++++++- .../Generators/SMCRunGenerator.cpp | 12 +++--------- .../VerificationTypes/SMCVerification.cpp | 12 ++++++++++-- 7 files changed, 38 insertions(+), 16 deletions(-) diff --git a/include/Core/TAPN/StochasticStructure.hpp b/include/Core/TAPN/StochasticStructure.hpp index 1acbde02..a0519a68 100644 --- a/include/Core/TAPN/StochasticStructure.hpp +++ b/include/Core/TAPN/StochasticStructure.hpp @@ -69,7 +69,7 @@ namespace VerifyTAPN::SMC { DistributionParameters parameters; template - double sample(T& engine) const { + double sample(T& engine, const unsigned int precision = 0) const { double date = 0; switch(type) { case Constant: @@ -95,7 +95,10 @@ namespace VerifyTAPN::SMC { date = std::geometric_distribution(parameters.geometric.p)(engine); break; } - date = round(date * 100000) / 100000; + if(precision > 0) { + double factor = pow(10.0, precision); + date = round(date * factor) / factor; + } return std::max(date, 0.0); } diff --git a/include/Core/VerificationOptions.hpp b/include/Core/VerificationOptions.hpp index 214f8b81..719a03a6 100755 --- a/include/Core/VerificationOptions.hpp +++ b/include/Core/VerificationOptions.hpp @@ -275,6 +275,14 @@ namespace VerifyTAPN { smcTracesType = toSave; } + inline void setSMCNumericPrecision(const unsigned int precision) { + smcNumericPrecision = precision; + } + + inline unsigned int getSMCNumericPrecision() const { + return smcNumericPrecision; + } + protected: std::string inputFile; std::string queryFile; @@ -306,6 +314,7 @@ namespace VerifyTAPN { bool timeStdDev = false; unsigned int smcTraces = 0; SMCTracesType smcTracesType = ANY_TRACE; + unsigned int smcNumericPrecision = 5; friend class ArgsParser; }; diff --git a/include/DiscreteVerification/Generators/SMCRunGenerator.h b/include/DiscreteVerification/Generators/SMCRunGenerator.h index ee3b611d..cd52c230 100644 --- a/include/DiscreteVerification/Generators/SMCRunGenerator.h +++ b/include/DiscreteVerification/Generators/SMCRunGenerator.h @@ -23,10 +23,11 @@ namespace VerifyTAPN { public: - SMCRunGenerator(TAPN::TimedArcPetriNet &tapn) + SMCRunGenerator(TAPN::TimedArcPetriNet &tapn, const unsigned int numericPrecision = 0) : _tapn(tapn) , _defaultTransitionIntervals(tapn.getTransitions().size()) , _transitionsStatistics(tapn.getTransitions().size(), 0) + , _numericPrecision(numericPrecision) { /*std::random_device rd; _rng = std::ranlux48(rd());*/ @@ -92,6 +93,8 @@ namespace VerifyTAPN { double _totalTime = 0; int _totalSteps = 0; + unsigned int _numericPrecision = 0; + boost::random::mt19937_64 _rng; std::vector _trace; diff --git a/include/DiscreteVerification/VerificationTypes/SMCVerification.hpp b/include/DiscreteVerification/VerificationTypes/SMCVerification.hpp index 29bf6f3b..9dbe880c 100644 --- a/include/DiscreteVerification/VerificationTypes/SMCVerification.hpp +++ b/include/DiscreteVerification/VerificationTypes/SMCVerification.hpp @@ -17,7 +17,7 @@ class SMCVerification : public Verification { SMCVerification(TAPN::TimedArcPetriNet &tapn, RealMarking &initialMarking, AST::SMCQuery *query, VerificationOptions options) : Verification(tapn, initialMarking, query, options) - , runGenerator(tapn) + , runGenerator(tapn, options.getSMCNumericPrecision()) , numberOfRuns(0), maxTokensSeen(0), smcSettings(query->getSmcSettings()) { } diff --git a/src/Core/ArgsParser.cpp b/src/Core/ArgsParser.cpp index 70d5ffcd..03a2f060 100755 --- a/src/Core/ArgsParser.cpp +++ b/src/Core/ArgsParser.cpp @@ -181,7 +181,8 @@ namespace VerifyTAPN { ("smc-traces-type", po::value(), "Specify the desired SMC runs to save.\n" " 0: any (default)\n" " 1: only runs satisfying the property\n" - " 2: only runs not satisfying the property"); + " 2: only runs not satisfying the property") + ("smc-numeric-precision", po::value(), "Specify the number of rounding digits to use in SMC verifications (default = 5, 0 means no rounding)."); } @@ -296,6 +297,10 @@ namespace VerifyTAPN { ); } + if(vm.count("smc-numeric-precision")) { + opts.setSMCNumericPrecision(vm["smc-numeric-precision"].as()); + } + std::vector files = po::collect_unrecognized(parsed.options, po::include_positional); // remove everything that is just a space diff --git a/src/DiscreteVerification/Generators/SMCRunGenerator.cpp b/src/DiscreteVerification/Generators/SMCRunGenerator.cpp index 6869b390..e8f20e64 100644 --- a/src/DiscreteVerification/Generators/SMCRunGenerator.cpp +++ b/src/DiscreteVerification/Generators/SMCRunGenerator.cpp @@ -57,7 +57,7 @@ namespace VerifyTAPN { auto* intervals = &_transitionIntervals[i]; if(!intervals->empty() && intervals->front().lower() == 0) { const Distribution& distrib = _tapn.getTransitions()[i]->getDistribution(); - _dates_sampled[i] = distrib.sample(_rng); + _dates_sampled[i] = distrib.sample(_rng, _numericPrecision); } deadlocked &= _transitionIntervals[i].empty() || ( @@ -73,6 +73,7 @@ namespace VerifyTAPN { { SMCRunGenerator clone(_tapn); clone._origin = new RealMarking(*_origin); + clone._numericPrecision = _numericPrecision; clone._defaultTransitionIntervals = _defaultTransitionIntervals; clone.recordTrace = recordTrace; clone.reset(); @@ -99,7 +100,7 @@ namespace VerifyTAPN { _dates_sampled[i] = std::numeric_limits::infinity(); } else if(newlyEnabled) { const Distribution& distrib = _tapn.getTransitions()[i]->getDistribution(); - double date = distrib.sample(_rng); + double date = distrib.sample(_rng, _numericPrecision); if(_transitionIntervals[i].front().upper() > 0 || date == 0) { _dates_sampled[i] = date; } @@ -162,13 +163,6 @@ namespace VerifyTAPN { refreshTransitionsIntervals(); - /*for(auto& transi : _tapn.getTransitions()) { - std::cout << transi->getName() << std::endl; - for(auto& interv : _transitionIntervals[transi->getIndex()]) { - std::cout << interv.lower() << ";" << interv.upper() << std::endl; - } - }*/ - return _parent; } diff --git a/src/DiscreteVerification/VerificationTypes/SMCVerification.cpp b/src/DiscreteVerification/VerificationTypes/SMCVerification.cpp index 140f3a9b..dc5400b5 100644 --- a/src/DiscreteVerification/VerificationTypes/SMCVerification.cpp +++ b/src/DiscreteVerification/VerificationTypes/SMCVerification.cpp @@ -1,11 +1,19 @@ #include "DiscreteVerification/VerificationTypes/SMCVerification.hpp" #include - +#include #include +#include #define STEP_MS 5000 +std::string printDouble(double value, unsigned int precision) { + std::ostringstream oss; + if(precision == 0) precision = std::numeric_limits::max_digits10; + oss << std::fixed << std::setprecision(precision) << value; + return oss.str(); +} + namespace VerifyTAPN::DiscreteVerification { bool SMCVerification::parallel_run() { @@ -292,7 +300,7 @@ SMCVerification::createTokenNode(rapidxml::xml_document<> &doc, const TAPN::Time xml_attribute<> *placeAttribute = doc.allocate_attribute("place", doc.allocate_string(place.getName().c_str())); tokenNode->append_attribute(placeAttribute); - auto str = std::to_string(token.getAge() * tapn.getGCD()); + auto str = printDouble(token.getAge(), options.getSMCNumericPrecision()); xml_attribute<> *ageAttribute = doc.allocate_attribute("age", doc.allocate_string( str.c_str())); tokenNode->append_attribute(ageAttribute);