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

Added unique constant failure in transformation

tempestpy_adaptions
Alexander Bork 6 years ago
parent
69987cc76c
commit
12c0a6d72c
1 changed files with 21 additions and 3 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. 24
      src/storm-dft/transformations/DftTransformator.cpp

24
src/storm-dft/transformations/DftTransformator.cpp
View File

@ -15,9 +15,9 @@ namespace storm {
for (size_t i = 0; i < mDft.nrElements(); ++i) { for (size_t i = 0; i < mDft.nrElements(); ++i) {
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = mDft.getElement(i); std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = mDft.getElement(i);
STORM_LOG_DEBUG("Transform " + element->name());
switch (element->type()) { switch (element->type()) {
case storm::storage::DFTElementType::BE_EXP: { case storm::storage::DFTElementType::BE_EXP: {
STORM_LOG_DEBUG("Transform " + element->name() + " [BE (exp)]");
auto be_exp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>( auto be_exp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>(
element); element);
builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(),
@ -28,43 +28,58 @@ namespace storm {
auto be_const = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>( auto be_const = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>(
element); element);
if (be_const->canFail()) { if (be_const->canFail()) {
STORM_LOG_DEBUG("Transform " + element->name() + " [BE (const failed)]");
failedBEs.push_back(be_const->name()); failedBEs.push_back(be_const->name());
} else {
STORM_LOG_DEBUG("Transform " + element->name() + " [BE (const failsafe)]");
} }
// All original constant BEs are set to failsafe, failed BEs are later triggered by a new element // All original constant BEs are set to failsafe, failed BEs are later triggered by a new element
builder.addBasicElementConst(be_const->name(), false); builder.addBasicElementConst(be_const->name(), false);
break; break;
} }
case storm::storage::DFTElementType::AND: case storm::storage::DFTElementType::AND:
STORM_LOG_DEBUG("Transform " + element->name() + " [AND]");
builder.addAndElement(element->name(), getChildrenVector(element)); builder.addAndElement(element->name(), getChildrenVector(element));
break; break;
case storm::storage::DFTElementType::OR: case storm::storage::DFTElementType::OR:
STORM_LOG_DEBUG("Transform " + element->name() + " [OR]");
builder.addOrElement(element->name(), getChildrenVector(element)); builder.addOrElement(element->name(), getChildrenVector(element));
break; break;
case storm::storage::DFTElementType::VOT: { case storm::storage::DFTElementType::VOT: {
STORM_LOG_DEBUG("Transform " + element->name() + " [VOT]");
auto vot = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(element); auto vot = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(element);
builder.addVotElement(vot->name(), vot->threshold(), getChildrenVector(vot)); builder.addVotElement(vot->name(), vot->threshold(), getChildrenVector(vot));
break; break;
} }
case storm::storage::DFTElementType::PAND: { case storm::storage::DFTElementType::PAND: {
STORM_LOG_DEBUG("Transform " + element->name() + " [PAND]");
auto pand = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(element); auto pand = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(element);
builder.addPandElement(pand->name(), getChildrenVector(pand), pand->isInclusive()); builder.addPandElement(pand->name(), getChildrenVector(pand), pand->isInclusive());
break; break;
} }
case storm::storage::DFTElementType::POR: { case storm::storage::DFTElementType::POR: {
STORM_LOG_DEBUG("Transform " + element->name() + " [POR]");
auto por = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(element); auto por = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(element);
builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive()); builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive());
break; break;
} }
case storm::storage::DFTElementType::SPARE: case storm::storage::DFTElementType::SPARE:
STORM_LOG_DEBUG("Transform " + element->name() + " [SPARE]");
builder.addSpareElement(element->name(), getChildrenVector(element)); builder.addSpareElement(element->name(), getChildrenVector(element));
break; break;
case storm::storage::DFTElementType::PDEP: { case storm::storage::DFTElementType::PDEP: {
auto dep = std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>( auto dep = std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(
element); element);
if (dep->isFDEP()) {
STORM_LOG_DEBUG("Transform " + element->name() + " [FDEP]");
} else {
STORM_LOG_DEBUG("Transform " + element->name() + " [PDEP]");
}
builder.addDepElement(dep->name(), getChildrenVector(element), dep->probability()); builder.addDepElement(dep->name(), getChildrenVector(element), dep->probability());
break; break;
} }
case storm::storage::DFTElementType::SEQ: case storm::storage::DFTElementType::SEQ:
STORM_LOG_DEBUG("Transform " + element->name() + " [SEQ]");
builder.addSequenceEnforcer(element->name(), getChildrenVector(element)); builder.addSequenceEnforcer(element->name(), getChildrenVector(element));
break; break;
default: default:
@ -75,6 +90,11 @@ namespace storm {
} }
// At this point the DFT is an exact copy of the original, except for all constant failure probabilities being 0 // At this point the DFT is an exact copy of the original, except for all constant failure probabilities being 0
if (!failedBEs.empty()) {
builder.addBasicElementConst("Unique_Constant_Failure", true);
failedBEs.insert(std::begin(failedBEs), "Unique_Constant_Failure");
builder.addDepElement("Failure_Trigger", failedBEs, storm::utility::one<ValueType>());
}
builder.setTopLevel(mDft.getTopLevelGate()->name()); builder.setTopLevel(mDft.getTopLevelGate()->name());
@ -85,7 +105,6 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
std::vector<std::string> DftTransformator<ValueType>::getChildrenVector( std::vector<std::string> DftTransformator<ValueType>::getChildrenVector(
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) { std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) {
STORM_LOG_DEBUG("Get children for " + element->name());
std::vector<std::string> res; std::vector<std::string> res;
if (element->isDependency()) { if (element->isDependency()) {
// Dependencies have to be handled separately // Dependencies have to be handled separately
@ -99,7 +118,6 @@ namespace storm {
element); element);
for (auto const &child : elementWithChildren->children()) { for (auto const &child : elementWithChildren->children()) {
res.push_back(child->name()); res.push_back(child->name());
STORM_LOG_DEBUG("Got child " + child->name());
} }
} }
return res; return res;

Write Preview
Loading…
Cancel
Save