diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 75dba4492..de8542e25 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -744,7 +744,14 @@ namespace storm { STORM_LOG_THROW(regions.size() <= 1, storm::exceptions::InvalidArgumentException, "Monotonicity analysis only allowed on single region"); storm::analysis::MonotonicityChecker monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, regions, monSettings.isValidateAssumptionsSet(), monSettings.getNumberOfSamples(), monSettings.getMonotonicityAnalysisPrecision()); - monotonicityChecker.checkMonotonicity(); + if (ioSettings.isExportMonotonicitySet()) { + std::ofstream outfile; + utility::openFile(ioSettings.getExportMonotonicityFilename(), outfile); + monotonicityChecker.checkMonotonicity(outfile); + utility::closeFile(outfile); + } else { + monotonicityChecker.checkMonotonicity(std::cout); + } monotonicityWatch.stop(); STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl << std::endl); diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index c53609220..f8ba84c7e 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -67,19 +67,18 @@ namespace storm { } template - std::map::type, std::pair>> MonotonicityChecker::checkMonotonicity() { + std::map::type, std::pair>> MonotonicityChecker::checkMonotonicity(std::ostream& outfile) { auto map = createOrder(); std::shared_ptr> sparseModel = model->as>(); auto matrix = sparseModel->getTransitionMatrix(); - return checkMonotonicity(map, matrix); + return checkMonotonicity(outfile, map, matrix); } template - std::map::type, std::pair>> MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix) { + std::map::type, std::pair>> MonotonicityChecker::checkMonotonicity(std::ostream& outfile, std::map>> map, storm::storage::SparseMatrix matrix) { storm::utility::Stopwatch monotonicityCheckWatch(true); std::map::type, std::pair>> result; - outfile.open(filename, std::ios_base::app); if (map.size() == 0) { // Nothing is known @@ -166,7 +165,6 @@ namespace storm { outfile << ", "; monotonicityCheckWatch.stop(); - outfile.close(); return result; } diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index 5d32ecf70..31fc0e193 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -41,7 +41,7 @@ namespace storm { /*! * Checks for model and formula as provided in constructor for monotonicity */ - std::map::type, std::pair>> checkMonotonicity(); + std::map::type, std::pair>> checkMonotonicity(std::ostream& outfile); /*! * Checks if monotonicity can be found in this order. Unordered states are not checked @@ -113,7 +113,7 @@ namespace storm { } private: - std::map::type, std::pair>> checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); + std::map::type, std::pair>> checkMonotonicity(std::ostream& outfile, std::map>> map, storm::storage::SparseMatrix matrix); std::map::type, std::pair> analyseMonotonicity(uint_fast64_t i, Order* order, storm::storage::SparseMatrix matrix) ; @@ -141,10 +141,6 @@ namespace storm { OrderExtender *extender; - std::ofstream outfile; - - std::string filename = "monotonicity.txt"; - double precision; storm::storage::ParameterRegion region; diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 86866e7e6..7f78e93cb 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -25,6 +25,7 @@ namespace storm { const std::string IOSettings::exportCdfOptionName = "exportcdf"; const std::string IOSettings::exportCdfOptionShortName = "cdf"; const std::string IOSettings::exportSchedulerOptionName = "exportscheduler"; + const std::string IOSettings::exportMonotonicityName = "exportmonotonicity"; const std::string IOSettings::explicitOptionName = "explicit"; const std::string IOSettings::explicitOptionShortName = "exp"; const std::string IOSettings::explicitDrnOptionName = "explicit-drn"; @@ -59,6 +60,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportSchedulerOptionName, false, "Exports the choices of an optimal scheduler to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportMonotonicityName, false, "Exports the result of monotonicity checking to the given file.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportDdOptionName, "", "If given, the loaded model will be written to the specified file in the drdd format.") @@ -162,6 +164,14 @@ namespace storm { std::string IOSettings::getExportSchedulerFilename() const { return this->getOption(exportSchedulerOptionName).getArgumentByName("filename").getValueAsString(); } + + bool IOSettings::isExportMonotonicitySet() const { + return this->getOption(exportMonotonicityName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExportMonotonicityFilename() const { + return this->getOption(exportMonotonicityName).getArgumentByName("filename").getValueAsString(); + } bool IOSettings::isExplicitSet() const { return this->getOption(explicitOptionName).getHasOptionBeenSet(); diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 91cc3b765..2cbdf65bf 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -105,6 +105,16 @@ namespace storm { * Retrieves a filename to which an optimal scheduler will be exported. */ std::string getExportSchedulerFilename() const; + + /*! + * Retrieves whether an optimal scheduler is to be exported + */ + bool isExportMonotonicitySet() const; + + /*! + * Retrieves a filename to which an optimal scheduler will be exported. + */ + std::string getExportMonotonicityFilename() const; /*! * Retrieves whether the explicit option was set. @@ -339,6 +349,7 @@ namespace storm { static const std::string exportCdfOptionName; static const std::string exportCdfOptionShortName; static const std::string exportSchedulerOptionName; + static const std::string exportMonotonicityName; static const std::string explicitOptionName; static const std::string explicitOptionShortName; static const std::string explicitDrnOptionName; diff --git a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp index 0eda2d56d..14973cfc2 100644 --- a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp @@ -149,7 +149,7 @@ std::vector> regions = ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); storm::analysis::MonotonicityChecker monotonicityChecker = storm::analysis::MonotonicityChecker(dtmc, formulas, regions, true); - auto result = monotonicityChecker.checkMonotonicity(); + auto result = monotonicityChecker.checkMonotonicity(std::cout); EXPECT_EQ(1ul, result.size()); EXPECT_EQ(2ul, result.begin()->second.size()); auto monotone = result.begin()->second.begin(); @@ -197,7 +197,7 @@ TEST(MonotonicityCheckerTest, Brp_with_bisimulation_samples) { ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); auto monotonicityChecker = storm::analysis::MonotonicityChecker(dtmc, formulas, regions, true, 50); - auto result = monotonicityChecker.checkMonotonicity(); + auto result = monotonicityChecker.checkMonotonicity(std::cout); EXPECT_EQ(1ul, result.size()); EXPECT_EQ(2ul, result.begin()->second.size()); auto monotone = result.begin()->second.begin();