From 7bc6ce99fa27906512791ad3f02cf2ddc27fef8c Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 12 Feb 2017 17:21:55 +0100 Subject: [PATCH] JANI Export now preserves variable names correctly --- src/storm/storage/jani/JSONExporter.cpp | 83 ++++++++++++++----------- src/storm/storage/jani/JSONExporter.h | 8 ++- 2 files changed, 53 insertions(+), 38 deletions(-) diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 5231a1506..edde5cc59 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -30,8 +30,12 @@ namespace storm { namespace jani { - - + + + modernjson::json buildExpression(storm::expressions::Expression const& exp, std::vector const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet()) { + return ExpressionToJson::translate(exp, constants, globalVariables, localVariables); + } + class CompositionJsonExporter : public CompositionVisitor { public: CompositionJsonExporter(bool allowRecursion) : allowRecursion(allowRecursion){ @@ -145,7 +149,7 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const&) const { - return ExpressionToJson::translate(f.getExpression()); + return buildExpression(f.getExpression(), model.getConstants(), model.getGlobalVariables()); } boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const&) const { @@ -450,8 +454,8 @@ namespace storm { } } - modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr) { - ExpressionToJson visitor; + modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) { + ExpressionToJson visitor(constants, globalVariables, localVariables); return boost::any_cast(expr.accept(visitor, boost::none)); } @@ -486,7 +490,18 @@ namespace storm { return opDecl; } boost::any ExpressionToJson::visit(storm::expressions::VariableExpression const& expression, boost::any const&) { - return modernjson::json(expression.getVariableName()); + if (globalVariables.hasVariable(expression.getVariable())) { + return modernjson::json(globalVariables.getVariable(expression.getVariable()).getName()); + } else if (localVariables.hasVariable(expression.getVariable())) { + return modernjson::json(localVariables.getVariable(expression.getVariable()).getName()); + } else { + for (auto const& constant : constants) { + if (constant.getExpressionVariable() == expression.getVariable()) { + return modernjson::json(constant.getName()); + } + } + } + STORM_LOG_ASSERT(false, "Expression variable '" << expression.getVariableName() << "' not known in Jani data structures."); } boost::any ExpressionToJson::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) { modernjson::json opDecl; @@ -554,11 +569,7 @@ namespace storm { } - - modernjson::json buildExpression(storm::expressions::Expression const& exp) { - return ExpressionToJson::translate(exp); - } - + modernjson::json buildConstantsArray(std::vector const& constants) { std::vector constantDeclarations; @@ -576,14 +587,14 @@ namespace storm { } constantEntry["type"] = typeDesc; if(constant.isDefined()) { - constantEntry["value"] = buildExpression(constant.getExpression()); + constantEntry["value"] = buildExpression(constant.getExpression(), constants); } constantDeclarations.push_back(constantEntry); } return modernjson::json(constantDeclarations); } - modernjson::json buildVariablesArray(storm::jani::VariableSet const& varSet) { + modernjson::json buildVariablesArray(storm::jani::VariableSet const& varSet, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) { std::vector variableDeclarations; for(auto const& variable : varSet) { modernjson::json varEntry; @@ -602,13 +613,13 @@ namespace storm { assert(variable.isBoundedIntegerVariable()); typeDesc["kind"] = "bounded"; typeDesc["base"] = "int"; - typeDesc["lower-bound"] = buildExpression(variable.asBoundedIntegerVariable().getLowerBound()); - typeDesc["upper-bound"] = buildExpression(variable.asBoundedIntegerVariable().getUpperBound()); + typeDesc["lower-bound"] = buildExpression(variable.asBoundedIntegerVariable().getLowerBound(), constants, globalVariables, localVariables); + typeDesc["upper-bound"] = buildExpression(variable.asBoundedIntegerVariable().getUpperBound(), constants, globalVariables, localVariables); } varEntry["type"] = typeDesc; if(variable.hasInitExpression()) { - varEntry["initial-value"] = buildExpression(variable.getInitExpression()); + varEntry["initial-value"] = buildExpression(variable.getInitExpression(), constants, globalVariables, localVariables); } variableDeclarations.push_back(varEntry); } @@ -616,13 +627,13 @@ namespace storm { } - modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments) { + modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) { std::vector assignmentDeclarations; bool addIndex = orderedAssignments.hasMultipleLevels(); for(auto const& assignment : orderedAssignments) { modernjson::json assignmentEntry; assignmentEntry["ref"] = assignment.getVariable().getName(); - assignmentEntry["value"] = buildExpression(assignment.getAssignedExpression()); + assignmentEntry["value"] = buildExpression(assignment.getAssignedExpression(), constants, globalVariables, localVariables); if(addIndex) { assignmentEntry["index"] = assignment.getLevel(); } @@ -631,14 +642,14 @@ namespace storm { return modernjson::json(assignmentDeclarations); } - modernjson::json buildLocationsArray(std::vector const& locations) { + modernjson::json buildLocationsArray(std::vector const& locations, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) { std::vector locationDeclarations; for(auto const& location : locations) { modernjson::json locEntry; locEntry["name"] = location.getName(); // TODO support invariants? if (!location.getAssignments().empty()) { - locEntry["transient-values"] = buildAssignmentArray(location.getAssignments()); + locEntry["transient-values"] = buildAssignmentArray(location.getAssignments(), constants, globalVariables, localVariables); } locationDeclarations.push_back(locEntry); } @@ -653,7 +664,7 @@ namespace storm { return modernjson::json(names); } - modernjson::json buildDestinations(std::vector const& destinations, std::map const& locationNames) { + modernjson::json buildDestinations(std::vector const& destinations, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) { assert(destinations.size() > 0); std::vector destDeclarations; for(auto const& destination : destinations) { @@ -666,17 +677,17 @@ namespace storm { } } if (!prob1) { - destEntry["probability"]["exp"] = buildExpression(destination.getProbability()); + destEntry["probability"]["exp"] = buildExpression(destination.getProbability(), constants, globalVariables, localVariables); } if (!destination.getOrderedAssignments().empty()) { - destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments()); + destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments(), constants, globalVariables, localVariables); } destDeclarations.push_back(destEntry); } return modernjson::json(destDeclarations); } - modernjson::json buildEdges(std::vector const& edges , std::map const& actionNames, std::map const& locationNames) { + modernjson::json buildEdges(std::vector const& edges , std::map const& actionNames, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) { std::vector edgeDeclarations; for(auto const& edge : edges) { if (edge.getGuard().isFalse()) { @@ -689,14 +700,14 @@ namespace storm { edgeEntry["action"] = actionNames.at(edge.getActionIndex()); } if(edge.hasRate()) { - edgeEntry["rate"]["exp"] = buildExpression(edge.getRate()); + edgeEntry["rate"]["exp"] = buildExpression(edge.getRate(), constants, globalVariables, localVariables); } if (!edge.getGuard().isTrue()) { - edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard()); + edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard(), constants, globalVariables, localVariables); } - edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames); + edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames, constants, globalVariables, localVariables); if (!edge.getAssignments().empty()) { - edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments()); + edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments(), constants, globalVariables, localVariables); } edgeDeclarations.push_back(edgeEntry); @@ -704,18 +715,18 @@ namespace storm { return modernjson::json(edgeDeclarations); } - modernjson::json buildAutomataArray(std::vector const& automata, std::map const& actionNames) { + modernjson::json buildAutomataArray(std::vector const& automata, std::map const& actionNames, std::vector const& constants, VariableSet const& globalVariables) { std::vector automataDeclarations; for(auto const& automaton : automata) { modernjson::json autoEntry; autoEntry["name"] = automaton.getName(); - autoEntry["variables"] = buildVariablesArray(automaton.getVariables()); + autoEntry["variables"] = buildVariablesArray(automaton.getVariables(), constants, globalVariables, automaton.getVariables()); if(automaton.hasRestrictedInitialStates()) { - autoEntry["restrict-initial"]["exp"] = buildExpression(automaton.getInitialStatesRestriction()); + autoEntry["restrict-initial"]["exp"] = buildExpression(automaton.getInitialStatesRestriction(), constants, globalVariables, automaton.getVariables()); } - autoEntry["locations"] = buildLocationsArray(automaton.getLocations()); + autoEntry["locations"] = buildLocationsArray(automaton.getLocations(), constants, globalVariables, automaton.getVariables()); autoEntry["initial-locations"] = buildInitialLocations(automaton); - autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap()); + autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap(), constants, globalVariables, automaton.getVariables()); automataDeclarations.push_back(autoEntry); } return modernjson::json(automataDeclarations); @@ -728,9 +739,9 @@ namespace storm { jsonStruct["type"] = to_string(janiModel.getModelType()); jsonStruct["actions"] = buildActionArray(janiModel.getActions()); jsonStruct["constants"] = buildConstantsArray(janiModel.getConstants()); - jsonStruct["variables"] = buildVariablesArray(janiModel.getGlobalVariables()); - jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction()); - jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap()); + jsonStruct["variables"] = buildVariablesArray(janiModel.getGlobalVariables(), janiModel.getConstants(), janiModel.getGlobalVariables()); + jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction(), janiModel.getConstants(), janiModel.getGlobalVariables()); + jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables()); jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition()); std::vector standardFeatureVector = {"derived-operators"}; jsonStruct["features"] = standardFeatureVector; diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index 1eceb5d2e..ca26c08e6 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -18,7 +18,7 @@ namespace storm { class ExpressionToJson : public storm::expressions::ExpressionVisitor { public: - static modernjson::json translate(storm::expressions::Expression const& expr); + static modernjson::json translate(storm::expressions::Expression const& expr, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables); virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data); virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data); @@ -30,7 +30,11 @@ namespace storm { virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data); virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data); virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data); - + private: + ExpressionToJson(std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) : constants(constants), globalVariables(globalVariables), localVariables(localVariables) {} + std::vector const& constants; + VariableSet const& globalVariables; + VariableSet const& localVariables; }; class FormulaToJaniJson : public storm::logic::FormulaVisitor {