Use precision in sample checking monotonicity

src/storm-pars/analysis/MonotonicityChecker.cpp

@@ -23,11 +23,12 @@
 namespace storm {
     namespace analysis {
         template <typename ValueType>
-        MonotonicityChecker<ValueType>::MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, bool validate, uint_fast64_t numberOfSamples) {
+        MonotonicityChecker<ValueType>::MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, bool validate, uint_fast64_t numberOfSamples, double const& precision) {
             assert (model != nullptr);
             this->model = model;
             this->formulas = formulas;
             this->validate = validate;
+            this->precision = precision;
 
             if (numberOfSamples > 0) {
                 // sampling
@@ -512,7 +513,7 @@ namespace storm {
                 bool monDecr = true;
                 bool monIncr = true;
 
-                for (auto i = 0; i < numberOfSamples; ++i) {
+                for (auto i = 0; (monDecr || monIncr) && i < numberOfSamples; ++i) {
                     auto valuation = storm::utility::parametric::Valuation<ValueType>();
                     for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) {
                         // Only change value for current variable
@@ -553,11 +554,10 @@ namespace storm {
                     for (auto i = initialStates.getNextSetIndex(0); i < model->getNumberOfStates(); i = initialStates.getNextSetIndex(i+1)) {
                         initial += values[i];
                     }
-                    float diff = previous - initial;
-                    // TODO: define precision
-                    if (previous != -1 && diff > 0.000005 && diff < -0.000005) {
-                        monDecr &= previous >= initial;
-                        monIncr &= previous <= initial;
+                    double diff = previous - initial;
+                    if (previous != -1 && (diff > precision || diff < -precision)) {
+                        monDecr &= diff > precision; // then previous value is larger than the current value from the initial states
+                        monIncr &= diff < -precision;
                     }
                     previous = initial;
                 }

src/storm-pars/analysis/MonotonicityChecker.h

@@ -33,8 +33,9 @@ namespace storm {
              * @param validate whether or not assumptions are to be validated
              * @param numberOfSamples number of samples taken for monotonicity checking, default 0,
              *          if 0then no check on samples is executed
+             * @param precision precision on which the samples are compared
              */
-            MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, bool validate, uint_fast64_t numberOfSamples=0);
+            MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, bool validate, uint_fast64_t numberOfSamples=0, double const& precision=0.000001);
 
             /*!
              * Checks for model and formula as provided in constructor for monotonicity
@@ -141,6 +142,8 @@ namespace storm {
             std::ofstream outfile;
 
             std::string filename = "monotonicity.txt";
+
+            double precision;
         };
     }
 }