From b308f4e1d08d4edb841c3c157f2dd4bd6cfb05c3 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Fri, 26 Jul 2019 11:47:40 +0200
Subject: [PATCH] Initialize region before creating sample points

---
 .../analysis/MonotonicityChecker.cpp          | 54 ++++++++++---------
 1 file changed, 28 insertions(+), 26 deletions(-)

diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp
index 47bc27b69..6c3518acf 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.cpp
+++ b/src/storm-pars/analysis/MonotonicityChecker.cpp
@@ -29,26 +29,10 @@ namespace storm {
             this->formulas = formulas;
             this->validate = validate;
             this->precision = precision;
-
-            if (numberOfSamples > 0) {
-                // sampling
-                if (model->isOfType(storm::models::ModelType::Dtmc)) {
-                    this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(
-                            checkOnSamples(model->as<storm::models::sparse::Dtmc<ValueType>>(), numberOfSamples));
-                } else if (model->isOfType(storm::models::ModelType::Mdp)) {
-                    this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(
-                            checkOnSamples(model->as<storm::models::sparse::Mdp<ValueType>>(), numberOfSamples));
-
-                }
-                checkSamples= true;
-            } else {
-                checkSamples= false;
-            }
-
             std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
 
             if (regions.size() == 1) {
-                region = *(regions.begin());
+                this->region = *(regions.begin());
             } else {
                 assert (regions.size() == 0);
                 typename storm::storage::ParameterRegion<ValueType>::Valuation lowerBoundaries;
@@ -61,7 +45,22 @@ namespace storm {
                     lowerBoundaries.insert(std::make_pair(var, lb));
                     upperBoundaries.insert(std::make_pair(var, ub));
                 }
-                region =  storm::storage::ParameterRegion<ValueType>(std::move(lowerBoundaries), std::move(upperBoundaries));
+                this->region =  storm::storage::ParameterRegion<ValueType>(std::move(lowerBoundaries), std::move(upperBoundaries));
+            }
+
+            if (numberOfSamples > 0) {
+                // sampling
+                if (model->isOfType(storm::models::ModelType::Dtmc)) {
+                    this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(
+                            checkOnSamples(model->as<storm::models::sparse::Dtmc<ValueType>>(), numberOfSamples));
+                } else if (model->isOfType(storm::models::ModelType::Mdp)) {
+                    this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(
+                            checkOnSamples(model->as<storm::models::sparse::Mdp<ValueType>>(), numberOfSamples));
+
+                }
+                checkSamples= true;
+            } else {
+                checkSamples= false;
             }
 
             this->extender = new storm::analysis::OrderExtender<ValueType>(sparseModel);
@@ -561,17 +560,20 @@ namespace storm {
                     for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) {
                         // Only change value for current variable
                         if ((*itr) == (*itr2)) {
-                            auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>(
-                                    (*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(
-                                            boost::lexical_cast<std::string>((i + 1) / (double(numberOfSamples + 1)))));
+                            auto lb = region.getLowerBoundary(itr->name());
+                            auto ub = region.getUpperBoundary(itr->name());
+                            // Creates samples between lb and ub, that is: lb, lb + (ub-lb)/(#samples -1), lb + 2* (ub-lb)/(#samples -1), ..., ub
+                            auto val =
+                                    std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>
+                                            (*itr,utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(lb + i*(ub-lb)/(numberOfSamples-1)));
                             valuation.insert(val);
-                            assert (0 < val.second && val.second < 1);
+
                         } else {
-                            auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>(
-                                    (*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(
-                                            boost::lexical_cast<std::string>((1) / (double(numberOfSamples + 1)))));
+                            auto lb = region.getLowerBoundary(itr->name());
+                            auto val =
+                                    std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>
+                                            (*itr,utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(lb));
                             valuation.insert(val);
-                            assert (0 < val.second && val.second < 1);
                         }
                     }
                     storm::models::sparse::Dtmc<double> sampleModel = instantiator.instantiate(valuation);