Added scheduler export in .json

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
 

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

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

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

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;