diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 0105e55ef..42415b81a 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -598,10 +598,6 @@ namespace storm { if (parSettings.isMonotonicityAnalysisSet()) { // Simplify the model storm::utility::Stopwatch simplifyingWatch(true); - std::ofstream outfile; - outfile.open("results.txt", std::ios_base::app); - outfile << ioSettings.getPrismInputFilename() << ", "; - if (model->isOfType(storm::models::ModelType::Dtmc)) { auto consideredModel = (model->as>()); auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*consideredModel); @@ -631,11 +627,9 @@ namespace storm { simplifyingWatch.stop(); STORM_PRINT(std::endl << "Time for model simplification: " << simplifyingWatch << "." << std::endl << std::endl); model->printModelInformationToStream(std::cout); - outfile << simplifyingWatch << ", "; - outfile.close(); } - if (parSettings.isMonotonicityAnalysisSet() && model) { + if (model) { auto preprocessingResult = storm::pars::preprocessModel(model, input); if (preprocessingResult.changed) { model = preprocessingResult.model; @@ -722,20 +716,13 @@ namespace storm { if (parSettings.isMonotonicityAnalysisSet()) { std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); - // Monotonicity - std::ofstream outfile; - outfile.open("results.txt", std::ios_base::app); storm::utility::Stopwatch monotonicityWatch(true); - auto numberOfSamples = parSettings.getNumberOfSamples(); - auto monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, parSettings.isValidateAssumptionsSet(), numberOfSamples); + auto monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, parSettings.isValidateAssumptionsSet(), parSettings.getNumberOfSamples(), parSettings.getMonotonicityAnalysisPrecision()); monotonicityChecker.checkMonotonicity(); monotonicityWatch.stop(); STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl << std::endl); - - outfile << monotonicityWatch << std::endl; - outfile.close(); } std::vector> regions = parseRegions(model); diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index f4e6fbde0..33bc02d63 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -522,11 +522,13 @@ namespace storm { (*itr2), storm::utility::convertNumber::type>( boost::lexical_cast((i + 1) / (double(numberOfSamples + 1))))); valuation.insert(val); + assert (0 < val.second && val.second < 1); } else { auto val = std::pair::type, typename utility::parametric::CoefficientType::type>( (*itr2), storm::utility::convertNumber::type>( boost::lexical_cast((1) / (double(numberOfSamples + 1))))); valuation.insert(val); + assert (0 < val.second && val.second < 1); } } storm::models::sparse::Dtmc sampleModel = instantiator.instantiate(valuation); @@ -551,10 +553,12 @@ namespace storm { std::vector values = quantitativeResult.getValueVector(); auto initialStates = model->getInitialStates(); double initial = 0; - for (auto i = initialStates.getNextSetIndex(0); i < model->getNumberOfStates(); i = initialStates.getNextSetIndex(i+1)) { - initial += values[i]; + for (auto j = initialStates.getNextSetIndex(0); j < model->getNumberOfStates(); j = initialStates.getNextSetIndex(j+1)) { + initial += values[j]; } + assert (initial >= precision && initial <= 1+precision); double diff = previous - initial; + assert (previous == -1 || diff >= -1-precision && diff <= 1 + precision); 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; @@ -625,9 +629,12 @@ namespace storm { for (auto i = initialStates.getNextSetIndex(0); i < model->getNumberOfStates(); i = initialStates.getNextSetIndex(i+1)) { initial += values[i]; } - if (previous != -1) { - monDecr &= previous >= initial; - monIncr &= previous <= initial; + assert (initial >= precision && initial <= 1+precision); + double diff = previous - initial; + assert (previous == -1 || diff >= -1-precision && diff <= 1 + precision); + 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/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index e0c8c3bee..75d31566e 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/src/storm-pars/settings/modules/ParametricSettings.cpp @@ -25,6 +25,7 @@ namespace storm { const std::string ParametricSettings::sccElimination = "mon-elim-scc"; const std::string ParametricSettings::validateAssumptions = "mon-validate-assumptions"; const std::string ParametricSettings::samplesMonotonicityAnalysis = "mon-samples"; + const std::string ParametricSettings::precision = "mon-precision"; ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.") @@ -41,6 +42,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").build()); this->addOption(storm::settings::OptionBuilder(moduleName, samplesMonotonicityAnalysis, false, "Sets whether monotonicity should be checked on samples") .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mon-samples", "The number of samples taken in monotonicity-analysis can be given, default is 0, no samples").setDefaultValueUnsignedInteger(0).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precision, false, "Sets precision of monotonicity checking on samples") + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("mon-precision", "The precision of checking monotonicity on samples, default is 1e-6").setDefaultValueDouble(0.000001).build()).build()); } @@ -91,6 +94,10 @@ namespace storm { uint_fast64_t ParametricSettings::getNumberOfSamples() const { return this->getOption(samplesMonotonicityAnalysis).getArgumentByName("mon-samples").getValueAsUnsignedInteger(); } + + double ParametricSettings::getMonotonicityAnalysisPrecision() const { + return this->getOption(precision).getArgumentByName("mon-precision").getValueAsDouble(); + } } // namespace modules } // namespace settings } // namespace storm diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index cbb740ec6..60e8fe067 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -84,6 +84,11 @@ namespace storm { */ uint_fast64_t getNumberOfSamples() const; + /*! + * Retrieves the precision for the extremal value + */ + double getMonotonicityAnalysisPrecision() const; + const static std::string moduleName; private: @@ -99,6 +104,7 @@ namespace storm { const static std::string sccElimination; const static std::string validateAssumptions; const static std::string samplesMonotonicityAnalysis; + const static std::string precision; }; } // namespace modules