CLI: Added an option to export the produced scheduler to a file.

src/storm-cli-utilities/model-handling.h

@@ -748,10 +748,14 @@ namespace storm {
         template <typename ValueType>
         void verifyWithSparseEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
             auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
+            auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
             verifyProperties<ValueType>(input,
-                                        [&sparseModel] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+                                        [&sparseModel,&ioSettings] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
                                             bool filterForInitialStates = states->isInitialFormula();
                                             auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+                                            if (ioSettings.isExportSchedulerSet()) {
+                                                task.setProduceSchedulers(true);
+                                            }
                                             std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, task);
                                             
                                             std::unique_ptr<storm::modelchecker::CheckResult> filter;
@@ -764,6 +768,17 @@ namespace storm {
                                                 result->filter(filter->asQualitativeCheckResult());
                                             }
                                             return result;
+                                        },
+                                        [&sparseModel,&ioSettings] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
+                                            if (ioSettings.isExportSchedulerSet()) {
+                                                if (result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler()) {
+                                                    auto const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
+                                                    STORM_PRINT_AND_LOG("Exporting scheduler to '" << ioSettings.getExportSchedulerFilename())
+                                                    storm::api::exportScheduler(sparseModel, scheduler, ioSettings.getExportSchedulerFilename());
+                                                } else {
+                                                    STORM_LOG_ERROR("Scheduler requested but could not be generated.");
+                                                }
+                                            }
                                         });
         }
         

src/storm/api/export.h

@@ -6,6 +6,7 @@
 #include "storm/utility/DDEncodingExporter.h"
 #include "storm/utility/file.h"
 #include "storm/utility/macros.h"
+#include "storm/storage/Scheduler.h"
 
 namespace storm {
     
@@ -42,5 +43,14 @@ namespace storm {
         void exportSymbolicModelAsDot(std::shared_ptr<storm::models::symbolic::Model<Type,ValueType>> const& model, std::string const& filename) {
             model->writeDotToFile(filename);
         }
+        
+        template <typename ValueType>
+        void exportScheduler(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::storage::Scheduler<ValueType> const& scheduler, std::string const& filename) {
+            std::ofstream stream;
+            storm::utility::openFile(filename, stream);
+            scheduler.printToStream(stream, model);
+            storm::utility::closeFile(stream);
+        }
+        
     }
 }

src/storm/settings/modules/IOSettings.cpp

@@ -23,6 +23,7 @@ namespace storm {
             const std::string IOSettings::exportJaniDotOptionName = "exportjanidot";
             const std::string IOSettings::exportCdfOptionName = "exportcdf";
             const std::string IOSettings::exportCdfOptionShortName = "cdf";
+            const std::string IOSettings::exportSchedulerOptionName = "exportscheduler";
             const std::string IOSettings::explicitOptionName = "explicit";
             const std::string IOSettings::explicitOptionShortName = "exp";
             const std::string IOSettings::explicitDrnOptionName = "explicit-drn";
@@ -55,6 +56,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.").setIsAdvanced()
                                         .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, 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.")
@@ -148,6 +150,14 @@ namespace storm {
                 return result;
             }
             
+            bool IOSettings::isExportSchedulerSet() const {
+                return this->getOption(exportSchedulerOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string IOSettings::getExportSchedulerFilename() const {
+                return this->getOption(exportSchedulerOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
             bool IOSettings::isExplicitSet() const {
                 return this->getOption(explicitOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/IOSettings.h

@@ -89,6 +89,16 @@ namespace storm {
                  */
                  std::string getExportCdfDirectory() const;
                 
+                /*!
+                 * Retrieves whether an optimal scheduler is to be exported
+                 */
+                bool isExportSchedulerSet() const;
+                
+                /*!
+                 * Retrieves a filename to which an optimal scheduler will be exported.
+                 */
+                 std::string getExportSchedulerFilename() const;
+                
                 /*!
                  * Retrieves whether the explicit option was set.
                  *
@@ -325,6 +335,7 @@ namespace storm {
                 static const std::string exportDdOptionName;
                 static const std::string exportCdfOptionName;
                 static const std::string exportCdfOptionShortName;
+                static const std::string exportSchedulerOptionName;
                 static const std::string explicitOptionName;
                 static const std::string explicitOptionShortName;
                 static const std::string explicitDrnOptionName;