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

Updated DFT export to new JSON format

tempestpy_adaptions
Matthias Volk 7 years ago
parent
1850cf7368
commit
7dc17065c1
2 changed files with 39 additions and 67 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. 99
      src/storm-dft/storage/dft/DftJsonExporter.cpp
  2. 7
      src/storm-dft/storage/dft/DftJsonExporter.h

99
src/storm-dft/storage/dft/DftJsonExporter.cpp
View File

@ -1,7 +1,7 @@
#include "DftJsonExporter.h"
#include "storm/utility/file.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/FileIoException.h"
#include <algorithm>
#include <string>
@ -9,19 +9,12 @@
namespace storm {
namespace storage {
template<typename ValueType>
size_t DftJsonExporter<ValueType>::currentId = 0;
template<typename ValueType>
void DftJsonExporter<ValueType>::toFile(storm::storage::DFT<ValueType> const& dft, std::string const& filepath) {
std::ofstream ofs;
ofs.open(filepath, std::ofstream::out);
if(ofs.is_open()) {
toStream(dft, ofs);
ofs.close();
} else {
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath);
}
std::ofstream stream;
storm::utility::openFile(filepath, stream);
toStream(dft, stream);
storm::utility::closeFile(stream);
}
template<typename ValueType>
@ -32,27 +25,19 @@ namespace storm {
template<typename ValueType>
modernjson::json DftJsonExporter<ValueType>::translate(storm::storage::DFT<ValueType> const& dft) {
modernjson::json jsonDft;
currentId = 0;
jsonDft["toplevel"] = dft.getTopLevelIndex();
// Parameters
modernjson::json jsonParameters;
jsonDft["parameters"] = jsonParameters;
// Nodes
modernjson::json jsonNodes;
for (size_t i = 0; i < dft.nrElements(); ++i) {
modernjson::json jsonNode = translateNode(dft.getElement(i));
jsonDft.push_back(jsonNode);
}
// Edges
modernjson::json jsonEdges;
for (size_t i = 0; i < dft.nrElements(); ++i) {
if (dft.isGate(i)) {
std::shared_ptr<DFTGate<ValueType> const> gate = dft.getGate(i);
for (size_t index = 0; index < gate->nrChildren(); ++index) {
DFTElementPointer child = gate->children()[index];
modernjson::json jsonEdge = translateEdge(gate, child, index);
jsonDft.push_back(jsonEdge);
}
}
jsonNodes.push_back(jsonNode);
}
jsonDft["nodes"] = jsonNodes;
return jsonDft;
}
@ -61,9 +46,10 @@ namespace storm {
modernjson::json DftJsonExporter<ValueType>::translateNode(DFTElementCPointer const& element) {
modernjson::json nodeData;
nodeData["id"] = element->id();
++currentId;
STORM_LOG_ASSERT(element->id() == currentId-1, "Ids do not correspond");
nodeData["name"] = element->name();
std::string type = storm::storage::toString(element->type());
std::transform(type.begin(), type.end(), type.begin(), ::tolower);
nodeData["type"] = type;
if (element->isGate()) {
// Set children for gate
@ -73,52 +59,43 @@ namespace storm {
children.push_back(child->id());
}
nodeData["children"] = children;
// Set gate specific data
switch (element->type()) {
case storm::storage::DFTElementType::VOT:
nodeData["voting"] = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(element)->threshold();
break;
default:
break;
}
} else if (element->isBasicElement()) {
// Set rates for BE
// Set BE specific data
std::shared_ptr<DFTBE<ValueType> const> be = std::static_pointer_cast<DFTBE<ValueType> const>(element);
std::stringstream stream;
stream << be->activeFailureRate();
nodeData["rate"] = stream.str();
stream.clear();
stream << (be->passiveFailureRate() / be->activeFailureRate());
nodeData["dorm"] = stream.str();
nodeData["rate"] = storm::utility::to_string(be->activeFailureRate());
nodeData["dorm"] = storm::utility::to_string(be->passiveFailureRate() / be->activeFailureRate());
nodeData["repair"] = 0;
nodeData["transient"] = be->isTransient();
} else if (element->isDependency()) {
std::shared_ptr<DFTDependency<ValueType> const> dependency = std::static_pointer_cast<DFTDependency<ValueType> const>(element);
std::vector<size_t> children = { dependency->triggerEvent()->id() };
for (DFTElementPointer const& child : dependency->dependentEvents()) {
children.push_back(child->id());
}
nodeData["children"] = children;
nodeData["prob"] = storm::utility::to_string(dependency->probability());
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Type name: " << type << " not supported for export.");
}
modernjson::json jsonNode;
jsonNode["data"] = nodeData;
jsonNode["group"] = "nodes";
std::string type = storm::storage::toString(element->type());
std::transform(type.begin(), type.end(), type.begin(), ::tolower);
jsonNode["classes"] = type;
return jsonNode;
}
template<typename ValueType>
modernjson::json DftJsonExporter<ValueType>::translateEdge(std::shared_ptr<DFTGate<ValueType> const> const& gate, DFTElementCPointer const& child, size_t index) {
modernjson::json nodeData;
std::stringstream stream;
stream << gate->id() << "e" << child->id();
nodeData["id"] = stream.str();
++currentId;
nodeData["source"] = gate->id();
nodeData["target"] = child->id();
nodeData["index"] = index;
modernjson::json jsonNode;
jsonNode["data"] = nodeData;
jsonNode["group"] = "edges";
jsonNode["classes"] = "";
return jsonNode;
}
// Explicitly instantiate the class.
template class DftJsonExporter<double>;
#ifdef STORM_HAVE_CARL
template class DftJsonExporter<storm::RationalFunction>;
#endif
}
}

7
src/storm-dft/storage/dft/DftJsonExporter.h
View File

@ -34,14 +34,9 @@ namespace storm {
private:
static size_t currentId;
static modernjson::json translateNode(DFTElementCPointer const& element);
static modernjson::json translateEdge(std::shared_ptr<DFTGate<ValueType> const> const& gate, DFTElementCPointer const& child, size_t index);
};
}
}
Write Preview
Loading…
Cancel
Save