diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index bf68a095c..a4a15947c 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -2,6 +2,7 @@
#include <map>
#include "DFT.h"
+#include "DFTBuilder.h"
#include "src/exceptions/NotSupportedException.h"
#include "DFTIsomorphism.h"
@@ -228,7 +229,87 @@ namespace storm {
}
return stateIndex;
}
-
+
+ template<typename ValueType>
+ DFT<ValueType> DFT<ValueType>::optimize() const {
+ std::vector<std::vector<size_t>> rewriteIds = findModulesRewrite();
+ if (rewriteIds.empty()) {
+ // No rewrite needed
+ return *this;
+ }
+
+ DFTBuilder<ValueType> builder;
+
+ // Accumulate elements which must be rewritten
+ std::set<size_t> rewriteSet;
+ for (std::vector<size_t> rewrites : rewriteIds) {
+ rewriteSet.insert(rewrites.front());
+ }
+ // Copy all other elements which do not change
+ for (auto elem : mElements) {
+ if (rewriteSet.count(elem->id()) == 0) {
+ builder.copyElement(elem);
+ }
+ }
+
+ // Add rewritten elements
+ for (std::vector<size_t> rewrites : rewriteIds) {
+ assert(rewrites.size() > 1);
+ assert(mElements[rewrites[1]]->hasParents());
+ assert(mElements[rewrites[1]]->parents().front()->isGate());
+ DFTGatePointer originalParent = std::static_pointer_cast<DFTGate<ValueType>>(mElements[rewrites[1]]->parents().front());
+ std::string newParentName = builder.getUniqueName(originalParent->name());
+
+ // Accumulate children names
+ std::vector<std::string> childrenNames;
+ for (size_t i = 1; i < rewrites.size(); ++i) {
+ assert(mElements[rewrites[i]]->parents().front()->id() == originalParent->id()); // Children have the same father
+ childrenNames.push_back(mElements[rewrites[i]]->name());
+ }
+
+ // Add element inbetween parent and children
+ switch (originalParent->type()) {
+ case DFTElementType::AND:
+ builder.addAndElement(newParentName, childrenNames);
+ break;
+ case DFTElementType::OR:
+ builder.addOrElement(newParentName, childrenNames);
+ break;
+ case DFTElementType::BE:
+ case DFTElementType::CONSTF:
+ case DFTElementType::CONSTS:
+ case DFTElementType::VOT:
+ case DFTElementType::PAND:
+ case DFTElementType::SPARE:
+ case DFTElementType::POR:
+ case DFTElementType::PDEP:
+ case DFTElementType::SEQ:
+ case DFTElementType::MUTEX:
+ // Other elements are not supported
+ assert(false);
+ break;
+ default:
+ assert(false);
+ }
+
+ // Add parent with the new child newParent and all its remaining children
+ childrenNames.clear();
+ childrenNames.push_back(newParentName);
+ for (auto const& child : originalParent->children()) {
+ if (std::find(rewrites.begin()+1, rewrites.end(), child->id()) == rewrites.end()) {
+ // Child was not rewritten and must be kept
+ childrenNames.push_back(child->name());
+ }
+ }
+ builder.copyGate(originalParent, childrenNames);
+ }
+
+ builder.setTopLevel(mElements[mTopLevelIndex]->name());
+ // TODO use reference?
+ DFT<ValueType> newDft = builder.build();
+ return newDft.optimize();
+ }
+
template<typename ValueType>
std::string DFT<ValueType>::getElementsString() const {
std::stringstream stream;
@@ -449,6 +530,13 @@ namespace storm {
return res;
}
+ template<typename ValueType>
+ std::vector<std::vector<size_t>> DFT<ValueType>::findModulesRewrite() const {
+ std::vector<std::vector<size_t>> modulesRewrite;
+ // TODO write
+ return modulesRewrite;
+ }
+
// Explicitly instantiate the class.
template class DFT<double>;
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index 32e807197..557914d7e 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -34,6 +34,8 @@ namespace storm {
// Forward declarations
template<typename T> class DFTColouring;
+
+ template<typename T> class DFTBuilder;
@@ -72,6 +74,10 @@ namespace storm {
size_t generateStateInfo(DFTStateGenerationInfo& generationInfo, size_t id, storm::storage::BitVector& visited, size_t stateIndex) const;
size_t performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue<size_t>& visitQueue, storm::storage::BitVector& visited, size_t stateIndex) const;
+
+ DFT<ValueType> optimize() const;
+
+ void copyElements(std::vector<size_t> elements, DFTBuilder<ValueType> builder) const;
size_t stateVectorSize() const {
return mStateVectorSize;
@@ -236,6 +242,9 @@ namespace storm {
DFTIndependentSymmetries findSymmetries(DFTColouring<ValueType> const& colouring) const;
std::vector<size_t> immediateFailureCauses(size_t index) const;
+
+ std::vector<std::vector<size_t>> findModulesRewrite() const;
+
private:
std::pair<std::vector<size_t>, std::vector<size_t>> getSortedParentAndOutDepIds(size_t index) const;
diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp
index 08d85d879..f3d83e4c0 100644
--- a/src/storage/dft/DFTBuilder.cpp
+++ b/src/storage/dft/DFTBuilder.cpp
@@ -70,7 +70,8 @@ namespace storm {
for(DFTElementPointer e : elems) {
e->setId(id++);
}
- return DFT<ValueType>(elems, mElements[topLevelIdentifier]);
+ assert(!mTopLevelIdentifier.empty());
+ return DFT<ValueType>(elems, mElements[mTopLevelIdentifier]);
}
template<typename ValueType>
@@ -180,7 +181,6 @@ namespace storm {
}
}
- // TODO Matthias: use typedefs
template<typename ValueType>
std::vector<std::shared_ptr<DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>> visited;
@@ -195,6 +195,87 @@ namespace storm {
//std::reverse(L.begin(), L.end());
return L;
}
+
+ template<typename ValueType>
+ std::string DFTBuilder<ValueType>::getUniqueName(std::string name) {
+ return name + "_" + std::to_string(++mUniqueOffset);
+ }
+
+ template<typename ValueType>
+ void DFTBuilder<ValueType>::copyElement(DFTElementPointer element) {
+ std::vector<std::string> children;
+ switch (element->type()) {
+ case DFTElementType::AND:
+ case DFTElementType::OR:
+ case DFTElementType::PAND:
+ case DFTElementType::POR:
+ case DFTElementType::SPARE:
+ case DFTElementType::VOT:
+ {
+ for (DFTElementPointer const& elem : std::static_pointer_cast<DFTGate<ValueType>>(element)->children()) {
+ children.push_back(elem->name());
+ }
+ copyGate(std::static_pointer_cast<DFTGate<ValueType>>(element), children);
+ break;
+ }
+ case DFTElementType::BE:
+ {
+ std::shared_ptr<DFTBE<ValueType>> be = std::static_pointer_cast<DFTBE<ValueType>>(element);
+ ValueType dormancyFactor = storm::utility::zero<ValueType>();
+ if (!storm::utility::isZero(be->passiveFailureRate())) {
+ dormancyFactor = be->activeFailureRate() / be->passiveFailureRate();
+ }
+ addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor);
+ break;
+ }
+ case DFTElementType::CONSTF:
+ case DFTElementType::CONSTS:
+ // TODO
+ assert(false);
+ break;
+ case DFTElementType::PDEP:
+ {
+ DFTDependencyPointer dependency = std::static_pointer_cast<DFTDependency<ValueType>>(element);
+ children.push_back(dependency->triggerEvent()->name());
+ children.push_back(dependency->dependentEvent()->name());
+ addDepElement(element->name(), children, dependency->probability());
+ break;
+ }
+ case DFTElementType::SEQ:
+ case DFTElementType::MUTEX:
+ {
+ for (DFTElementPointer const& elem : std::static_pointer_cast<DFTRestriction<ValueType>>(element)->children()) {
+ children.push_back(elem->name());
+ }
+ addRestriction(element->name(), children, element->type());
+ break;
+ }
+ default:
+ assert(false);
+ break;
+ }
+ }
+
+ template<typename ValueType>
+ void DFTBuilder<ValueType>::copyGate(DFTGatePointer gate, std::vector<std::string> const& children) {
+ switch (gate->type()) {
+ case DFTElementType::AND:
+ case DFTElementType::OR:
+ case DFTElementType::PAND:
+ case DFTElementType::POR:
+ case DFTElementType::SPARE:
+ addStandardGate(gate->name(), children, gate->type());
+ break;
+ case DFTElementType::VOT:
+ addVotElement(gate->name(), std::static_pointer_cast<DFTVot<ValueType>>(gate)->threshold(), children);
+ break;
+ default:
+ assert(false);
+ break;
+ }
+ }
+
+
// Explicitly instantiate the class.
template class DFTBuilder<double>;
diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h
index 8ef0d6cf1..6c6fcc143 100644
--- a/src/storage/dft/DFTBuilder.h
+++ b/src/storage/dft/DFTBuilder.h
@@ -26,7 +26,8 @@ namespace storm {
private:
std::size_t mNextId = 0;
- std::string topLevelIdentifier;
+ std::size_t mUniqueOffset = 0;
+ std::string mTopLevelIdentifier;
std::unordered_map<std::string, DFTElementPointer> mElements;
std::unordered_map<DFTElementPointer, std::vector<std::string>> mChildNames;
std::unordered_map<DFTRestrictionPointer, std::vector<std::string>> mRestrictionChildNames;
@@ -140,18 +141,36 @@ namespace storm {
}
bool setTopLevel(std::string const& tle) {
- topLevelIdentifier = tle;
+ mTopLevelIdentifier = tle;
return mElements.count(tle) > 0;
}
+ std::string getUniqueName(std::string name);
+
DFT<ValueType> build();
+
+ /**
+ * Copy element and insert it again in the builder.
+ *
+ * @param element Element to copy.
+ */
+ void copyElement(DFTElementPointer element);
+
+ /**
+ * Copy gate with given children and insert it again in the builder. The current children of the element
+ * are discarded.
+ *
+ * @param gate Gate to copy.
+ * @param children New children of copied element.
+ */
+ void copyGate(DFTGatePointer gate, std::vector<std::string> const& children);
-
private:
unsigned computeRank(DFTElementPointer const& elem);
bool addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementType tp);
+
bool addRestriction(std::string const& name, std::vector<std::string> const& children, DFTElementType tp);
enum class topoSortColour {WHITE, BLACK, GREY};
diff --git a/src/storage/dft/elements/DFTVot.h b/src/storage/dft/elements/DFTVot.h
index 0233d979d..776055848 100644
--- a/src/storage/dft/elements/DFTVot.h
+++ b/src/storage/dft/elements/DFTVot.h
@@ -51,6 +51,10 @@ namespace storm {
}
}
}
+
+ unsigned threshold() const {
+ return mThreshold;
+ }
virtual DFTElementType type() const override {
return DFTElementType::VOT;
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index 13b43f5ff..6240bf374 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -29,6 +29,9 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false)
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas(parsedFormulas.begin(), parsedFormulas.end());
assert(formulas.size() == 1);
std::cout << "Parsed formula." << std::endl;
+
+ dft = dft.optimize();
+
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
if(symred) {