Export of choice origins to json

src/storm/storage/jani/JSONExporter.cpp

@@ -995,12 +995,7 @@ namespace storm {
             return destDeclarations;
         }
         
-        ExportJsonType buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
-            ExportJsonType edgeDeclarations = std::vector<ExportJsonType>();
-            for(auto const& edge : edges) {
-                if (edge.getGuard().isFalse()) {
-                    continue;
-                }
+        ExportJsonType buildEdge(Edge const& edge , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
             STORM_LOG_THROW(edge.getDestinations().size() > 0, storm::exceptions::InvalidJaniException, "An edge without destinations is not allowed.");
             ExportJsonType edgeEntry;
             edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex());
@@ -1023,8 +1018,16 @@ namespace storm {
             if (!edge.getAssignments().empty()) {
                 edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments(), constants, globalVariables, localVariables, commentExpressions);
             }
+            return edgeEntry;
+        }
         
-                edgeDeclarations.push_back(std::move(edgeEntry));
+        ExportJsonType buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
+            ExportJsonType edgeDeclarations = std::vector<ExportJsonType>();
+            for(auto const& edge : edges) {
+                if (edge.getGuard().isFalse()) {
+                    continue;
+                }
+                edgeDeclarations.push_back(buildEdge(edge, actionNames, locationNames, constants, globalVariables, localVariables, commentExpressions));
             }
             return edgeDeclarations;
         }
@@ -1065,6 +1068,11 @@ namespace storm {
             jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition());
         }
         
