From 72425ec1b2f3da16ff7c7fd3cc3f5d404495f17c Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 31 Jul 2019 18:45:01 +0200
Subject: [PATCH] CLI: Added an option to export the produced scheduler to a
file.
---
src/storm-cli-utilities/model-handling.h | 17 ++++++++++++++++-
src/storm/api/export.h | 10 ++++++++++
src/storm/settings/modules/IOSettings.cpp | 10 ++++++++++
src/storm/settings/modules/IOSettings.h | 11 +++++++++++
4 files changed, 47 insertions(+), 1 deletion(-)
diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 155707f10..fd88471c5 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/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.");
+ }
+ }
});
}
diff --git a/src/storm/api/export.h b/src/storm/api/export.h
index f1342ef5a..f3064b538 100644
--- a/src/storm/api/export.h
+++ b/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);
+ }
+
}
}
diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp
index 43bf02306..04c7d4256 100644
--- a/src/storm/settings/modules/IOSettings.cpp
+++ b/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();
}
diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h
index e4ff6adf2..96b419b67 100644
--- a/src/storm/settings/modules/IOSettings.h
+++ b/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;