You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
338 lines
15 KiB
338 lines
15 KiB
#include "DFTBuilder.h"
|
|
|
|
#include <algorithm>
|
|
|
|
#include "storm/utility/macros.h"
|
|
#include "storm/exceptions/NotSupportedException.h"
|
|
#include "storm/exceptions/WrongFormatException.h"
|
|
|
|
#include "storm-dft/storage/dft/DFT.h"
|
|
#include "storm-dft/storage/dft/OrderDFTElementsById.h"
|
|
|
|
|
|
namespace storm {
|
|
namespace storage {
|
|
|
|
template<typename ValueType>
|
|
std::size_t DFTBuilder<ValueType>::mUniqueOffset = 0;
|
|
|
|
template<typename ValueType>
|
|
DFT<ValueType> DFTBuilder<ValueType>::build() {
|
|
for(auto& elem : mChildNames) {
|
|
DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem.first);
|
|
for(auto const& child : elem.second) {
|
|
auto itFind = mElements.find(child);
|
|
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 {
|
|
// Child not found -> find first dependent event to assure that child is dependency
|
|
// TODO: Not sure whether this is the intended behaviour?
|
|
auto itFind = mElements.find(child + "_1");
|
|
STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << child << "' for gate '" << gate->name() << "' not found.");
|
|
STORM_LOG_ASSERT(itFind->second->isDependency(), "Child is no dependency.");
|
|
STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name());
|
|
}
|
|
}
|
|
}
|
|
|
|
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.");
|
|
elem.first->pushBackChild(childElement);
|
|
childElement->addRestriction(elem.first);
|
|
}
|
|
}
|
|
|
|
for(auto& elem : mDependencyChildNames) {
|
|
bool first = true;
|
|
std::vector<std::shared_ptr<DFTBE<ValueType>>> dependencies;
|
|
for(auto const& childName : elem.second) {
|
|
auto itFind = mElements.find(childName);
|
|
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.");
|
|
dependencies.push_back(std::static_pointer_cast<DFTBE<ValueType>>(childElement));
|
|
} else {
|
|
elem.first->setTriggerElement(std::static_pointer_cast<DFTGate<ValueType>>(childElement));
|
|
childElement->addOutgoingDependency(elem.first);
|
|
}
|
|
first = false;
|
|
}
|
|
if (binaryDependencies) {
|
|
assert(dependencies.size() == 1);
|
|
}
|
|
elem.first->setDependentEvents(dependencies);
|
|
for (auto& dependency : dependencies) {
|
|
dependency->addIngoingDependency(elem.first);
|
|
}
|
|
|
|
}
|
|
|
|
|
|
// Sort elements topologically
|
|
// compute rank
|
|
for (auto& elem : mElements) {
|
|
computeRank(elem.second);
|
|
}
|
|
|
|
DFTElementVector elems = topoSort();
|
|
size_t id = 0;
|
|
for(DFTElementPointer e : elems) {
|
|
e->setId(id++);
|
|
}
|
|
|
|
STORM_LOG_ASSERT(!mTopLevelIdentifier.empty(), "No top level element.");
|
|
DFT<ValueType> dft(elems, mElements[mTopLevelIdentifier]);
|
|
|
|
// Set layout info
|
|
for (auto& elem : mElements) {
|
|
if(mLayoutInfo.count(elem.first) > 0) {
|
|
dft.setElementLayoutInfo(elem.second->id(), mLayoutInfo.at(elem.first));
|
|
} else {
|
|
// Set default layout
|
|
dft.setElementLayoutInfo(elem.second->id(), storm::storage::DFTLayoutInfo());
|
|
}
|
|
}
|
|
|
|
return dft;
|
|
}
|
|
|
|
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()) {
|
|
elem->setRank(0);
|
|
} else {
|
|
DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem);
|
|
unsigned maxrnk = 0;
|
|
unsigned newrnk = 0;
|
|
|
|
for (DFTElementPointer const &child : gate->children()) {
|
|
newrnk = computeRank(child);
|
|
if (newrnk > maxrnk) {
|
|
maxrnk = newrnk;
|
|
}
|
|
}
|
|
elem->setRank(maxrnk + 1);
|
|
}
|
|
}
|
|
|
|
return elem->rank();
|
|
}
|
|
|
|
template<typename ValueType>
|
|
bool DFTBuilder<ValueType>::addRestriction(std::string const& name, std::vector<std::string> const& children, DFTElementType tp) {
|
|
if (children.size() <= 1) {
|
|
STORM_LOG_ERROR("Sequence enforcers require at least two children");
|
|
}
|
|
if (mElements.count(name) != 0) {
|
|
return false;
|
|
}
|
|
DFTRestrictionPointer restr;
|
|
switch (tp) {
|
|
case DFTElementType::SEQ:
|
|
restr = std::make_shared<DFTSeq<ValueType>>(mNextId++, name);
|
|
break;
|
|
case DFTElementType::MUTEX:
|
|
// TODO notice that mutex state generation support is lacking anyway, as DONT CARE propagation would be broken for this.
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported.");
|
|
break;
|
|
default:
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known.");
|
|
break;
|
|
}
|
|
|
|
mElements[name] = restr;
|
|
mRestrictionChildNames[restr] = children;
|
|
mRestrictions.push_back(restr);
|
|
return true;
|
|
}
|
|
|
|
template<typename ValueType>
|
|
bool DFTBuilder<ValueType>::addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementType tp) {
|
|
STORM_LOG_ASSERT(children.size() > 0, "No child for " << name);
|
|
if(mElements.count(name) != 0) {
|
|
// Element with that name already exists.
|
|
return false;
|
|
}
|
|
DFTElementPointer element;
|
|
switch(tp) {
|
|
case DFTElementType::AND:
|
|
element = std::make_shared<DFTAnd<ValueType>>(mNextId++, name);
|
|
break;
|
|
case DFTElementType::OR:
|
|
element = std::make_shared<DFTOr<ValueType>>(mNextId++, name);
|
|
break;
|
|
case DFTElementType::PAND:
|
|
element = std::make_shared<DFTPand<ValueType>>(mNextId++, name, pandDefaultInclusive);
|
|
break;
|
|
case DFTElementType::POR:
|
|
element = std::make_shared<DFTPor<ValueType>>(mNextId++, name, porDefaultInclusive);
|
|
break;
|
|
case DFTElementType::SPARE:
|
|
element = std::make_shared<DFTSpare<ValueType>>(mNextId++, name);
|
|
break;
|
|
case DFTElementType::BE:
|
|
case DFTElementType::VOT:
|
|
case DFTElementType::PDEP:
|
|
// Handled separately
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type handled separately.");
|
|
case DFTElementType::CONSTF:
|
|
case DFTElementType::CONSTS:
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported.");
|
|
default:
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known.");
|
|
}
|
|
mElements[name] = element;
|
|
mChildNames[element] = children;
|
|
return true;
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>>& visited, DFTElementVector& L) {
|
|
if(visited[n] == topoSortColour::GREY) {
|
|
throw storm::exceptions::WrongFormatException("DFT is cyclic");
|
|
} else if(visited[n] == topoSortColour::WHITE) {
|
|
if(n->isGate()) {
|
|
visited[n] = topoSortColour::GREY;
|
|
for (DFTElementPointer const& c : std::static_pointer_cast<DFTGate<ValueType>>(n)->children()) {
|
|
topoVisit(c, visited, L);
|
|
}
|
|
}
|
|
// TODO restrictions and dependencies have no parents, so this can be done more efficiently.
|
|
if(n->isRestriction()) {
|
|
visited[n] = topoSortColour::GREY;
|
|
for (DFTElementPointer const& c : std::static_pointer_cast<DFTRestriction<ValueType>>(n)->children()) {
|
|
topoVisit(c, visited, L);
|
|
}
|
|
}
|
|
if(n->isDependency()) {
|
|
visited[n] = topoSortColour::GREY;
|
|
for (DFTElementPointer const& c : std::static_pointer_cast<DFTDependency<ValueType>>(n)->dependentEvents()) {
|
|
topoVisit(c, visited, L);
|
|
}
|
|
topoVisit(std::static_pointer_cast<DFTDependency<ValueType>>(n)->triggerEvent(), visited, L);
|
|
}
|
|
visited[n] = topoSortColour::BLACK;
|
|
L.push_back(n);
|
|
}
|
|
}
|
|
|
|
template<typename ValueType>
|
|
std::vector<std::shared_ptr<DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
|
|
std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>> visited;
|
|
for(auto const& e : mElements) {
|
|
visited.insert(std::make_pair(e.second, topoSortColour::WHITE));
|
|
}
|
|
|
|
DFTElementVector L;
|
|
for(auto const& e : visited) {
|
|
topoVisit(e.first, visited, L);
|
|
}
|
|
//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 (be->canFail()) {
|
|
dormancyFactor = be->passiveFailureRate() / be->activeFailureRate();
|
|
}
|
|
addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor, be->isTransient());
|
|
break;
|
|
}
|
|
case DFTElementType::CONSTF:
|
|
case DFTElementType::CONSTS:
|
|
// TODO
|
|
STORM_LOG_ASSERT(false, "Const elements not supported.");
|
|
break;
|
|
case DFTElementType::PDEP:
|
|
{
|
|
DFTDependencyPointer dependency = std::static_pointer_cast<DFTDependency<ValueType>>(element);
|
|
children.push_back(dependency->triggerEvent()->name());
|
|
for(auto const& depEv : dependency->dependentEvents()) {
|
|
children.push_back(depEv->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:
|
|
STORM_LOG_ASSERT(false, "Dft type not known.");
|
|
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:
|
|
STORM_LOG_ASSERT(false, "Dft type not known.");
|
|
break;
|
|
}
|
|
}
|
|
|
|
|
|
|
|
// Explicitly instantiate the class.
|
|
template class DFTBuilder<double>;
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template class DFTBuilder<RationalFunction>;
|
|
#endif
|
|
|
|
}
|
|
}
|
|
|