+        ExportJsonType JsonExporter::getEdgeAsJson(storm::jani::Model const& janiModel, uint64_t automatonIndex, uint64_t edgeIndex, bool commentExpressions) {
+            auto const& automaton = janiModel.getAutomaton(automatonIndex);
+            return buildEdge(automaton.getEdge(edgeIndex), janiModel.getActionIndexToNameMap(), automaton.buildIdToLocationNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), automaton.getVariables(), commentExpressions);
+        }
+        
         std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) {
             switch(ft) {
                 case storm::modelchecker::FilterType::MIN:

src/storm/storage/jani/JSONExporter.h

@@ -89,7 +89,7 @@ namespace storm {
             static void toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid = true, bool compact = false);
             static void toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& ostream, bool checkValid = false, bool compact = false);
             
-            
+            static ExportJsonType getEdgeAsJson(storm::jani::Model const& janiModel, uint64_t automatonIndex, uint64_t edgeIndex, bool commentExpressions = true);
         private:
             void convertModel(storm::jani::Model const& model, bool commentExpressions = true);
             void convertProperties(std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model);

src/storm/storage/sparse/ChoiceOrigins.cpp

@@ -67,6 +67,18 @@ namespace storm {
 				return getIdentifierInfo(getIdentifier(choiceIndex));
 			}
    
+			typename ChoiceOrigins::Json const& ChoiceOrigins::getIdentifierAsJson(uint_fast64_t identifier) const {
+                STORM_LOG_ASSERT(identifier < this->getNumberOfIdentifiers(), "Invalid choice origin identifier: " << identifier);
+                if (identifierToJson.empty()) {
+                    computeIdentifierInfos();
+                }
+				return identifierToJson[identifier];
+            }
+            
+            typename ChoiceOrigins::Json const& ChoiceOrigins::getChoiceAsJson(uint_fast64_t choiceIndex) const {
+                return getIdentifierAsJson(getIdentifier(choiceIndex));
+            }
+            
             std::shared_ptr<ChoiceOrigins> ChoiceOrigins::selectChoices(storm::storage::BitVector const& selectedChoices) const {
                 std::vector<uint_fast64_t> indexToIdentifierMapping(selectedChoices.getNumberOfSetBits());
                 storm::utility::vector::selectVectorValues(indexToIdentifierMapping, selectedChoices, indexToIdentifier);

src/storm/storage/sparse/ChoiceOrigins.h

@@ -5,6 +5,7 @@
 #include "storm/storage/BitVector.h"
 #include "storm/models/sparse/ChoiceLabeling.h"
 
+#include "storm/adapters/JsonAdapter.h"
 
 namespace storm {
     namespace storage {
@@ -19,6 +20,7 @@ namespace storm {
              */
             class ChoiceOrigins {
             public:
+                typedef storm::json<storm::RationalNumber> Json;
                 
                 virtual ~ChoiceOrigins() = default;
                 
@@ -63,6 +65,16 @@ namespace storm {
                  */
                 std::string const& getChoiceInfo(uint_fast64_t choiceIndex) const;
                 
+                /*
+                 * Returns the information for the given choice origin identifier as a (human readable) string
+                 */
+                Json const& getIdentifierAsJson(uint_fast64_t identifier) const;
+                
+                /*
+                 * Returns the choice origin information as a (human readable) string.
+                 */
+                Json const& getChoiceAsJson(uint_fast64_t choiceIndex) const;
+                
                 /*
                  * Derive new choice origins from this by selecting the given choices.
                  */
@@ -95,11 +107,19 @@ namespace storm {
                  */
                 virtual void computeIdentifierInfos() const = 0;
                 
+                /*
+                 * Computes the identifier infos (i.e., human readable strings representing the choice origins).
+                 */
+                virtual void computeIdentifierJson() const = 0;
+                
                 std::vector<uint_fast64_t> indexToIdentifier;
                 
                 // cached identifier infos might be empty if identifiers have not been generated yet.
                 mutable std::vector<std::string> identifierToInfo;
                 
+                // cached identifier infos might be empty if identifiers have not been generated yet.
+                mutable std::vector<Json> identifierToJson;
+
             };
         }
     }

src/storm/storage/sparse/JaniChoiceOrigins.cpp

@@ -1,6 +1,7 @@
 #include "storm/storage/sparse/JaniChoiceOrigins.h"
 
 #include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/JSONExporter.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidArgumentException.h"
@@ -52,6 +53,32 @@ namespace storm {
                 }
             }
             
+            void JaniChoiceOrigins::computeIdentifierJson() const {
+                this->identifierToJson.clear();
+                this->identifierToJson.reserve(this->getNumberOfIdentifiers());
+                for (auto const& set : identifierToEdgeIndexSet) {
+                    Json setJson;
+                    if (set.empty()) {
+                        setJson = "No origin";
+                    } else {
+                        bool first = true;
+                        std::vector<Json> edgesJson;
+                        for (auto const& edgeIndex : set) {
+                            auto autAndEdgeOffset = model->decodeAutomatonAndEdgeIndices(edgeIndex);
+                            auto const& automaton = model->getAutomaton(autAndEdgeOffset.first);
+                            auto const& edge = automaton.getEdge(autAndEdgeOffset.second);
+                            if (first) {
+                                setJson["action-label"] = model->getAction(edge.getActionIndex()).getName();
+                                first = false;
+                            }
+                            edgesJson.push_back(storm::jani::JsonExporter::getEdgeAsJson(*model, autAndEdgeOffset.first, autAndEdgeOffset.second));
+                            edgesJson.back()["automaton"] = automaton.getName();
+                        }
+                        setJson["edges"] = std::move(edgesJson);
+                    }
+                    this->identifierToJson.push_back(std::move(setJson));
+                }
+            }
         }
     }
 }

src/storm/storage/sparse/JaniChoiceOrigins.h

@@ -59,6 +59,11 @@ namespace storm {
                  */
                 virtual void computeIdentifierInfos() const override;
                 
+                /*
+                 * Computes the identifier infos as json (i.e., a machine readable representation of the choice origins).
+                 */
+                virtual void computeIdentifierJson() const override;
+                
                 std::shared_ptr<storm::jani::Model const> model;
                 std::vector<EdgeIndexSet> identifierToEdgeIndexSet;
             };

src/storm/storage/sparse/PrismChoiceOrigins.cpp

@@ -108,6 +108,54 @@ namespace storm {
                 STORM_LOG_DEBUG("Generated the following names for the choice origins: " << storm::utility::vector::toString(this->identifierToInfo));
                 STORM_LOG_ASSERT(storm::utility::vector::isUnique(this->identifierToInfo), "The generated names for the prism choice origins are not unique.");
             }
+            
+            void PrismChoiceOrigins::computeIdentifierJson() const {
+                this->identifierToJson.clear();
+                this->identifierToJson.reserve(this->getNumberOfIdentifiers());
+                for (CommandSet const& set : identifierToCommandSet) {
+                    // Get a string representation of this command set.
+                    Json setJson;
+                    if (set.empty()) {
+                        setJson = "No origin";
+                    } else {
+                        bool first = true;
+                        std::vector<Json> commandsJson;
+                        for (auto const& commandIndex : set) {
+                            Json commandJson;
+                            auto moduleCommandPair = program->getModuleCommandIndexByGlobalCommandIndex(commandIndex);
+                            storm::prism::Module const& module = program->getModule(moduleCommandPair.first);
+                            storm::prism::Command const& command = module.getCommand(moduleCommandPair.second);
+                            if (first) {
+                                setJson["action-label"] = command.getActionName();
+                                first = false;
+                            }
+                            commandJson["module"] = module.getName();
+                            commandJson["guard"] = command.getGuardExpression().toString();
+                            std::vector<Json> updatesJson;
+                            for (auto const& update : command.getUpdates()) {
+                                Json updateJson;
+                                updateJson["prob"] = update.getLikelihoodExpression().toString();
+                                std::stringstream assignmentsString;
+                                bool firstAssignment = true;
+                                for (auto const& a : update.getAssignments()) {
+                                    if (firstAssignment) {
+                                        firstAssignment = false;
+                                    } else {
+                                        assignmentsString << " & ";
+                                    }
+                                    assignmentsString << a;
+                                }
+                                updateJson["result"] = assignmentsString.str();
+                                updatesJson.push_back(std::move(updateJson));
+                            }
+                            commandJson["updates"] = updatesJson;
+                            commandsJson.push_back(std::move(commandJson));
+                        }
+                        setJson["commands"] = commandsJson;
+                    }
+                    this->identifierToJson.push_back(std::move(setJson));
+                }
+            }
         }
     }
 }

src/storm/storage/sparse/PrismChoiceOrigins.h

@@ -62,6 +62,11 @@ namespace storm {
                  */
                 virtual void computeIdentifierInfos() const override;
                 
+                /*
+                 * Computes the identifier infos as json (i.e., a machine readable representation of the choice origins).
+                 */
+                virtual void computeIdentifierJson() const override;
+                
                 std::shared_ptr<storm::prism::Program const> program;
                 std::vector<CommandSet> identifierToCommandSet;
             };