sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Finished JSON export for GSPNs

main
Matthias Volk 7 years ago
parent
ea2a56ece7
commit
ca0d76e502
2 changed files with 113 additions and 9 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 86
      src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
  2. 36
      src/storm-gspn/storage/gspn/GspnJsonExporter.h

86
src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
View File

@ -34,15 +34,61 @@ namespace storm {
jsonGspn.push_back(jsonTimedTransition);
}
// Export arcs
std::vector<storm::gspn::Place> places = gspn.getPlaces();
// Export arcs for immediate transitions
for (const auto &transition : gspn.getImmediateTransitions()) {
// Export input arcs
for (auto const& entry : transition.getInputPlaces()) {
storm::gspn::Place place = places.at(entry.first);
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::INPUT);
jsonGspn.push_back(jsonInputArc);
}
// Export inhibitor arcs
for (auto const& entry : transition.getInhibitionPlaces()) {
storm::gspn::Place place = places.at(entry.first);
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::INHIBITOR);
jsonGspn.push_back(jsonInputArc);
}
// Export output arcs
for (auto const& entry : transition.getOutputPlaces()) {
storm::gspn::Place place = places.at(entry.first);
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::OUTPUT);
jsonGspn.push_back(jsonInputArc);
}
}
// Export arcs for timed transitions
for (const auto &transition : gspn.getTimedTransitions()) {
// Export input arcs
for (auto const& entry : transition.getInputPlaces()) {
storm::gspn::Place place = places.at(entry.first);
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::INPUT);
jsonGspn.push_back(jsonInputArc);
}
// Export inhibitor arcs
for (auto const& entry : transition.getInhibitionPlaces()) {
storm::gspn::Place place = places.at(entry.first);
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::INHIBITOR);
jsonGspn.push_back(jsonInputArc);
}
// Export output arcs
for (auto const& entry : transition.getOutputPlaces()) {
storm::gspn::Place place = places.at(entry.first);
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::OUTPUT);
jsonGspn.push_back(jsonInputArc);
}
}
return jsonGspn;
}
modernjson::json GspnJsonExporter::translatePlace(storm::gspn::Place const& place) {
modernjson::json data;
std::stringstream stream;
stream << "p" << place.getID();
data["id"] = stream.str();
data["id"] = toJsonString(place);
data["name"] = place.getName();
data["marking"] = place.getNumberOfInitialTokens();
@ -55,9 +101,7 @@ namespace storm {
modernjson::json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition) {
modernjson::json data;
std::stringstream stream;
stream << "i" << transition.getID();
data["id"] = stream.str();
data["id"] = toJsonString(transition, true);
data["name"] = transition.getName();
data["priority"] = transition.getPriority();
data["weight"] = transition.getWeight();
@ -71,9 +115,7 @@ namespace storm {
modernjson::json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition<double> const& transition) {
modernjson::json data;
std::stringstream stream;
stream << "t" << transition.getID();
data["id"] = stream.str();
data["id"] = toJsonString(transition, false);
data["name"] = transition.getName();
data["rate"] = transition.getRate();
data["priority"] = transition.getPriority();
@ -85,5 +127,31 @@ namespace storm {
return jsonTrans;
}
modernjson::json GspnJsonExporter::translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype) {
modernjson::json data;
data["id"] = toJsonString(transition, place, arctype);
data["source"] = toJsonString(place);
data["target"] = toJsonString(transition, immediate);
data["mult"] = multiplicity;
modernjson::json jsonArc;
jsonArc["data"] = data;
//jsonTrans["group"] = "nodes";
switch (arctype) {
case INPUT:
jsonArc["classes"] = "input";
break;
case OUTPUT:
jsonArc["classes"] = "output";
break;
case INHIBITOR:
jsonArc["classes"] = "inhibit";
break;
default:
STORM_LOG_ASSERT(false, "Unknown type " << arctype << " used.");
}
return jsonArc;
}
}
}

36
src/storm-gspn/storage/gspn/GspnJsonExporter.h
View File

@ -24,11 +24,47 @@ namespace storm {
static modernjson::json translate(storm::gspn::GSPN const& gspn);
private:
enum ArcType { INPUT, OUTPUT, INHIBITOR };
static modernjson::json translatePlace(storm::gspn::Place const& place);
static modernjson::json translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition);
static modernjson::json translateTimedTransition(storm::gspn::TimedTransition<double> const& transition);
static modernjson::json translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype);
std::string static inline toJsonString(storm::gspn::Place const& place) {
std::stringstream stream;
stream << "p" << place.getID();
return stream.str();
}
std::string static inline toJsonString(storm::gspn::Transition const& transition, bool immediate) {
std::stringstream stream;
stream << (immediate ? "i" : "t") << transition.getID();
return stream.str();
}
std::string static inline toJsonString(storm::gspn::Transition const& transition, storm::gspn::Place const& place, ArcType arctype) {
std::stringstream stream;
stream << place.getID();
switch (arctype) {
case INPUT:
stream << "i";
break;
case OUTPUT:
stream << "o";
break;
case INHIBITOR:
stream << "h";
break;
default:
STORM_LOG_ASSERT(false, "Unknown type " << arctype << " used.");
}
stream << transition.getID();
return stream.str();
}
};
}

Write Preview
Loading…
Cancel
Save