diff --git a/CHANGELOG.md b/CHANGELOG.md
index 149861c2e..2c11fea31 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,6 +8,7 @@ The releases of major and minor versions contain an overview of changes since th
Version 1.5.x
-------------
## Version 1.5.x (Under development)
+- Scheduler export: Properly handle models with end components. Added export in .json format.
- CMake: Search for Gurobi prefers new versions
- Tests: Enabled tests for permissive schedulers
diff --git a/src/storm/api/export.h b/src/storm/api/export.h
index 97859520c..792319f31 100644
--- a/src/storm/api/export.h
+++ b/src/storm/api/export.h
@@ -48,7 +48,12 @@ namespace storm {
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);
+ std::string jsonFileExtension = ".json";
+ if (filename.size() > 4 && std::equal(jsonFileExtension.rbegin(), jsonFileExtension.rend(), filename.rbegin())) {
+ scheduler.printJsonToStream(stream, model);
+ } else {
+ 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 7da94b94e..e2ecdf14b 100644
--- a/src/storm/settings/modules/IOSettings.cpp
+++ b/src/storm/settings/modules/IOSettings.cpp
@@ -59,7 +59,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, false, "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, 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. Use file extension '.json' to export in json.").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());
diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp
index fa40732c6..673a64173 100644
--- a/src/storm/storage/Scheduler.cpp
+++ b/src/storm/storage/Scheduler.cpp
@@ -1,7 +1,8 @@
-#include <storm/utility/vector.h>
+#include "storm/utility/vector.h"
#include "storm/storage/Scheduler.h"
#include "storm/utility/macros.h"
+#include "storm/adapters/JsonAdapter.h"
#include "storm/exceptions/NotImplementedException.h"
#include <boost/algorithm/string/join.hpp>
@@ -222,6 +223,54 @@ namespace storm {
out << "___________________________________________________________________" << std::endl;
}
+ template <>
+ void Scheduler<float>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<float>> model, bool skipUniqueChoices) const {
+ STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers not implemented for this value type.");
+ }
+
+ template <typename ValueType>
+ void Scheduler<ValueType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const {
+ STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler.");
+ STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given.");
+ STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers with memory not implemented.");
+ storm::json<storm::RationalNumber> output;
+ for (uint64_t state = 0; state < schedulerChoices.front().size(); ++state) {
+ // Check whether the state is skipped
+ if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) {
+ continue;
+ }
+ storm::json<storm::RationalNumber> stateChoicesJson;
+ if (model && model->hasStateValuations()) {
+ stateChoicesJson["s"] = model->getStateValuations().getStateValuation(state).toJson();
+ } else {
+ stateChoicesJson["s"] = state;
+ }
+ auto const& choice = schedulerChoices.front()[state];
+ storm::json<storm::RationalNumber> choicesJson;
+ if (choice.isDefined()) {
+ for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
+ uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
+ storm::json<storm::RationalNumber> choiceJson;
+ if (model && model->hasChoiceOrigins() && model->getChoiceOrigins()->getIdentifier(globalChoiceIndex) != model->getChoiceOrigins()->getIdentifierForChoicesWithNoOrigin()) {
+ choiceJson["origin"] = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceIndex);
+ }
+ if (model && model->hasChoiceLabeling()) {
+ auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex);
+ choiceJson["labels"] = std::vector<std::string>(choiceLabels.begin(), choiceLabels.end());
+ }
+ choiceJson["index"] = globalChoiceIndex;
+ choiceJson["prob"] = storm::utility::convertNumber<storm::RationalNumber>(choiceProbPair.second);
+ choicesJson.push_back(std::move(choiceJson));
+ }
+ } else {
+ choicesJson = "undefined";
+ }
+ stateChoicesJson["c"] = std::move(choicesJson);
+ output.push_back(std::move(stateChoicesJson));
+ }
+ out << output.dump(4);
+ }
+
template class Scheduler<double>;
template class Scheduler<float>;
template class Scheduler<storm::RationalNumber>;
diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h
index c6aa30b32..492a7a2f3 100644
--- a/src/storm/storage/Scheduler.h
+++ b/src/storm/storage/Scheduler.h
@@ -111,7 +111,12 @@ namespace storm {
*/
void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const;
-
+
+ /*!
+ * Prints the scheduler in json format to the given output stream.
+ */
+ void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const;
+
private:
boost::optional<storm::storage::MemoryStructure> memoryStructure;