diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index d58e96b8c..d127ceec3 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -50,8 +50,16 @@ namespace storm { for(auto const& constant : constants) { modernjson::json constantEntry; constantEntry["name"] = constant.getName(); - // TODO add type info - //onstantEntry["type"] = buildType(constant.getType()); + modernjson::json typeDesc; + if(constant.isBooleanConstant()) { + typeDesc = "bool"; + } else if(constant.isRealConstant()) { + typeDesc = "real"; + } else { + assert(constant.isIntegerConstant()); + typeDesc = "int"; + } + constantEntry["type"] = typeDesc; if(constant.isDefined()) { constantEntry["value"] = buildExpression(constant.getExpression()); } @@ -66,7 +74,6 @@ namespace storm { modernjson::json varEntry; varEntry["name"] = variable.getName(); varEntry["transient"] = variable.isTransient(); - // TODO type modernjson::json typeDesc; if(variable.isBooleanVariable()) { typeDesc = "bool"; @@ -127,12 +134,11 @@ namespace storm { return modernjson::json(names); } - modernjson::json buildDestinations(std::vector const& destinations) { + modernjson::json buildDestinations(std::vector const& destinations, std::map const& locationNames) { std::vector destDeclarations; for(auto const& destination : destinations) { modernjson::json destEntry; - // TODO - //destEntry["location"] = + destEntry["location"] = locationNames.at(destination.getLocationIndex()); destEntry["probability"] = buildExpression(destination.getProbability()); // TODO //destEntry["assignments"] = buildAssignmentArray(destination.getAssignments()); @@ -141,28 +147,27 @@ namespace storm { return modernjson::json(destDeclarations); } - modernjson::json buildEdges(storm::jani::Automaton const& automaton) { - std::vector const& edges = automaton.getEdges(); + modernjson::json buildEdges(std::vector const& edges , std::map const& actionNames, std::map const& locationNames) { std::vector edgeDeclarations; for(auto const& edge : edges) { modernjson::json edgeEntry; - edgeEntry["location"] = automaton.getLocation(edge.getSourceLocationIndex()).getName(); - // TODO actions + edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex()); + // TODO silent action //if(edge.nonSilentAction()) { - // edgeEntry["action"] = edge.getActionIndex() + edgeEntry["action"] = actionNames.at(edge.getActionIndex()); //} if(edge.hasRate()) { edgeEntry["rate"]["exp"] = buildExpression(edge.getRate()); } edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard()); - edgeEntry["destinations"] = buildDestinations(edge.getDestinations()); + edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames); edgeDeclarations.push_back(edgeEntry); } return modernjson::json(edgeDeclarations); } - modernjson::json buildAutomataArray(std::vector const& automata) { + modernjson::json buildAutomataArray(std::vector const& automata, std::map const& actionNames) { std::vector automataDeclarations; for(auto const& automaton : automata) { modernjson::json autoEntry; @@ -171,7 +176,7 @@ namespace storm { autoEntry["restrict-initial"]["exp"] = buildExpression(automaton.getInitialStatesRestriction()); autoEntry["locations"] = buildLocationsArray(automaton.getLocations()); autoEntry["initial-locations"] = buildInitialLocations(automaton); - autoEntry["edges"] = buildEdges(automaton); + autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap()); automataDeclarations.push_back(autoEntry); } return modernjson::json(automataDeclarations); @@ -186,7 +191,7 @@ namespace storm { jsonStruct["constants"] = buildConstantsArray(janiModel.getConstants()); jsonStruct["variables"] = buildVariablesArray(janiModel.getGlobalVariables()); jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction()); - jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata()); + jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.buildActionToNameMap()); //jsonStruct["system"] = buildComposition(); }