SMC Numeric Precision

TAPAAL · Sep 6, 2024 · abf1bc9 · abf1bc9
1 parent c3720c5
commit abf1bc9
Show file tree

Hide file tree

Showing 7 changed files with 38 additions and 16 deletions.
diff --git a/include/Core/TAPN/StochasticStructure.hpp b/include/Core/TAPN/StochasticStructure.hpp
@@ -69,7 +69,7 @@ namespace VerifyTAPN::SMC {
         DistributionParameters parameters;
 
         template<typename T>
-        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
@@ -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
@@ -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<RealMarking*> _trace;

diff --git a/include/DiscreteVerification/VerificationTypes/SMCVerification.hpp b/include/DiscreteVerification/VerificationTypes/SMCVerification.hpp
@@ -17,7 +17,7 @@ class SMCVerification : public Verification<RealMarking> {
         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
@@ -181,7 +181,8 @@ namespace VerifyTAPN {
             ("smc-traces-type", po::value<unsigned int>(), "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<unsigned int>(), "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<unsigned int>());
+        }
+
         std::vector<std::string> 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
@@ -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<double>::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
@@ -1,11 +1,19 @@
 #include "DiscreteVerification/VerificationTypes/SMCVerification.hpp"
 
 #include <thread>
-
+#include <sstream>
 #include <chrono>
+#include <iomanip>
 
 #define STEP_MS 5000
 
+std::string printDouble(double value, unsigned int precision) {
+    std::ostringstream oss;
+    if(precision == 0) precision = std::numeric_limits<double>::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);