From feebf1a24d18481de9cfae6dda6aa377620d88ed Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 10 Apr 2020 16:52:28 +0200 Subject: [PATCH] Added scheduler export in .json --- CHANGELOG.md | 1 + src/storm/api/export.h | 7 +++- src/storm/settings/modules/IOSettings.cpp | 2 +- src/storm/storage/Scheduler.cpp | 51 ++++++++++++++++++++++- src/storm/storage/Scheduler.h | 7 +++- 5 files changed, 64 insertions(+), 4 deletions(-) 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> const& model, storm::storage::Scheduler 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 +#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 @@ -222,6 +223,54 @@ namespace storm { out << "___________________________________________________________________" << std::endl; } + template <> + void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers not implemented for this value type."); + } + + template + void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> 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 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 stateChoicesJson; + if (model && model->hasStateValuations()) { + stateChoicesJson["s"] = model->getStateValuations().getStateValuation(state).toJson(); + } else { + stateChoicesJson["s"] = state; + } + auto const& choice = schedulerChoices.front()[state]; + storm::json choicesJson; + if (choice.isDefined()) { + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; + storm::json 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(choiceLabels.begin(), choiceLabels.end()); + } + choiceJson["index"] = globalChoiceIndex; + choiceJson["prob"] = storm::utility::convertNumber(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; template class Scheduler; template class Scheduler; 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> 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> model = nullptr, bool skipUniqueChoices = false) const; + private: boost::optional memoryStructure;