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

Added checks for well-formedness of DFT

tempestpy_adaptions
Matthias Volk 6 years ago
parent
c7d2db4260
commit
43d1a7d2e9
2 changed files with 38 additions and 19 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. 30
      src/storm-dft/builder/DFTBuilder.cpp
  2. 23
      src/storm-dft/storage/dft/DFT.cpp

30
src/storm-dft/builder/DFTBuilder.cpp
View File

@ -18,6 +18,7 @@ namespace storm {
template<typename ValueType>
storm::storage::DFT<ValueType> DFTBuilder<ValueType>::build() {
// Build parent/child connections between elements
for(auto& elem : mChildNames) {
DFTGatePointer gate = std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(elem.first);
for(auto const& child : elem.second) {
@ -25,10 +26,11 @@ namespace storm {
if (itFind != mElements.end()) {
// Child found
DFTElementPointer childElement = itFind->second;
STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name());
if(!childElement->isDependency()) {
gate->pushBackChild(childElement);
childElement->addParent(gate);
} else {
STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name());
}
} else {
// Child not found -> find first dependent event to assure that child is dependency
@ -41,17 +43,19 @@ namespace storm {
}
}
// Build connections for restrictions
for(auto& elem : mRestrictionChildNames) {
for(auto const& childName : elem.second) {
auto itFind = mElements.find(childName);
STORM_LOG_ASSERT(itFind != mElements.end(), "Child not found.");
DFTElementPointer childElement = itFind->second;
STORM_LOG_ASSERT(!childElement->isDependency() && !childElement->isRestriction(), "Child '" << childElement->name() << "' has invalid type.");
STORM_LOG_THROW(childElement->isGate() || childElement->isBasicElement(), storm::exceptions::WrongFormatException, "Child '" << childElement->name() << "' of restriction '" << elem.first->name() << "' must be gate or BE.");
elem.first->pushBackChild(childElement);
childElement->addRestriction(elem.first);
}
}
// Build connections for dependencies
for(auto& elem : mDependencyChildNames) {
bool first = true;
std::vector<std::shared_ptr<storm::storage::DFTBE<ValueType>>> dependencies;
@ -60,16 +64,17 @@ namespace storm {
STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << childName << "' not found");
DFTElementPointer childElement = itFind->second;
if (!first) {
STORM_LOG_ASSERT(childElement->isBasicElement(), "Child '" << childName << "' of dependency '" << elem.first->name() << "' must be BE.");
STORM_LOG_THROW(childElement->isBasicElement(), storm::exceptions::WrongFormatException, "Child '" << childName << "' of dependency '" << elem.first->name() << "' must be BE.");
dependencies.push_back(std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(childElement));
} else {
first = false;
STORM_LOG_THROW(childElement->isGate() || childElement->isBasicElement(), storm::exceptions::WrongFormatException, "Child '" << childName << "' of dependency '" << elem.first->name() << "' must be gate or BE.");
elem.first->setTriggerElement(std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(childElement));
childElement->addOutgoingDependency(elem.first);
}
first = false;
}
if (binaryDependencies) {
assert(dependencies.size() == 1);
STORM_LOG_ASSERT(dependencies.size() == 1, "Dependency '" << elem.first->name() << "' should only have one dependent element.");
}
elem.first->setDependentEvents(dependencies);
for (auto& dependency : dependencies) {
@ -84,14 +89,14 @@ namespace storm {
for (auto& elem : mElements) {
computeRank(elem.second);
}
DFTElementVector elems = topoSort();
// Set ids
size_t id = 0;
for(DFTElementPointer e : elems) {
e->setId(id++);
}
STORM_LOG_ASSERT(!mTopLevelIdentifier.empty(), "No top level element.");
STORM_LOG_THROW(!mTopLevelIdentifier.empty(), storm::exceptions::WrongFormatException, "No top level element defined.");
storm::storage::DFT<ValueType> dft(elems, mElements[mTopLevelIdentifier]);
// Set layout info
@ -110,7 +115,7 @@ namespace storm {
template<typename ValueType>
unsigned DFTBuilder<ValueType>::computeRank(DFTElementPointer const& elem) {
if(elem->rank() == static_cast<decltype(elem->rank())>(-1)) {
if(elem->nrChildren() == 0 || elem->isDependency()) {
if(elem->nrChildren() == 0 || elem->isDependency() || elem->isRestriction()) {
elem->setRank(0);
} else {
DFTGatePointer gate = std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(elem);
@ -200,9 +205,8 @@ namespace storm {
template<typename ValueType>
void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, storm::storage::OrderElementsById<ValueType>>& visited, DFTElementVector& L) {
if(visited[n] == topoSortColour::GREY) {
throw storm::exceptions::WrongFormatException("DFT is cyclic");
} else if(visited[n] == topoSortColour::WHITE) {
STORM_LOG_THROW(visited[n] != topoSortColour::GREY, storm::exceptions::WrongFormatException, "DFT is cyclic");
if(visited[n] == topoSortColour::WHITE) {
if(n->isGate()) {
visited[n] = topoSortColour::GREY;
for (DFTElementPointer const& c : std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(n)->children()) {
@ -210,13 +214,13 @@ namespace storm {
}
}
// TODO restrictions and dependencies have no parents, so this can be done more efficiently.
if(n->isRestriction()) {
else if(n->isRestriction()) {
visited[n] = topoSortColour::GREY;
for (DFTElementPointer const& c : std::static_pointer_cast<storm::storage::DFTRestriction<ValueType>>(n)->children()) {
topoVisit(c, visited, L);
}
}
if(n->isDependency()) {
else if(n->isDependency()) {
visited[n] = topoSortColour::GREY;
for (DFTElementPointer const& c : std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(n)->dependentEvents()) {
topoVisit(c, visited, L);

23
src/storm-dft/storage/dft/DFT.cpp
View File

@ -4,6 +4,7 @@
#include <map>
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/WrongFormatException.h"
#include "storm/utility/iota_n.h"
#include "storm/utility/vector.h"
@ -25,11 +26,12 @@ namespace storm {
}
if(elem->isBasicElement()) {
++mNrOfBEs;
}
else if (elem->isSpareGate()) {
} else if (elem->isSpareGate()) {
// Build spare modules by setting representatives and representants
++mNrOfSpares;
mMaxSpareChildCount = std::max(mMaxSpareChildCount, std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children().size());
for(auto const& spareReprs : std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children()) {
STORM_LOG_THROW(spareReprs->isGate() || spareReprs->isBasicElement(), storm::exceptions::WrongFormatException, "Child '" << spareReprs->name() << "' of spare '" << elem->name() << "' must be gate or BE.");
std::set<size_t> module = {spareReprs->id()};
spareReprs->extendSpareModule(module);
std::vector<size_t> sparesAndBes;
@ -41,12 +43,22 @@ namespace storm {
}
mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes));
}
} else if (elem->isDependency()) {
mDependencies.push_back(elem->id());
}
}
// Check independence of spare modules
// TODO: comparing one element of each spare module sufficient?
for (auto module1 = mSpareModules.begin() ; module1 != mSpareModules.end() ; ++module1) {
size_t firstElement = module1->second.front();
for (auto module2 = std::next(module1) ; module2 != mSpareModules.end() ; ++module2) {
if (std::find(module2->second.begin(), module2->second.end(), firstElement) != module2->second.end()) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Spare modules of '" << getElement(module1->first)->name() << "' and '" << getElement(module2->first)->name() << "' should not overlap.");
}
}
}
// For the top module, we assume, contrary to [Jun15], that we have all spare gates and basic elements which are not in another module.
std::set<size_t> topModuleSet;
// Initialize with all ids.
@ -64,10 +76,13 @@ namespace storm {
// Extend top module and insert those elements which are part of the top module and a spare module
mElements[mTopLevelIndex]->extendSpareModule(topModuleSet);
mTopModule = std::vector<size_t>(topModuleSet.begin(), topModuleSet.end());
// Clear all spare modules where at least one element is also in the top module
// Clear all spare modules where at least one element is also in the top module.
// These spare modules will be activated from the beginning.
if (!mTopModule.empty()) {
for (auto& module : mSpareModules) {
if (std::find(module.second.begin(), module.second.end(), mTopModule.front()) != module.second.end()) {
STORM_LOG_WARN("Elements of spare module '" << getElement(module.first)->name() << "' also contained in top module. All elements of this spare module will be activated from the beginning on.");
module.second.clear();
}
}

Write Preview
Loading…
Cancel
Save