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 - MonotonicityChecker::MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate, uint_fast64_t numberOfSamples) { + MonotonicityChecker::MonotonicityChecker(std::shared_ptr model, std::vector> 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(); 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 model, std::vector> formulas, bool validate, uint_fast64_t numberOfSamples=0); + MonotonicityChecker(std::shared_ptr model, std::vector> 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; }; } }