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

Moved DFTBuilder to builder dir

tempestpy_adaptions
Matthias Volk 7 years ago
parent
b00e65adf9
commit
ed7efc0268
7 changed files with 101 additions and 97 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. 118
      src/storm-dft/builder/DFTBuilder.cpp
  2. 50
      src/storm-dft/builder/DFTBuilder.h
  3. 4
      src/storm-dft/parser/DFTGalileoParser.cpp
  4. 4
      src/storm-dft/parser/DFTGalileoParser.h
  5. 4
      src/storm-dft/parser/DFTJsonParser.h
  6. 6
      src/storm-dft/storage/dft/DFT.cpp
  7. 12
      src/storm-dft/storage/dft/DFT.h

118
src/storm-dft/storage/dft/DFTBuilder.cpp → src/storm-dft/builder/DFTBuilder.cpp
View File

@ -11,15 +11,15 @@
namespace storm { namespace storm {
namespace storage {
namespace builder {
template<typename ValueType> template<typename ValueType>
std::size_t DFTBuilder<ValueType>::mUniqueOffset = 0; std::size_t DFTBuilder<ValueType>::mUniqueOffset = 0;
template<typename ValueType> template<typename ValueType>
DFT<ValueType> DFTBuilder<ValueType>::build() {
storm::storage::DFT<ValueType> DFTBuilder<ValueType>::build() {
for(auto& elem : mChildNames) { for(auto& elem : mChildNames) {
DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem.first);
DFTGatePointer gate = std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(elem.first);
for(auto const& child : elem.second) { for(auto const& child : elem.second) {
auto itFind = mElements.find(child); auto itFind = mElements.find(child);
if (itFind != mElements.end()) { if (itFind != mElements.end()) {
@ -54,16 +54,16 @@ namespace storm {
for(auto& elem : mDependencyChildNames) { for(auto& elem : mDependencyChildNames) {
bool first = true; bool first = true;
std::vector<std::shared_ptr<DFTBE<ValueType>>> dependencies;
std::vector<std::shared_ptr<storm::storage::DFTBE<ValueType>>> dependencies;
for(auto const& childName : elem.second) { for(auto const& childName : elem.second) {
auto itFind = mElements.find(childName); auto itFind = mElements.find(childName);
STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << childName << "' not found"); STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << childName << "' not found");
DFTElementPointer childElement = itFind->second; DFTElementPointer childElement = itFind->second;
if (!first) { if (!first) {
STORM_LOG_ASSERT(childElement->isBasicElement(), "Child '" << childName << "' of dependency '" << elem.first->name() << "' must be BE."); 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));
dependencies.push_back(std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(childElement));
} else { } else {
elem.first->setTriggerElement(std::static_pointer_cast<DFTGate<ValueType>>(childElement));
elem.first->setTriggerElement(std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(childElement));
childElement->addOutgoingDependency(elem.first); childElement->addOutgoingDependency(elem.first);
} }
first = false; first = false;
@ -92,7 +92,7 @@ namespace storm {
} }
STORM_LOG_ASSERT(!mTopLevelIdentifier.empty(), "No top level element."); STORM_LOG_ASSERT(!mTopLevelIdentifier.empty(), "No top level element.");
DFT<ValueType> dft(elems, mElements[mTopLevelIdentifier]);
storm::storage::DFT<ValueType> dft(elems, mElements[mTopLevelIdentifier]);
// Set layout info // Set layout info
for (auto& elem : mElements) { for (auto& elem : mElements) {
@ -113,7 +113,7 @@ namespace storm {
if(elem->nrChildren() == 0 || elem->isDependency()) { if(elem->nrChildren() == 0 || elem->isDependency()) {
elem->setRank(0); elem->setRank(0);
} else { } else {
DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem);
DFTGatePointer gate = std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(elem);
unsigned maxrnk = 0; unsigned maxrnk = 0;
unsigned newrnk = 0; unsigned newrnk = 0;
@ -131,7 +131,7 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
bool DFTBuilder<ValueType>::addRestriction(std::string const& name, std::vector<std::string> const& children, DFTElementType tp) {
bool DFTBuilder<ValueType>::addRestriction(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp) {
if (children.size() <= 1) { if (children.size() <= 1) {
STORM_LOG_ERROR("Sequence enforcers require at least two children"); STORM_LOG_ERROR("Sequence enforcers require at least two children");
} }
@ -140,10 +140,10 @@ namespace storm {
} }
DFTRestrictionPointer restr; DFTRestrictionPointer restr;
switch (tp) { switch (tp) {
case DFTElementType::SEQ:
restr = std::make_shared<DFTSeq<ValueType>>(mNextId++, name);
case storm::storage::DFTElementType::SEQ:
restr = std::make_shared<storm::storage::DFTSeq<ValueType>>(mNextId++, name);
break; break;
case DFTElementType::MUTEX:
case storm::storage::DFTElementType::MUTEX:
// TODO notice that mutex state generation support is lacking anyway, as DONT CARE propagation would be broken for this. // 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."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported.");
break; break;
@ -159,7 +159,7 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
bool DFTBuilder<ValueType>::addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementType tp) {
bool DFTBuilder<ValueType>::addStandardGate(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp) {
STORM_LOG_ASSERT(children.size() > 0, "No child for " << name); STORM_LOG_ASSERT(children.size() > 0, "No child for " << name);
if(mElements.count(name) != 0) { if(mElements.count(name) != 0) {
// Element with that name already exists. // Element with that name already exists.
@ -167,28 +167,28 @@ namespace storm {
} }
DFTElementPointer element; DFTElementPointer element;
switch(tp) { switch(tp) {
case DFTElementType::AND:
element = std::make_shared<DFTAnd<ValueType>>(mNextId++, name);
case storm::storage::DFTElementType::AND:
element = std::make_shared<storm::storage::DFTAnd<ValueType>>(mNextId++, name);
break; break;
case DFTElementType::OR:
element = std::make_shared<DFTOr<ValueType>>(mNextId++, name);
case storm::storage::DFTElementType::OR:
element = std::make_shared<storm::storage::DFTOr<ValueType>>(mNextId++, name);
break; break;
case DFTElementType::PAND:
element = std::make_shared<DFTPand<ValueType>>(mNextId++, name, pandDefaultInclusive);
case storm::storage::DFTElementType::PAND:
element = std::make_shared<storm::storage::DFTPand<ValueType>>(mNextId++, name, pandDefaultInclusive);
break; break;
case DFTElementType::POR:
element = std::make_shared<DFTPor<ValueType>>(mNextId++, name, porDefaultInclusive);
case storm::storage::DFTElementType::POR:
element = std::make_shared<storm::storage::DFTPor<ValueType>>(mNextId++, name, porDefaultInclusive);
break; break;
case DFTElementType::SPARE:
element = std::make_shared<DFTSpare<ValueType>>(mNextId++, name);
case storm::storage::DFTElementType::SPARE:
element = std::make_shared<storm::storage::DFTSpare<ValueType>>(mNextId++, name);
break; break;
case DFTElementType::BE:
case DFTElementType::VOT:
case DFTElementType::PDEP:
case storm::storage::DFTElementType::BE:
case storm::storage::DFTElementType::VOT:
case storm::storage::DFTElementType::PDEP:
// Handled separately // Handled separately
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type handled separately."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type handled separately.");
case DFTElementType::CONSTF:
case DFTElementType::CONSTS:
case storm::storage::DFTElementType::CONSTF:
case storm::storage::DFTElementType::CONSTS:
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported.");
default: default:
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known.");
@ -199,29 +199,29 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>>& visited, DFTElementVector& L) {
void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, storm::storage::OrderElementsById<ValueType>>& visited, DFTElementVector& L) {
if(visited[n] == topoSortColour::GREY) { if(visited[n] == topoSortColour::GREY) {
throw storm::exceptions::WrongFormatException("DFT is cyclic"); throw storm::exceptions::WrongFormatException("DFT is cyclic");
} else if(visited[n] == topoSortColour::WHITE) { } else if(visited[n] == topoSortColour::WHITE) {
if(n->isGate()) { if(n->isGate()) {
visited[n] = topoSortColour::GREY; visited[n] = topoSortColour::GREY;
for (DFTElementPointer const& c : std::static_pointer_cast<DFTGate<ValueType>>(n)->children()) {
for (DFTElementPointer const& c : std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(n)->children()) {
topoVisit(c, visited, L); topoVisit(c, visited, L);
} }
} }
// TODO restrictions and dependencies have no parents, so this can be done more efficiently. // TODO restrictions and dependencies have no parents, so this can be done more efficiently.
if(n->isRestriction()) { if(n->isRestriction()) {
visited[n] = topoSortColour::GREY; visited[n] = topoSortColour::GREY;
for (DFTElementPointer const& c : std::static_pointer_cast<DFTRestriction<ValueType>>(n)->children()) {
for (DFTElementPointer const& c : std::static_pointer_cast<storm::storage::DFTRestriction<ValueType>>(n)->children()) {
topoVisit(c, visited, L); topoVisit(c, visited, L);
} }
} }
if(n->isDependency()) { if(n->isDependency()) {
visited[n] = topoSortColour::GREY; visited[n] = topoSortColour::GREY;
for (DFTElementPointer const& c : std::static_pointer_cast<DFTDependency<ValueType>>(n)->dependentEvents()) {
for (DFTElementPointer const& c : std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(n)->dependentEvents()) {
topoVisit(c, visited, L); topoVisit(c, visited, L);
} }
topoVisit(std::static_pointer_cast<DFTDependency<ValueType>>(n)->triggerEvent(), visited, L);
topoVisit(std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(n)->triggerEvent(), visited, L);
} }
visited[n] = topoSortColour::BLACK; visited[n] = topoSortColour::BLACK;
L.push_back(n); L.push_back(n);
@ -229,8 +229,8 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
std::vector<std::shared_ptr<DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>> visited;
std::vector<std::shared_ptr<storm::storage::DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
std::map<DFTElementPointer, topoSortColour, storm::storage::OrderElementsById<ValueType>> visited;
for(auto const& e : mElements) { for(auto const& e : mElements) {
visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); visited.insert(std::make_pair(e.second, topoSortColour::WHITE));
} }
@ -252,22 +252,22 @@ namespace storm {
void DFTBuilder<ValueType>::copyElement(DFTElementPointer element) { void DFTBuilder<ValueType>::copyElement(DFTElementPointer element) {
std::vector<std::string> children; std::vector<std::string> children;
switch (element->type()) { switch (element->type()) {
case DFTElementType::AND:
case DFTElementType::OR:
case DFTElementType::PAND:
case DFTElementType::POR:
case DFTElementType::SPARE:
case DFTElementType::VOT:
case storm::storage::DFTElementType::AND:
case storm::storage::DFTElementType::OR:
case storm::storage::DFTElementType::PAND:
case storm::storage::DFTElementType::POR:
case storm::storage::DFTElementType::SPARE:
case storm::storage::DFTElementType::VOT:
{ {
for (DFTElementPointer const& elem : std::static_pointer_cast<DFTGate<ValueType>>(element)->children()) {
for (DFTElementPointer const& elem : std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(element)->children()) {
children.push_back(elem->name()); children.push_back(elem->name());
} }
copyGate(std::static_pointer_cast<DFTGate<ValueType>>(element), children);
copyGate(std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(element), children);
break; break;
} }
case DFTElementType::BE:
case storm::storage::DFTElementType::BE:
{ {
std::shared_ptr<DFTBE<ValueType>> be = std::static_pointer_cast<DFTBE<ValueType>>(element);
std::shared_ptr<storm::storage::DFTBE<ValueType>> be = std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(element);
ValueType dormancyFactor = storm::utility::zero<ValueType>(); ValueType dormancyFactor = storm::utility::zero<ValueType>();
if (be->canFail()) { if (be->canFail()) {
dormancyFactor = be->passiveFailureRate() / be->activeFailureRate(); dormancyFactor = be->passiveFailureRate() / be->activeFailureRate();
@ -275,14 +275,14 @@ namespace storm {
addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor, be->isTransient()); addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor, be->isTransient());
break; break;
} }
case DFTElementType::CONSTF:
case DFTElementType::CONSTS:
case storm::storage::DFTElementType::CONSTF:
case storm::storage::DFTElementType::CONSTS:
// TODO // TODO
STORM_LOG_ASSERT(false, "Const elements not supported."); STORM_LOG_ASSERT(false, "Const elements not supported.");
break; break;
case DFTElementType::PDEP:
case storm::storage::DFTElementType::PDEP:
{ {
DFTDependencyPointer dependency = std::static_pointer_cast<DFTDependency<ValueType>>(element);
DFTDependencyPointer dependency = std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(element);
children.push_back(dependency->triggerEvent()->name()); children.push_back(dependency->triggerEvent()->name());
for(auto const& depEv : dependency->dependentEvents()) { for(auto const& depEv : dependency->dependentEvents()) {
children.push_back(depEv->name()); children.push_back(depEv->name());
@ -290,10 +290,10 @@ namespace storm {
addDepElement(element->name(), children, dependency->probability()); addDepElement(element->name(), children, dependency->probability());
break; break;
} }
case DFTElementType::SEQ:
case DFTElementType::MUTEX:
case storm::storage::DFTElementType::SEQ:
case storm::storage::DFTElementType::MUTEX:
{ {
for (DFTElementPointer const& elem : std::static_pointer_cast<DFTRestriction<ValueType>>(element)->children()) {
for (DFTElementPointer const& elem : std::static_pointer_cast<storm::storage::DFTRestriction<ValueType>>(element)->children()) {
children.push_back(elem->name()); children.push_back(elem->name());
} }
addRestriction(element->name(), children, element->type()); addRestriction(element->name(), children, element->type());
@ -308,15 +308,15 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void DFTBuilder<ValueType>::copyGate(DFTGatePointer gate, std::vector<std::string> const& children) { void DFTBuilder<ValueType>::copyGate(DFTGatePointer gate, std::vector<std::string> const& children) {
switch (gate->type()) { switch (gate->type()) {
case DFTElementType::AND:
case DFTElementType::OR:
case DFTElementType::PAND:
case DFTElementType::POR:
case DFTElementType::SPARE:
case storm::storage::DFTElementType::AND:
case storm::storage::DFTElementType::OR:
case storm::storage::DFTElementType::PAND:
case storm::storage::DFTElementType::POR:
case storm::storage::DFTElementType::SPARE:
addStandardGate(gate->name(), children, gate->type()); addStandardGate(gate->name(), children, gate->type());
break; break;
case DFTElementType::VOT:
addVotElement(gate->name(), std::static_pointer_cast<DFTVot<ValueType>>(gate)->threshold(), children);
case storm::storage::DFTElementType::VOT:
addVotElement(gate->name(), std::static_pointer_cast<storm::storage::DFTVot<ValueType>>(gate)->threshold(), children);
break; break;
default: default:
STORM_LOG_ASSERT(false, "Dft type not known."); STORM_LOG_ASSERT(false, "Dft type not known.");

50
src/storm-dft/storage/dft/DFTBuilder.h → src/storm-dft/builder/DFTBuilder.h
View File

@ -11,18 +11,22 @@
namespace storm { namespace storm {
namespace storage { namespace storage {
// Forward declaration
template<typename ValueType> template<typename ValueType>
class DFT; class DFT;
}
namespace builder {
template<typename ValueType> template<typename ValueType>
class DFTBuilder { class DFTBuilder {
using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
using DFTElementVector = std::vector<DFTElementPointer>; using DFTElementVector = std::vector<DFTElementPointer>;
using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
using DFTGateVector = std::vector<DFTGatePointer>; using DFTGateVector = std::vector<DFTGatePointer>;
using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
using DFTRestrictionPointer = std::shared_ptr<DFTRestriction<ValueType>>;
using DFTDependencyPointer = std::shared_ptr<storm::storage::DFTDependency<ValueType>>;
using DFTRestrictionPointer = std::shared_ptr<storm::storage::DFTRestriction<ValueType>>;
private: private:
std::size_t mNextId = 0; std::size_t mNextId = 0;
@ -34,7 +38,7 @@ namespace storm {
std::unordered_map<DFTDependencyPointer, std::vector<std::string>> mDependencyChildNames; std::unordered_map<DFTDependencyPointer, std::vector<std::string>> mDependencyChildNames;
std::vector<DFTDependencyPointer> mDependencies; std::vector<DFTDependencyPointer> mDependencies;
std::vector<DFTRestrictionPointer> mRestrictions; std::vector<DFTRestrictionPointer> mRestrictions;
std::unordered_map<std::string, DFTLayoutInfo> mLayoutInfo;
std::unordered_map<std::string, storm::storage::DFTLayoutInfo> mLayoutInfo;
public: public:
DFTBuilder(bool defaultInclusive = true, bool binaryDependencies = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive), binaryDependencies(binaryDependencies) { DFTBuilder(bool defaultInclusive = true, bool binaryDependencies = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive), binaryDependencies(binaryDependencies) {
@ -42,47 +46,47 @@ namespace storm {
} }
bool addAndElement(std::string const& name, std::vector<std::string> const& children) { bool addAndElement(std::string const& name, std::vector<std::string> const& children) {
return addStandardGate(name, children, DFTElementType::AND);
return addStandardGate(name, children, storm::storage::DFTElementType::AND);
} }
bool addOrElement(std::string const& name, std::vector<std::string> const& children) { bool addOrElement(std::string const& name, std::vector<std::string> const& children) {
return addStandardGate(name, children, DFTElementType::OR);
return addStandardGate(name, children, storm::storage::DFTElementType::OR);
} }
bool addPandElement(std::string const& name, std::vector<std::string> const& children) { bool addPandElement(std::string const& name, std::vector<std::string> const& children) {
return addStandardGate(name, children, DFTElementType::PAND);
return addStandardGate(name, children, storm::storage::DFTElementType::PAND);
} }
bool addPandElement(std::string const& name, std::vector<std::string> const& children, bool inclusive) { bool addPandElement(std::string const& name, std::vector<std::string> const& children, bool inclusive) {
bool tmpDefault = pandDefaultInclusive; bool tmpDefault = pandDefaultInclusive;
pandDefaultInclusive = inclusive; pandDefaultInclusive = inclusive;
bool result = addStandardGate(name, children, DFTElementType::PAND);
bool result = addStandardGate(name, children, storm::storage::DFTElementType::PAND);
pandDefaultInclusive = tmpDefault; pandDefaultInclusive = tmpDefault;
return result; return result;
} }
bool addPorElement(std::string const& name, std::vector<std::string> const& children) { bool addPorElement(std::string const& name, std::vector<std::string> const& children) {
return addStandardGate(name, children, DFTElementType::POR);
return addStandardGate(name, children, storm::storage::DFTElementType::POR);
} }
bool addPorElement(std::string const& name, std::vector<std::string> const& children, bool inclusive) { bool addPorElement(std::string const& name, std::vector<std::string> const& children, bool inclusive) {
bool tmpDefault = porDefaultInclusive; bool tmpDefault = porDefaultInclusive;
porDefaultInclusive = inclusive; porDefaultInclusive = inclusive;
bool result = addStandardGate(name, children, DFTElementType::POR);
bool result = addStandardGate(name, children, storm::storage::DFTElementType::POR);
pandDefaultInclusive = tmpDefault; pandDefaultInclusive = tmpDefault;
return result; return result;
} }
bool addSpareElement(std::string const& name, std::vector<std::string> const& children) { bool addSpareElement(std::string const& name, std::vector<std::string> const& children) {
return addStandardGate(name, children, DFTElementType::SPARE);
return addStandardGate(name, children, storm::storage::DFTElementType::SPARE);
} }
bool addSequenceEnforcer(std::string const& name, std::vector<std::string> const& children) { bool addSequenceEnforcer(std::string const& name, std::vector<std::string> const& children) {
return addRestriction(name, children, DFTElementType::SEQ);
return addRestriction(name, children, storm::storage::DFTElementType::SEQ);
} }
bool addMutex(std::string const& name, std::vector<std::string> const& children) { bool addMutex(std::string const& name, std::vector<std::string> const& children) {
return addRestriction(name, children, DFTElementType::MUTEX);
return addRestriction(name, children, storm::storage::DFTElementType::MUTEX);
} }
bool addDepElement(std::string const& name, std::vector<std::string> const& children, ValueType probability) { bool addDepElement(std::string const& name, std::vector<std::string> const& children, ValueType probability) {
@ -125,15 +129,13 @@ namespace storm {
} }
STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2,
"PDep with multiple children supported."); "PDep with multiple children supported.");
DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++,
nameDep,
probability);
DFTDependencyPointer element = std::make_shared<storm::storage::DFTDependency<ValueType>>(mNextId++, nameDep, probability);
mElements[element->name()] = element; mElements[element->name()] = element;
mDependencyChildNames[element] = {trigger, children[i]}; mDependencyChildNames[element] = {trigger, children[i]};
mDependencies.push_back(element); mDependencies.push_back(element);
} }
} else { } else {
DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, name, probability);
DFTDependencyPointer element = std::make_shared<storm::storage::DFTDependency<ValueType>>(mNextId++, name, probability);
mElements[element->name()] = element; mElements[element->name()] = element;
mDependencyChildNames[element] = children; mDependencyChildNames[element] = children;
mDependencies.push_back(element); mDependencies.push_back(element);
@ -161,7 +163,7 @@ namespace storm {
STORM_LOG_ERROR("Voting gates with threshold higher than the number of children is not supported."); STORM_LOG_ERROR("Voting gates with threshold higher than the number of children is not supported.");
return false; return false;
} }
DFTElementPointer element = std::make_shared<DFTVot<ValueType>>(mNextId++, name, threshold);
DFTElementPointer element = std::make_shared<storm::storage::DFTVot<ValueType>>(mNextId++, name, threshold);
mElements[name] = element; mElements[name] = element;
mChildNames[element] = children; mChildNames[element] = children;
@ -173,7 +175,7 @@ namespace storm {
//failureRate > 0 //failureRate > 0
//0 <= dormancyFactor <= 1 //0 <= dormancyFactor <= 1
mElements[name] = std::make_shared<DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor, transient);
mElements[name] = std::make_shared<storm::storage::DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor, transient);
return true; return true;
} }
@ -189,7 +191,7 @@ namespace storm {
std::string getUniqueName(std::string name); std::string getUniqueName(std::string name);
DFT<ValueType> build();
storm::storage::DFT<ValueType> build();
/** /**
* Copy element and insert it again in the builder. * Copy element and insert it again in the builder.
@ -211,13 +213,13 @@ namespace storm {
unsigned computeRank(DFTElementPointer const& elem); unsigned computeRank(DFTElementPointer const& elem);
bool addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementType tp);
bool addStandardGate(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp);
bool addRestriction(std::string const& name, std::vector<std::string> const& children, DFTElementType tp);
bool addRestriction(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp);
enum class topoSortColour {WHITE, BLACK, GREY}; enum class topoSortColour {WHITE, BLACK, GREY};
void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>>& visited, DFTElementVector& L);
void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, storm::storage::OrderElementsById<ValueType>>& visited, DFTElementVector& L);
DFTElementVector topoSort(); DFTElementVector topoSort();

4
src/storm-dft/parser/DFTGalileoParser.cpp
View File

@ -33,7 +33,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
storm::storage::DFT<ValueType> DFTGalileoParser<ValueType>::parseDFT(const std::string& filename, bool defaultInclusive, bool binaryDependencies) { storm::storage::DFT<ValueType> DFTGalileoParser<ValueType>::parseDFT(const std::string& filename, bool defaultInclusive, bool binaryDependencies) {
storm::storage::DFTBuilder<ValueType> builder(defaultInclusive, binaryDependencies);
storm::builder::DFTBuilder<ValueType> builder(defaultInclusive, binaryDependencies);
ValueParser<ValueType> valueParser; ValueParser<ValueType> valueParser;
// Regular expression to detect comments // Regular expression to detect comments
// taken from: https://stackoverflow.com/questions/9449887/removing-c-c-style-comments-using-boostregex // taken from: https://stackoverflow.com/questions/9449887/removing-c-c-style-comments-using-boostregex
@ -166,7 +166,7 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
bool DFTGalileoParser<ValueType>::parseBasicElement(std::vector<std::string> const& tokens, storm::storage::DFTBuilder<ValueType>& builder, ValueParser<ValueType>& valueParser) {
bool DFTGalileoParser<ValueType>::parseBasicElement(std::vector<std::string> const& tokens, storm::builder::DFTBuilder<ValueType>& builder, ValueParser<ValueType>& valueParser) {
// Default values // Default values
Distribution distribution = Distribution::None; Distribution distribution = Distribution::None;
ValueType firstValDistribution = storm::utility::zero<ValueType>(); ValueType firstValDistribution = storm::utility::zero<ValueType>();

4
src/storm-dft/parser/DFTGalileoParser.h
View File

@ -7,7 +7,7 @@
#include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/expressions/ExpressionEvaluator.h"
#include "storm-dft/storage/dft/DFT.h" #include "storm-dft/storage/dft/DFT.h"
#include "storm-dft/storage/dft/DFTBuilder.h"
#include "storm-dft/builder/DFTBuilder.h"
#include "storm/parser/ValueParser.h" #include "storm/parser/ValueParser.h"
@ -51,7 +51,7 @@ namespace storm {
* *
* @return True iff the parsing and creation was successful. * @return True iff the parsing and creation was successful.
*/ */
static bool parseBasicElement(std::vector<std::string> const& tokens, storm::storage::DFTBuilder<ValueType>& builder, ValueParser<ValueType>& valueParser);
static bool parseBasicElement(std::vector<std::string> const& tokens, storm::builder::DFTBuilder<ValueType>& builder, ValueParser<ValueType>& valueParser);
enum Distribution { None, Constant, Exponential, Weibull, LogNormal }; enum Distribution { None, Constant, Exponential, Weibull, LogNormal };
}; };

4
src/storm-dft/parser/DFTJsonParser.h
View File

@ -7,7 +7,7 @@
#include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/expressions/ExpressionEvaluator.h"
#include "storm-dft/storage/dft/DFT.h" #include "storm-dft/storage/dft/DFT.h"
#include "storm-dft/storage/dft/DFTBuilder.h"
#include "storm-dft/builder/DFTBuilder.h"
// JSON parser // JSON parser
#include "json.hpp" #include "json.hpp"
@ -19,7 +19,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
class DFTJsonParser { class DFTJsonParser {
storm::storage::DFTBuilder<ValueType> builder;
storm::builder::DFTBuilder<ValueType> builder;
std::shared_ptr<storm::expressions::ExpressionManager> manager; std::shared_ptr<storm::expressions::ExpressionManager> manager;

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

@ -7,7 +7,7 @@
#include "storm/utility/iota_n.h" #include "storm/utility/iota_n.h"
#include "storm/utility/vector.h" #include "storm/utility/vector.h"
#include "storm-dft/storage/dft/DFTBuilder.h"
#include "storm-dft/builder/DFTBuilder.h"
#include "storm-dft/storage/dft/DFTIsomorphism.h" #include "storm-dft/storage/dft/DFTIsomorphism.h"
@ -271,7 +271,7 @@ namespace storm {
std::vector<DFT<ValueType>> res; std::vector<DFT<ValueType>> res;
for(auto const& subdft : subdfts) { for(auto const& subdft : subdfts) {
DFTBuilder<ValueType> builder;
storm::builder::DFTBuilder<ValueType> builder;
for(size_t id : subdft.second) { for(size_t id : subdft.second) {
builder.copyElement(mElements[id]); builder.copyElement(mElements[id]);
@ -307,7 +307,7 @@ namespace storm {
std::vector<std::vector<size_t>> rewriteIds; std::vector<std::vector<size_t>> rewriteIds;
rewriteIds.push_back(modIdea); rewriteIds.push_back(modIdea);
DFTBuilder<ValueType> builder;
storm::builder::DFTBuilder<ValueType> builder;
// Accumulate elements which must be rewritten // Accumulate elements which must be rewritten
std::set<size_t> rewriteSet; std::set<size_t> rewriteSet;

12
src/storm-dft/storage/dft/DFT.h
View File

@ -18,6 +18,11 @@
#include "storm-dft/storage/dft/DFTLayoutInfo.h" #include "storm-dft/storage/dft/DFTLayoutInfo.h"
namespace storm { namespace storm {
namespace builder {
// Forward declaration
template<typename T> class DFTBuilder;
}
namespace storage { namespace storage {
template<typename ValueType> template<typename ValueType>
@ -32,11 +37,8 @@ namespace storm {
}; };
// Forward declarations
// Forward declaration
template<typename T> class DFTColouring; template<typename T> class DFTColouring;
template<typename T> class DFTBuilder;
/** /**
* Represents a Dynamic Fault Tree * Represents a Dynamic Fault Tree
@ -76,7 +78,7 @@ namespace storm {
DFT<ValueType> optimize() const; DFT<ValueType> optimize() const;
void copyElements(std::vector<size_t> elements, DFTBuilder<ValueType> builder) const;
void copyElements(std::vector<size_t> elements, storm::builder::DFTBuilder<ValueType> builder) const;
size_t stateVectorSize() const { size_t stateVectorSize() const {
return mStateVectorSize; return mStateVectorSize;

Write Preview
Loading…
Cancel
Save