From a5ebb8b81b5e1cc47643af36df6d39a77c9588d7 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 9 Apr 2020 21:13:54 +0200 Subject: [PATCH] Export of choice origins to json --- src/storm/storage/jani/JSONExporter.cpp | 56 +++++++++++-------- src/storm/storage/jani/JSONExporter.h | 2 +- src/storm/storage/sparse/ChoiceOrigins.cpp | 12 ++++ src/storm/storage/sparse/ChoiceOrigins.h | 20 +++++++ .../storage/sparse/JaniChoiceOrigins.cpp | 27 +++++++++ src/storm/storage/sparse/JaniChoiceOrigins.h | 5 ++ .../storage/sparse/PrismChoiceOrigins.cpp | 48 ++++++++++++++++ src/storm/storage/sparse/PrismChoiceOrigins.h | 5 ++ 8 files changed, 150 insertions(+), 25 deletions(-) diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index e312a7e93..46317c870 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -995,36 +995,39 @@ namespace storm { return destDeclarations; } + ExportJsonType buildEdge(Edge const& edge , std::map const& actionNames, std::map const& locationNames, std::vector 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()); + if (!edge.hasSilentAction()) { + edgeEntry["action"] = actionNames.at(edge.getActionIndex()); + } + if (edge.hasRate()) { + edgeEntry["rate"]["exp"] = buildExpression(edge.getRate(), constants, globalVariables, localVariables); + if (commentExpressions) { + edgeEntry["rate"]["comment"] = edge.getRate().toString(); + } + } + if (!edge.getGuard().isTrue()) { + edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard(), constants, globalVariables, localVariables); + if (commentExpressions) { + edgeEntry["guard"]["comment"] = edge.getGuard().toString(); + } + } + edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames, constants, globalVariables, localVariables, commentExpressions); + if (!edge.getAssignments().empty()) { + edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments(), constants, globalVariables, localVariables, commentExpressions); + } + return edgeEntry; + } + ExportJsonType buildEdges(std::vector const& edges , std::map const& actionNames, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { ExportJsonType edgeDeclarations = std::vector(); for(auto const& edge : edges) { if (edge.getGuard().isFalse()) { continue; } - 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()); - if(!edge.hasSilentAction()) { - edgeEntry["action"] = actionNames.at(edge.getActionIndex()); - } - if(edge.hasRate()) { - edgeEntry["rate"]["exp"] = buildExpression(edge.getRate(), constants, globalVariables, localVariables); - if (commentExpressions) { - edgeEntry["rate"]["comment"] = edge.getRate().toString(); - } - } - if (!edge.getGuard().isTrue()) { - edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard(), constants, globalVariables, localVariables); - if (commentExpressions) { - edgeEntry["guard"]["comment"] = edge.getGuard().toString(); - } - } - edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames, constants, globalVariables, localVariables, commentExpressions); - if (!edge.getAssignments().empty()) { - edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments(), constants, globalVariables, localVariables, commentExpressions); - } - - edgeDeclarations.push_back(std::move(edgeEntry)); + 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: diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index d8ba87489..7c11358c6 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -89,7 +89,7 @@ namespace storm { static void toFile(storm::jani::Model const& janiModel, std::vector const& formulas, std::string const& filepath, bool checkValid = true, bool compact = false); static void toStream(storm::jani::Model const& janiModel, std::vector 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 const& formulas, storm::jani::Model const& model); diff --git a/src/storm/storage/sparse/ChoiceOrigins.cpp b/src/storm/storage/sparse/ChoiceOrigins.cpp index 56c512f37..f0281120c 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.cpp +++ b/src/storm/storage/sparse/ChoiceOrigins.cpp @@ -66,6 +66,18 @@ namespace storm { std::string const& ChoiceOrigins::getChoiceInfo(uint_fast64_t choiceIndex) const { 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::selectChoices(storm::storage::BitVector const& selectedChoices) const { std::vector indexToIdentifierMapping(selectedChoices.getNumberOfSetBits()); diff --git a/src/storm/storage/sparse/ChoiceOrigins.h b/src/storm/storage/sparse/ChoiceOrigins.h index 902fdd031..afc85faf3 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.h +++ b/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 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,10 +107,18 @@ 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 indexToIdentifier; // cached identifier infos might be empty if identifiers have not been generated yet. mutable std::vector identifierToInfo; + + // cached identifier infos might be empty if identifiers have not been generated yet. + mutable std::vector identifierToJson; }; } diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.cpp b/src/storm/storage/sparse/JaniChoiceOrigins.cpp index c4d1c365b..d9314e6a5 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.cpp +++ b/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 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)); + } + } } } } diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.h b/src/storm/storage/sparse/JaniChoiceOrigins.h index 93698a0f0..5ee1aa69b 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.h +++ b/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 model; std::vector identifierToEdgeIndexSet; }; diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.cpp b/src/storm/storage/sparse/PrismChoiceOrigins.cpp index 69084f8cd..0b4c943be 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.cpp +++ b/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 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 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)); + } + } } } } diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.h b/src/storm/storage/sparse/PrismChoiceOrigins.h index 06ff3c584..05567a644 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.h +++ b/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 program; std::vector identifierToCommandSet; };