Browse Source

do not allow edges with no destinations in jani

tempestpy_adaptions
sjunges 8 years ago
parent
commit
4920eaaaea
  1. 5
      src/storm/storage/jani/JSONExporter.cpp

5
src/storm/storage/jani/JSONExporter.cpp

@ -650,6 +650,7 @@ namespace storm {
} }
modernjson::json buildDestinations(std::vector<EdgeDestination> const& destinations, std::map<uint64_t, std::string> const& locationNames) { modernjson::json buildDestinations(std::vector<EdgeDestination> const& destinations, std::map<uint64_t, std::string> const& locationNames) {
assert(destinations.size() > 0);
std::vector<modernjson::json> destDeclarations; std::vector<modernjson::json> destDeclarations;
for(auto const& destination : destinations) { for(auto const& destination : destinations) {
modernjson::json destEntry; modernjson::json destEntry;
@ -664,6 +665,10 @@ namespace storm {
modernjson::json buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames) { modernjson::json buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames) {
std::vector<modernjson::json> edgeDeclarations; std::vector<modernjson::json> edgeDeclarations;
for(auto const& edge : edges) { 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.");
modernjson::json edgeEntry; modernjson::json edgeEntry;
edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex()); edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex());
if(!edge.hasSilentAction()) { if(!edge.hasSilentAction()) {

Loading…
Cancel
Save