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

Small changes

main
Matthias Volk 7 years ago
parent
e4e467622f
commit
096d532aa0
5 changed files with 78 additions and 27 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 23
      src/storm-dft/transformations/DftToGspnTransformator.cpp
  2. 9
      src/storm-gspn/storage/gspn/GSPN.cpp
  3. 3
      src/storm-gspn/storage/gspn/GSPN.h
  4. 58
      src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
  5. 6
      src/storm-gspn/storage/gspn/GspnJsonExporter.h

23
src/storm-dft/transformations/DftToGspnTransformator.cpp
View File

@ -99,7 +99,6 @@ namespace storm {
builder.setPlaceLayoutInfo(beActive, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter)); builder.setPlaceLayoutInfo(beActive, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter));
builder.setPlaceLayoutInfo(beFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter)); builder.setPlaceLayoutInfo(beFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter));
uint64_t disabledNode = 0; uint64_t disabledNode = 0;
if (!smart || dftBE->nrRestrictions() > 0) { if (!smart || dftBE->nrRestrictions() > 0) {
disabledNode = addDisabledPlace(dftBE); disabledNode = addDisabledPlace(dftBE);
@ -146,7 +145,7 @@ namespace storm {
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
uint64_t unavailableNode = 0; uint64_t unavailableNode = 0;
if (isRepresentative) {
if (!smart || isRepresentative) {
unavailableNode = addUnavailableNode(dftAnd, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); unavailableNode = addUnavailableNode(dftAnd, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
} }
@ -155,7 +154,7 @@ namespace storm {
builder.setTransitionLayoutInfo(tAndFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0)); builder.setTransitionLayoutInfo(tAndFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0));
builder.addInhibitionArc(nodeFailed, tAndFailed); builder.addInhibitionArc(nodeFailed, tAndFailed);
builder.addOutputArc(tAndFailed, nodeFailed); builder.addOutputArc(tAndFailed, nodeFailed);
if (isRepresentative) {
if (!smart || isRepresentative) {
builder.addOutputArc(tAndFailed, unavailableNode); builder.addOutputArc(tAndFailed, unavailableNode);
} }
for (auto const& child : dftAnd->children()) { for (auto const& child : dftAnd->children()) {
@ -176,7 +175,7 @@ namespace storm {
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
uint64_t unavailableNode = 0; uint64_t unavailableNode = 0;
if (isRepresentative) {
if (!smart || isRepresentative) {
unavailableNode = addUnavailableNode(dftOr, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); unavailableNode = addUnavailableNode(dftOr, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
} }
@ -186,7 +185,7 @@ namespace storm {
builder.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0)); builder.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0));
builder.addInhibitionArc(nodeFailed, tNodeFailed); builder.addInhibitionArc(nodeFailed, tNodeFailed);
builder.addOutputArc(tNodeFailed, nodeFailed); builder.addOutputArc(tNodeFailed, nodeFailed);
if (isRepresentative) {
if (!smart || isRepresentative) {
builder.addOutputArc(tNodeFailed, unavailableNode); builder.addOutputArc(tNodeFailed, unavailableNode);
} }
assert(failedNodes.size() > child->id()); assert(failedNodes.size() > child->id());
@ -265,10 +264,12 @@ namespace storm {
builder.setPlaceLayoutInfo(nodeFS, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0)); builder.setPlaceLayoutInfo(nodeFS, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0));
builder.addInhibitionArc(nodeFS, tNodeFailed); builder.addInhibitionArc(nodeFS, tNodeFailed);
// Transition for failed
for (auto const& child : dftPand->children()) { for (auto const& child : dftPand->children()) {
builder.addInputArc(failedNodes[child->id()], tNodeFailed); builder.addInputArc(failedNodes[child->id()], tNodeFailed);
builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); builder.addOutputArc(tNodeFailed, failedNodes[child->id()]);
} }
// Transitions for fail-safe
for (uint64_t j = 1; j < dftPand->nrChildren(); ++j) { for (uint64_t j = 1; j < dftPand->nrChildren(); ++j) {
uint64_t tfs = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(j)); uint64_t tfs = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(j));
builder.setTransitionLayoutInfo(tfs, storm::gspn::LayoutInfo(xcenter-6.0+j*3.0, ycenter+3.0)); builder.setTransitionLayoutInfo(tfs, storm::gspn::LayoutInfo(xcenter-6.0+j*3.0, ycenter+3.0));
@ -290,9 +291,11 @@ namespace storm {
builder.addInhibitionArc(failedNodes.at(child->id()), tn); builder.addInhibitionArc(failedNodes.at(child->id()), tn);
} }
if (j != dftPand->nrChildren() - 1) { if (j != dftPand->nrChildren() - 1) {
// Not last child
tn = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(j)); tn = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(j));
builder.setTransitionLayoutInfo(tn, storm::gspn::LayoutInfo(xcenter-3.0, ycenter+3.0)); builder.setTransitionLayoutInfo(tn, storm::gspn::LayoutInfo(xcenter-3.0, ycenter+3.0));
} else { } else {
// Last child
tn = tNodeFailed; tn = tNodeFailed;
} }
builder.addInputArc(failedNodes.at(child->id()), tn); builder.addInputArc(failedNodes.at(child->id()), tn);
@ -353,7 +356,6 @@ namespace storm {
builder.addInhibitionArc(nodeFS, tfailsf); builder.addInhibitionArc(nodeFS, tfailsf);
builder.addInhibitionArc(failedNodes.at(dftPor->children().front()->id()), tfailsf); builder.addInhibitionArc(failedNodes.at(dftPor->children().front()->id()), tfailsf);
} }
++j; ++j;
} }
} else { } else {
@ -448,9 +450,6 @@ namespace storm {
builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode); builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode);
builder.addOutputArc(nextclTransitions.back(), unavailableNode); builder.addOutputArc(nextclTransitions.back(), unavailableNode);
} }
} }
template <typename ValueType> template <typename ValueType>
@ -515,13 +514,7 @@ namespace storm {
if (!smart || mDft.isRepresentative(depEv->id())) { if (!smart || mDft.isRepresentative(depEv->id())) {
builder.addOutputArc(tx, unavailableNodes.at(depEv->id())); builder.addOutputArc(tx, unavailableNodes.at(depEv->id()));
} }
} }
} }
template <typename ValueType> template <typename ValueType>

