From 1557f6d2131e8e77e7c52ffd45bb50347663ede4 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Wed, 15 May 2019 15:31:00 +0200
Subject: [PATCH] Use precision in sample checking monotonicity

---
 src/storm-pars/analysis/MonotonicityChecker.cpp | 14 +++++++-------
 src/storm-pars/analysis/MonotonicityChecker.h   |  5 ++++-
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp
index 972585535..f4e6fbde0 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.cpp
+++ b/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;
                 }
diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h
index 66a2d3869..5d6b60ba4 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.h
+++ b/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;
         };
     }
 }