Write output monotonicity checking to user-specified file

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<ValueType> monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(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);

src/storm-pars/analysis/MonotonicityChecker.cpp

@@ -67,19 +67,18 @@ namespace storm {
         }
 
         template <typename ValueType>
-        std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity() {
+        std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::ostream& outfile) {
             auto map = createOrder();
             std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
             auto matrix = sparseModel->getTransitionMatrix();
-            return checkMonotonicity(map, matrix);
+            return checkMonotonicity(outfile, map, matrix);
         }
 
         template <typename ValueType>
-        std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
+        std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::ostream& outfile, std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
             storm::utility::Stopwatch monotonicityCheckWatch(true);
             std::map<storm::analysis::Order *, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> 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;
         }
 

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<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> checkMonotonicity();
+            std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> 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<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> checkMonotonicity(std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
+            std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> checkMonotonicity(std::ostream& outfile, std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
 
             std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, Order* order, storm::storage::SparseMatrix<ValueType> matrix) ;
 
@@ -141,10 +141,6 @@ namespace storm {
 
             OrderExtender<ValueType> *extender;
 
-            std::ofstream outfile;
-
-            std::string filename = "monotonicity.txt";
-
             double precision;
 
             storm::storage::ParameterRegion<ValueType> region;

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();

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;

src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp

@@ -149,7 +149,7 @@ std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions =
     ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull);
 
     storm::analysis::MonotonicityChecker<storm::RationalFunction> monotonicityChecker = storm::analysis::MonotonicityChecker<storm::RationalFunction>(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<storm::RationalFunction>(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();