9
src/storm-gspn/storage/gspn/GSPN.cpp
View File

@ -395,6 +395,15 @@ namespace storm {
this->transitionLayout = transitionLayout; this->transitionLayout = transitionLayout;
} }
std::map<uint64_t, LayoutInfo> const& GSPN::getPlaceLayoutInfos() const {
return this->placeLayout;
}
std::map<uint64_t, LayoutInfo> const& GSPN::getTransitionLayoutInfos() const {
return this->transitionLayout;
}
void GSPN::toPnpro(std::ostream &stream) const { void GSPN::toPnpro(std::ostream &stream) const {
auto space = " "; auto space = " ";
auto space2 = " "; auto space2 = " ";

3
src/storm-gspn/storage/gspn/GSPN.h
View File

@ -155,6 +155,9 @@ namespace storm {
void setPlaceLayoutInfo(std::map<uint64_t, LayoutInfo> const& placeLayout) const; void setPlaceLayoutInfo(std::map<uint64_t, LayoutInfo> const& placeLayout) const;
void setTransitionLayoutInfo(std::map<uint64_t, LayoutInfo> const& transitionLayout) const; void setTransitionLayoutInfo(std::map<uint64_t, LayoutInfo> const& transitionLayout) const;
std::map<uint64_t, LayoutInfo> const& getPlaceLayoutInfos() const;
std::map<uint64_t, LayoutInfo> const& getTransitionLayoutInfos() const;
/*! /*!
* Performe some checks * Performe some checks

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

@ -9,6 +9,10 @@
namespace storm { namespace storm {
namespace gspn { namespace gspn {
// Prevent some magic constants
static constexpr const uint64_t scaleFactor = 50;
void GspnJsonExporter::toStream(storm::gspn::GSPN const& gspn, std::ostream& os) { void GspnJsonExporter::toStream(storm::gspn::GSPN const& gspn, std::ostream& os) {
os << translate(gspn).dump(4) << std::endl; os << translate(gspn).dump(4) << std::endl;
} }
@ -16,21 +20,48 @@ namespace storm {
modernjson::json GspnJsonExporter::translate(storm::gspn::GSPN const& gspn) { modernjson::json GspnJsonExporter::translate(storm::gspn::GSPN const& gspn) {
modernjson::json jsonGspn; modernjson::json jsonGspn;
// Layouts
std::map<uint64_t, LayoutInfo> placeLayout = gspn.getPlaceLayoutInfos();
std::map<uint64_t, LayoutInfo> transitionLayout = gspn.getTransitionLayoutInfos();
double tmpX = 0;
double tmpY = 10;
// Export places // Export places
for (const auto &place : gspn.getPlaces()) { for (const auto &place : gspn.getPlaces()) {
modernjson::json jsonPlace = translatePlace(place);
double x = tmpX;
double y = tmpY;
if (placeLayout.count(place.getID()) > 0) {
x = placeLayout.at(place.getID()).x;
y = placeLayout.at(place.getID()).y;
}
tmpX += 3;
modernjson::json jsonPlace = translatePlace(place, x, y);
jsonGspn.push_back(jsonPlace); jsonGspn.push_back(jsonPlace);
} }
// Export immediate transitions // Export immediate transitions
for (const auto &transition : gspn.getImmediateTransitions()) { for (const auto &transition : gspn.getImmediateTransitions()) {
modernjson::json jsonImmediateTransition = translateImmediateTransition(transition);
double x = tmpX;
double y = tmpY;
if (transitionLayout.count(transition.getID()) > 0) {
x = transitionLayout.at(transition.getID()).x;
y = transitionLayout.at(transition.getID()).y;
}
tmpX += 3;
modernjson::json jsonImmediateTransition = translateImmediateTransition(transition, x, y);
jsonGspn.push_back(jsonImmediateTransition); jsonGspn.push_back(jsonImmediateTransition);
} }
// Export timed transitions // Export timed transitions
for (const auto &transition : gspn.getTimedTransitions()) { for (const auto &transition : gspn.getTimedTransitions()) {
modernjson::json jsonTimedTransition = translateTimedTransition(transition);
double x = tmpX;
double y = tmpY;
if (transitionLayout.count(transition.getID()) > 0) {
x = transitionLayout.at(transition.getID()).x;
y = transitionLayout.at(transition.getID()).y;
}
tmpX += 3;
modernjson::json jsonTimedTransition = translateTimedTransition(transition, x, y);
jsonGspn.push_back(jsonTimedTransition); jsonGspn.push_back(jsonTimedTransition);
} }
@ -86,42 +117,57 @@ namespace storm {
} }
modernjson::json GspnJsonExporter::translatePlace(storm::gspn::Place const& place) {
modernjson::json GspnJsonExporter::translatePlace(storm::gspn::Place const& place, double x, double y) {
modernjson::json data; modernjson::json data;
data["id"] = toJsonString(place); data["id"] = toJsonString(place);
data["name"] = place.getName(); data["name"] = place.getName();
data["marking"] = place.getNumberOfInitialTokens(); data["marking"] = place.getNumberOfInitialTokens();
modernjson::json position;
position["x"] = x * scaleFactor;
position["y"] = y * scaleFactor;
modernjson::json jsonPlace; modernjson::json jsonPlace;
jsonPlace["data"] = data; jsonPlace["data"] = data;
jsonPlace["position"] = position;
jsonPlace["group"] = "nodes"; jsonPlace["group"] = "nodes";
jsonPlace["classes"] = "place"; jsonPlace["classes"] = "place";
return jsonPlace; return jsonPlace;
} }
modernjson::json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition) {
modernjson::json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition, double x, double y) {
modernjson::json data; modernjson::json data;
data["id"] = toJsonString(transition, true); data["id"] = toJsonString(transition, true);
data["name"] = transition.getName(); data["name"] = transition.getName();
data["priority"] = transition.getPriority(); data["priority"] = transition.getPriority();
data["weight"] = transition.getWeight(); data["weight"] = transition.getWeight();
modernjson::json position;
position["x"] = x * scaleFactor;
position["y"] = y * scaleFactor;
modernjson::json jsonTrans; modernjson::json jsonTrans;
jsonTrans["data"] = data; jsonTrans["data"] = data;
jsonTrans["position"] = position;
jsonTrans["group"] = "nodes"; jsonTrans["group"] = "nodes";
jsonTrans["classes"] = "trans_im"; jsonTrans["classes"] = "trans_im";
return jsonTrans; return jsonTrans;
} }
modernjson::json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition<double> const& transition) {
modernjson::json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition<double> const& transition, double x, double y) {
modernjson::json data; modernjson::json data;
data["id"] = toJsonString(transition, false); data["id"] = toJsonString(transition, false);
data["name"] = transition.getName(); data["name"] = transition.getName();
data["rate"] = transition.getRate(); data["rate"] = transition.getRate();
data["priority"] = transition.getPriority(); data["priority"] = transition.getPriority();
modernjson::json position;
position["x"] = x * scaleFactor;
position["y"] = y * scaleFactor;
modernjson::json jsonTrans; modernjson::json jsonTrans;
jsonTrans["data"] = data; jsonTrans["data"] = data;
jsonTrans["position"] = position;
jsonTrans["group"] = "nodes"; jsonTrans["group"] = "nodes";
jsonTrans["classes"] = "trans_time"; jsonTrans["classes"] = "trans_time";
return jsonTrans; return jsonTrans;

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

@ -26,11 +26,11 @@ namespace storm {
private: private:
enum ArcType { INPUT, OUTPUT, INHIBITOR }; enum ArcType { INPUT, OUTPUT, INHIBITOR };
static modernjson::json translatePlace(storm::gspn::Place const& place);
static modernjson::json translatePlace(storm::gspn::Place const& place, double x, double y);
static modernjson::json translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition);
static modernjson::json translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition, double x, double y);
static modernjson::json translateTimedTransition(storm::gspn::TimedTransition<double> const& transition);
static modernjson::json translateTimedTransition(storm::gspn::TimedTransition<double> const& transition, double x, double y);
static modernjson::json translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype); static modernjson::json translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype);

Write Preview
Loading…
Cancel
Save