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

removed transformators for now

tempestpy_adaptions
Sebastian Junges 8 years ago
parent
bed4710c7f
commit
752f20a65f
2 changed files with 0 additions and 1015 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. 845
      src/transformations/dft/DftToGspnTransformator.cpp
  2. 170
      src/transformations/dft/DftToGspnTransformator.h

845
src/transformations/dft/DftToGspnTransformator.cpp
View File

@ -1,845 +0,0 @@
#include "src/transformations/dft/DftToGspnTransformator.h"
#include "src/exceptions/NotImplementedException.h"
#include <memory>
namespace storm {
namespace transformations {
namespace dft {
// Prevent some magic constants
static constexpr const uint64_t defaultPriority = 0;
static constexpr const uint64_t defaultCapacity = 0;
template <typename ValueType>
DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft) : mDft(dft) {
// Intentionally left empty.
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::transform() {
builder.setGspnName("DftToGspnTransformation");
// Loop through every DFT element and draw them as a GSPN.
drawGSPNElements();
// When all DFT elements are drawn, draw the connections between them.
drawGSPNConnections();
// Draw functional/probability dependencies into the GSPN.
drawGSPNDependencies();
// Draw restrictions into the GSPN (i.e. SEQ or MUTEX).
drawGSPNRestrictions();
// Write GSPN to file.
writeGspn(true);
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNElements() {
// Loop through every DFT element and draw them as a GSPN.
for (std::size_t i = 0; i < mDft.nrElements(); i++) {
auto dftElement = mDft.getElement(i);
// Check which type the element is and call the corresponding drawing-function.
switch (dftElement->type()) {
case storm::storage::DFTElementType::AND:
drawAND(std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::OR:
drawOR(std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::VOT:
drawVOT(std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::PAND:
drawPAND(std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::SPARE:
drawSPARE(std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::POR:
drawPOR(std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::SEQ:
// No method call needed here. SEQ only consists of restrictions, which are handled later.
break;
case storm::storage::DFTElementType::MUTEX:
// No method call needed here. MUTEX only consists of restrictions, which are handled later.
break;
case storm::storage::DFTElementType::BE:
drawBE(std::static_pointer_cast<storm::storage::DFTBE<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::CONSTF:
drawCONSTF(dftElement);
break;
case storm::storage::DFTElementType::CONSTS:
drawCONSTS(dftElement);
break;
case storm::storage::DFTElementType::PDEP:
drawPDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement));
break;
default:
STORM_LOG_ASSERT(false, "DFT type unknown.");
break;
}
}
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE) {
uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED);
uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED);
assert(failedNodes.size() == dftBE->id());
failedNodes.push_back(beFailed);
uint64_t tActive = builder.addTimedTransition(defaultPriority, dftBE->activeFailureRate(), dftBE->name() + "_activeFailing");
builder.addInputArc(beActive, tActive);
builder.addInhibitionArc(beFailed, tActive);
builder.addOutputArc(tActive, beActive);
builder.addOutputArc(tActive, beFailed);
uint64_t tPassive = builder.addTimedTransition(defaultPriority, dftBE->passiveFailureRate(), dftBE->name() + "_passiveFailing");
builder.addInhibitionArc(beActive, tPassive);
builder.addInhibitionArc(beFailed, tPassive);
builder.addOutputArc(tActive, beFailed);
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd) {
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftAnd->name() + STR_FAILED);
assert(failedNodes.size() == dftAnd->id());
failedNodes.push_back(nodeFailed);
uint64_t tAndFailed = builder.addImmediateTransition( getFailPriority(dftAnd) , 0.0, dftAnd->name() + STR_FAILING );
builder.addInhibitionArc(nodeFailed, tAndFailed);
builder.addOutputArc(tAndFailed, nodeFailed);
for(auto const& child : dftAnd->children()) {
assert(failedNodes.size() > child->id());
builder.addInputArc(failedNodes[child->id()], tAndFailed);
}
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr) {
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftOr->name() + STR_FAILED);
assert(failedNodes.size() == dftOr->id());
failedNodes.push_back(nodeFailed);
uint64_t i = 0;
for (auto const& child : dftOr->children()) {
uint64_t tNodeFailed = builder.addImmediateTransition( getFailPriority(dftOr) , 0.0, dftOr->name() + STR_FAILING + std::to_string(i) );
builder.addInhibitionArc(nodeFailed, tNodeFailed);
builder.addOutputArc(tNodeFailed, nodeFailed);
assert(failedNodes.size() > child->id());
builder.addInputArc(failedNodes[child->id()], tNodeFailed);
++i;
}
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot) {
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftVot->name() + STR_FAILED);
assert(failedNodes.size() == dftVot->id());
failedNodes.push_back(nodeFailed);
uint64_t nodeCollector = builder.addPlace(dftVot->nrChildren(), 0, dftVot->name() + "_collector");
uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING);
builder.addOutputArc(tNodeFailed, nodeFailed);
builder.addInhibitionArc(nodeFailed, tNodeFailed);
builder.addInputArc(nodeCollector, tNodeFailed, dftVot->threshold());
builder.addOutputArc(tNodeFailed, nodeCollector, dftVot->threshold());
uint64_t i = 0;
for (auto const& child : dftVot->children()) {
uint64_t childInhibPlace = builder.addPlace(1, 0, dftVot->name() + "_child_fail_inhib" + std::to_string(i));
uint64_t tCollect = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + "_child_collect" + std::to_string(i));
builder.addOutputArc(tCollect, nodeCollector);
builder.addOutputArc(tCollect, childInhibPlace);
builder.addInhibitionArc(childInhibPlace, tCollect);
builder.addInputArc(failedNodes[child->id()], tCollect);
++i;
}
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawPAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand) {
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILED);
assert(failedNodes.size() == dftPand->id());
failedNodes.push_back(nodeFailed);
uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE);
uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING);
builder.addInhibitionArc(nodeFailed, tNodeFailed);
builder.addInhibitionArc(nodeFS, tNodeFailed);
builder.addOutputArc(tNodeFailed, nodeFailed);
for(auto const& child : dftPand->children()) {
builder.addInputArc(failedNodes[child->id()], tNodeFailed);
}
for (uint64_t j = 1; j < dftPand->nrChildren(); ++j) {
uint64_t tfs = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(j));
builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs);
builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs);
builder.addOutputArc(tfs, nodeFS);
}
//
// storm::gspn::Place placePANDFailed;
// placePANDFailed.setName(dftPand->name() + STR_FAILED);
// placePANDFailed.setNumberOfInitialTokens(0);
// mGspn.addPlace(placePANDFailed);
//
// storm::gspn::Place placePANDFailsave;
// placePANDFailsave.setName(dftPand->name() + STR_FAILSAVE);
// placePANDFailsave.setNumberOfInitialTokens(0);
// mGspn.addPlace(placePANDFailsave);
//
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPANDFailing;
// immediateTransitionPANDFailing.setName(dftPand->name() + STR_FAILING);
// immediateTransitionPANDFailing.setPriority(priority);
// immediateTransitionPANDFailing.setWeight(0.0);
// immediateTransitionPANDFailing.setInhibitionArcMultiplicity(placePANDFailed, 1);
// immediateTransitionPANDFailing.setInhibitionArcMultiplicity(placePANDFailsave, 1);
// immediateTransitionPANDFailing.setOutputArcMultiplicity(placePANDFailed, 1);
// mGspn.addImmediateTransition(immediateTransitionPANDFailing);
//
// for (std::size_t i = 0; i < dftPand->nrChildren() -1; i++) {
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPANDFailsave;
// immediateTransitionPANDFailsave.setName(dftPand->name() + "_" + std::to_string(i) + STR_FAILSAVING);
// immediateTransitionPANDFailsave.setPriority(priority);
// immediateTransitionPANDFailsave.setWeight(0.0);
// immediateTransitionPANDFailsave.setInhibitionArcMultiplicity(placePANDFailsave, 1);
// immediateTransitionPANDFailsave.setOutputArcMultiplicity(placePANDFailsave, 1);
// mGspn.addImmediateTransition(immediateTransitionPANDFailsave);
// }
}
//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {
// uint_fast64_t priority = getPriority(0, dftSpare);
//
// // This codeblock can be removed later, when I am 100% sure it is not needed anymore.
// /*
// storm::gspn::Place placeSPAREActivated;
// placeSPAREActivated.setName(dftSpare->name() + STR_ACTIVATED);
// placeSPAREActivated.setNumberOfInitialTokens(isBEActive(dftSpare));
// mGspn.addPlace(placeSPAREActivated);
//
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPCActivating;
// immediateTransitionPCActivating.setName(dftSpare->children()[0]->name() + STR_ACTIVATING);
// immediateTransitionPCActivating.setPriority(priority);
// immediateTransitionPCActivating.setWeight(0.0);
// immediateTransitionPCActivating.setInputArcMultiplicity(placeSPAREActivated, 1);
// immediateTransitionPCActivating.setOutputArcMultiplicity(placeSPAREActivated, 1);
// mGspn.addImmediateTransition(immediateTransitionPCActivating);
// */
//
// auto children = dftSpare->children();
//
// // Draw places and transitions that belong to each spare child.
// for (std::size_t i = 1; i < children.size(); i++) {
// auto placeChildClaimedPreexist = mGspn.getPlace(children[i]->name() + "_claimed");
//
// if (!placeChildClaimedPreexist.first) { // Only draw this place if it doesn't exist jet.
// storm::gspn::Place placeChildClaimed;
// placeChildClaimed.setName(children[i]->name() + "_claimed");
// placeChildClaimed.setNumberOfInitialTokens(0);
// mGspn.addPlace(placeChildClaimed);
//
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionSpareChildActivating;
// immediateTransitionSpareChildActivating.setName(children[i]->name() + STR_ACTIVATING);
// immediateTransitionSpareChildActivating.setPriority(priority);
// immediateTransitionSpareChildActivating.setWeight(0.0);
// immediateTransitionSpareChildActivating.setInputArcMultiplicity(placeChildClaimed, 1);
// immediateTransitionSpareChildActivating.setOutputArcMultiplicity(placeChildClaimed, 1);
// mGspn.addImmediateTransition(immediateTransitionSpareChildActivating);
// }
//
// auto placeChildClaimedExist = mGspn.getPlace(children[i]->name() + "_claimed");
//
// storm::gspn::Place placeSPAREClaimedChild;
// placeSPAREClaimedChild.setName(dftSpare->name() + "_claimed_" + children[i]->name());
// placeSPAREClaimedChild.setNumberOfInitialTokens(0);
// mGspn.addPlace(placeSPAREClaimedChild);
//
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildClaiming;
// immediateTransitionChildClaiming.setName(dftSpare->name() + "_claiming_" + children[i]->name());
// immediateTransitionChildClaiming.setPriority(priority + 1); // Higher priority needed!
// immediateTransitionChildClaiming.setWeight(0.0);
// immediateTransitionChildClaiming.setInhibitionArcMultiplicity(placeChildClaimedExist.second, 1);
// immediateTransitionChildClaiming.setOutputArcMultiplicity(placeChildClaimedExist.second, 1);
// immediateTransitionChildClaiming.setOutputArcMultiplicity(placeSPAREClaimedChild, 1);
// mGspn.addImmediateTransition(immediateTransitionChildClaiming);
//
// storm::gspn::Place placeSPAREChildConsumed;
// if (i < children.size() - 1) {
// placeSPAREChildConsumed.setName(dftSpare->name() + "_" + children[i]->name() + "_consumed");
// }
// else {
// placeSPAREChildConsumed.setName(dftSpare->name() + STR_FAILED);
// }
// placeSPAREChildConsumed.setNumberOfInitialTokens(0);
// mGspn.addPlace(placeSPAREChildConsumed);
//
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildConsuming1;
// immediateTransitionChildConsuming1.setName(dftSpare->name() + "_" + children[i]->name() + "_consuming1");
// immediateTransitionChildConsuming1.setPriority(priority);
// immediateTransitionChildConsuming1.setWeight(0.0);
// immediateTransitionChildConsuming1.setOutputArcMultiplicity(placeSPAREChildConsumed, 1);
// immediateTransitionChildConsuming1.setInhibitionArcMultiplicity(placeSPAREChildConsumed, 1);
// immediateTransitionChildConsuming1.setInhibitionArcMultiplicity(placeSPAREClaimedChild, 1);
// mGspn.addImmediateTransition(immediateTransitionChildConsuming1);
//
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildConsuming2;
// immediateTransitionChildConsuming2.setName(dftSpare->name() + "_" + children[i]->name() + "_consuming2");
// immediateTransitionChildConsuming2.setPriority(priority);
// immediateTransitionChildConsuming2.setWeight(0.0);
// immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREChildConsumed, 1);
// immediateTransitionChildConsuming2.setInhibitionArcMultiplicity(placeSPAREChildConsumed, 1);
// immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREClaimedChild, 1);
// immediateTransitionChildConsuming2.setInputArcMultiplicity(placeSPAREClaimedChild, 1);
// mGspn.addImmediateTransition(immediateTransitionChildConsuming2);
// }
//
// // Draw connections between all spare childs.
// for (std::size_t i = 1; i < children.size() - 1; i++) {
// auto placeSPAREChildConsumed = mGspn.getPlace(dftSpare->name() + "_" + children[i]->name() + "_consumed");
// auto immediateTransitionChildClaiming = mGspn.getImmediateTransition(dftSpare->name() + "_claiming_" + children[i + 1]->name());
// auto immediateTransitionChildConsuming1 = mGspn.getImmediateTransition(dftSpare->name() + "_" + children[i + 1]->name() + "_consuming1");
//
// immediateTransitionChildClaiming.second->setOutputArcMultiplicity(placeSPAREChildConsumed.second, 1);
// immediateTransitionChildClaiming.second->setInputArcMultiplicity(placeSPAREChildConsumed.second, 1);
//
// immediateTransitionChildConsuming1.second->setOutputArcMultiplicity(placeSPAREChildConsumed.second, 1);
// immediateTransitionChildConsuming1.second->setInputArcMultiplicity(placeSPAREChildConsumed.second, 1);
// }
}
//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor) {
// uint_fast64_t priority = getPriority(0, dftPor);
//
// storm::gspn::Place placePORFailed;
// placePORFailed.setName(dftPor->name() + STR_FAILED);
// placePORFailed.setNumberOfInitialTokens(0);
// mGspn.addPlace(placePORFailed);
//
// storm::gspn::Place placePORFailsave;
// placePORFailsave.setName(dftPor->name() + STR_FAILSAVE);
// placePORFailsave.setNumberOfInitialTokens(0);
// mGspn.addPlace(placePORFailsave);
//
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPORFailing;
// immediateTransitionPORFailing.setName(dftPor->name() + STR_FAILING);
// immediateTransitionPORFailing.setPriority(priority);
// immediateTransitionPORFailing.setWeight(0.0);
// immediateTransitionPORFailing.setInhibitionArcMultiplicity(placePORFailed, 1);
// immediateTransitionPORFailing.setInhibitionArcMultiplicity(placePORFailsave, 1);
// immediateTransitionPORFailing.setOutputArcMultiplicity(placePORFailed, 1);
// mGspn.addImmediateTransition(immediateTransitionPORFailing);
//
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPORFailsave;
// immediateTransitionPORFailsave.setName(dftPor->name() + STR_FAILSAVING);
// immediateTransitionPORFailsave.setPriority(priority);
// immediateTransitionPORFailsave.setWeight(0.0);
// immediateTransitionPORFailsave.setInhibitionArcMultiplicity(placePORFailsave, 1);
// immediateTransitionPORFailsave.setOutputArcMultiplicity(placePORFailsave, 1);
// mGspn.addImmediateTransition(immediateTransitionPORFailsave);
}
//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF) {
// storm::gspn::Place placeCONSTFFailed;
// placeCONSTFFailed.setName(dftConstF->name() + STR_FAILED);
// placeCONSTFFailed.setNumberOfInitialTokens(1);
// mGspn.addPlace(placeCONSTFFailed);
}
//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS) {
// storm::gspn::Place placeCONSTSFailed;
// placeCONSTSFailed.setName(dftConstS->name() + STR_FAILED);
// placeCONSTSFailed.setNumberOfInitialTokens(0);
// placeCONSTSFailed.setCapacity(0); // It cannot contain a token, because it cannot fail.
// mGspn.addPlace(placeCONSTSFailed);
}
//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const>(dftDependency)) {
// // Only draw dependency, if it wasn't drawn before.
// std::string gateName = dftDependency->name().substr(0, dftDependency->name().find("_"));
// auto exists = mGspn.getPlace(gateName + STR_FAILED);
// if (!exists.first) {
// storm::gspn::Place placeDEPFailed;
// placeDEPFailed.setName(gateName + STR_FAILED);
// placeDEPFailed.setNumberOfInitialTokens(0);
// mGspn.addPlace(placeDEPFailed);
//
// storm::gspn::TimedTransition<double> timedTransitionDEPFailure;
// timedTransitionDEPFailure.setName(gateName + STR_FAILING);
// timedTransitionDEPFailure.setPriority(getPriority(0, dftDependency));
// timedTransitionDEPFailure.setRate(dftDependency->probability());
// timedTransitionDEPFailure.setOutputArcMultiplicity(placeDEPFailed, 1);
// timedTransitionDEPFailure.setInhibitionArcMultiplicity(placeDEPFailed, 1);
// mGspn.addTimedTransition(timedTransitionDEPFailure);
// }
}
//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNConnections() {
// // Check for every element, if they have parents (all will have at least 1, except the top event).
// for (std::size_t i = 0; i < mDft.nrElements(); i++) {
// auto child = mDft.getElement(i);
// auto parents = child->parentIds();
//
// // Draw a connection to every parent.
// for (std::size_t j = 0; j < parents.size(); j++) {
// // Check the type of the parent and act accordingly (every parent gate has different entry points...).
// switch (mDft.getElement(parents[j])->type()) {
// case storm::storage::DFTElementType::AND:
// {
// auto andEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
// if (andEntry.first && childExit.first) { // Only add arcs if the objects have been found.
// andEntry.second->setInputArcMultiplicity(childExit.second, 1);
// andEntry.second->setOutputArcMultiplicity(childExit.second, 1);
// }
// break;
// }
// case storm::storage::DFTElementType::OR:
// {
// auto orEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + STR_FAILING);
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
// if (orEntry.first && childExit.first) { // Only add arcs if the objects have been found.
// orEntry.second->setInputArcMultiplicity(childExit.second, 1);
// orEntry.second->setOutputArcMultiplicity(childExit.second, 1);
// }
// break;
// }
// case storm::storage::DFTElementType::VOT:
// {
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
// auto parentEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_collecting");
//
// if (childExit.first && parentEntry.first) { // Only add arcs if the objects have been found.
// parentEntry.second->setInputArcMultiplicity(childExit.second, 1);
// parentEntry.second->setOutputArcMultiplicity(childExit.second, 1);
// }
//
// break;
// }
// case storm::storage::DFTElementType::PAND:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(mDft.getElement(parents[j]))->children();
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
// auto pandEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
//
// if (childExit.first && pandEntry.first) { // Only add arcs if the objects have been found.
// pandEntry.second->setInputArcMultiplicity(childExit.second, 1);
// pandEntry.second->setOutputArcMultiplicity(childExit.second, 1);
//
// if (children[0] == child) { // Current element is primary child.
// auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_0" + STR_FAILSAVING);
//
// if (pandEntry2.first) {
// pandEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
// }
// }
// else { // Current element is not the primary child.
// for (std::size_t k = 1; k < children.size(); k++) {
// if (children[k] == child) {
// auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k - 1)) + STR_FAILSAVING);
// auto pandEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k)) + STR_FAILSAVING);
//
// if (pandEntry2.first) {
// pandEntry2.second->setInputArcMultiplicity(childExit.second, 1);
// pandEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
// }
//
// if (pandEntry3.first) {
// pandEntry3.second->setInhibitionArcMultiplicity(childExit.second, 1);
// }
//
// continue;
// }
// }
// }
// }
//
// break;
// }
// case storm::storage::DFTElementType::SPARE:
// {
// // Check if current child is a primary or spare child.
// auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(mDft.getElement(parents[j]))->children();
//
// if (child == children[0]) { // Primary child.
// auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
//
// std::vector<int> ids = getAllBEIDsOfElement(child);
// for (std::size_t k = 0; k < ids.size(); k++) {
// auto childEntry = mGspn.getPlace(mDft.getElement(ids[k])->name() + STR_ACTIVATED);
//
// if (spareExit.first && childEntry.first) { // Only add arcs if the objects have been found.
// spareExit.second->setInhibitionArcMultiplicity(childEntry.second, 1);
// spareExit.second->setOutputArcMultiplicity(childEntry.second, 1);
// }
// }
//
// // Draw lines from "primary child_failed" to SPARE.
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
// auto spareEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + children[1]->name());
// auto spareEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + children[1]->name() + "_consuming1");
//
// if (childExit.first && spareEntry.first && spareEntry2.first) { // Only add arcs if the objects have been found.
// spareEntry.second->setInputArcMultiplicity(childExit.second, 1);
// spareEntry.second->setOutputArcMultiplicity(childExit.second, 1);
//
// spareEntry2.second->setInputArcMultiplicity(childExit.second, 1);
// spareEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
// }
// }
// else { // A spare child.
// auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
// auto spareExit2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + child->name());
//
// std::vector<int> ids = getAllBEIDsOfElement(child);
// for (std::size_t k = 0; k < ids.size(); k++) {
// auto childEntry = mGspn.getPlace(mDft.getElement(ids[k])->name() + STR_ACTIVATED);
//
// if (spareExit.first && spareExit2.first && childEntry.first) { // Only add arcs if the objects have been found.
// if (!spareExit.second->existsInhibitionArc(childEntry.second)) {
// spareExit.second->setInhibitionArcMultiplicity(childEntry.second, 1);
// }
// if (!spareExit.second->existsOutputArc(childEntry.second)) {
// spareExit.second->setOutputArcMultiplicity(childEntry.second, 1);
// }
// if (!spareExit2.second->existsInhibitionArc(childEntry.second)) {
// spareExit2.second->setInhibitionArcMultiplicity(childEntry.second, 1);
// }
// }
// }
//
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
// auto spareEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + child->name());
// auto spareEntry2 = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
// auto spareEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_consuming2");
//
// if (childExit.first && spareEntry.first && spareEntry2.first && spareEntry3.first) { // Only add arcs if the objects have been found.
// spareEntry.second->setInhibitionArcMultiplicity(childExit.second, 1);
//
// if (!spareEntry2.second->existsInhibitionArc(childExit.second)) {
// spareEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
// }
//
// spareEntry3.second->setInputArcMultiplicity(childExit.second, 1);
// spareEntry3.second->setOutputArcMultiplicity(childExit.second, 1);
// }
// }
//
// break;
// }
// case storm::storage::DFTElementType::POR:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(mDft.getElement(parents[j]))->children();
// auto porEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
// auto porEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILSAVING);
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
//
// if (porEntry.first && porEntry2.first && childExit.first) { // Only add arcs if the objects have been found.
// if (children[0] == child) { // Current element is primary child.
// porEntry.second->setInputArcMultiplicity(childExit.second, 1);
// porEntry.second->setOutputArcMultiplicity(childExit.second, 1);
// porEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
//
// }
// else { // Current element is not the primary child.
// porEntry2.second->setInputArcMultiplicity(childExit.second, 1);
// porEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
// }
// }
//
// break;
// }
// case storm::storage::DFTElementType::SEQ:
// {
// // Sequences are realized with restrictions. Nothing to do here.
// break;
// }
// case storm::storage::DFTElementType::MUTEX:
// {
// // MUTEX are realized with restrictions. Nothing to do here.
// break;
// }
// case storm::storage::DFTElementType::BE:
// {
// // The parent is never a Basic Event.
// break;
// }
// case storm::storage::DFTElementType::CONSTF:
// {
// // The parent is never a Basic Event.
// break;
// }
// case storm::storage::DFTElementType::CONSTS:
// {
// // The parent is never a Basic Event.
// break;
// }
// case storm::storage::DFTElementType::PDEP:
// {
// // The parent is never a DEP. Hence the connections must be drawn somewhere else.
// break;
// }
// default:
// {
// STORM_LOG_ASSERT(false, "DFT type unknown.");
// break;
// }
// }
// }
// }
}
template <typename ValueType>
bool DftToGspnTransformator<ValueType>::isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement)
{
// If element is the top element, return true.
if (dftElement->id() == mDft.getTopLevelIndex()) {
return true;
}
else { // Else look at all parents.
auto parents = dftElement->parents();
std::vector<bool> pathValidities;
for (std::size_t i = 0; i < parents.size(); i++) {
// Add all parents to the vector, except if the parent is a SPARE and the current element is an inactive child of the SPARE.
if (parents[i]->type() == storm::storage::DFTElementType::SPARE) {
auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(parents[i])->children();
if (children[0]->id() != dftElement->id()) {
continue;
}
}
pathValidities.push_back(isBEActive(parents[i]));
}
// Check all vector entries. If one is true, a "valid" path has been found.
for (std::size_t i = 0; i < pathValidities.size(); i++) {
if (pathValidities[i]) {
return true;
}
}
}
// No "valid" path found. BE is inactive.
return false;
}
template <typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement)
{
return mDft.maxRank() - dftElement->rank();
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNDependencies() {
// for (std::size_t i = 0; i < mDft.nrElements(); i++) {
// auto dftElement = mDft.getElement(i);
//
// if (dftElement->isDependency()) {
// std::string gateName = dftElement->name().substr(0, dftElement->name().find("_"));
// auto depEntry = mGspn.getTimedTransition(gateName + STR_FAILING);
// auto trigger = mGspn.getPlace(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement)->nameTrigger() + STR_FAILED);
//
// if (depEntry.first && trigger.first) { // Only add arcs if the objects have been found.
// if (!depEntry.second->existsInputArc(trigger.second)) {
// depEntry.second->setInputArcMultiplicity(trigger.second, 1);
// }
// if (!depEntry.second->existsOutputArc(trigger.second)){
// depEntry.second->setOutputArcMultiplicity(trigger.second, 1);
// }
// }
//
// auto dependent = mGspn.getPlace(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement)->nameDependent() + STR_FAILED);
//
// if (dependent.first) { // Only add arcs if the objects have been found.
// depEntry.second->setOutputArcMultiplicity(dependent.second, 1);
// }
// }
// }
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() {
// for (std::size_t i = 0; i < mDft.nrElements(); i++) {
// auto dftElement = mDft.getElement(i);
//
// if (dftElement->isRestriction()) {
// switch (dftElement->type()) {
// case storm::storage::DFTElementType::SEQ:
// {
// auto children = mDft.getRestriction(i)->children();
//
// for (std::size_t j = 0; j < children.size() - 1; j++) {
// auto suppressor = mGspn.getPlace(children[j]->name() + STR_FAILED);
//
// switch (children[j + 1]->type()) {
// case storm::storage::DFTElementType::BE: // If suppressed is a BE, add 2 arcs to timed transitions.
// {
// auto suppressedActive = mGspn.getTimedTransition(children[j + 1]->name() + "_activeFailing");
// auto suppressedPassive = mGspn.getTimedTransition(children[j + 1]->name() + "_passiveFailing");
//
// if (suppressor.first && suppressedActive.first && suppressedPassive.first) { // Only add arcs if the objects have been found.
// suppressedActive.second->setInputArcMultiplicity(suppressor.second, 1);
// suppressedActive.second->setOutputArcMultiplicity(suppressor.second, 1);
// suppressedPassive.second->setInputArcMultiplicity(suppressor.second, 1);
// suppressedPassive.second->setOutputArcMultiplicity(suppressor.second, 1);
// }
// break;
// }
// default: // If supressed is not a BE, add single arc to immediate transition.
// {
// auto suppressed = mGspn.getImmediateTransition(children[j + 1]->name() + STR_FAILING);
//
// if (suppressor.first && suppressed.first) { // Only add arcs if the objects have been found.
// suppressed.second->setInputArcMultiplicity(suppressor.second, 1);
// suppressed.second->setOutputArcMultiplicity(suppressor.second, 1);
// }
// break;
// }
// }
// }
// break;
// }
// case storm::storage::DFTElementType::MUTEX:
// {
// // MUTEX is not implemented by the DFTGalileoParser yet. Nothing to do here.
// STORM_LOG_ASSERT(false, "MUTEX is not supported by DftToGspnTransformator.");
// break;
// }
// default:
// {
// break;
// }
// }
// }
// }
}
template <typename ValueType>
std::vector<int> DftToGspnTransformator<ValueType>::getAllBEIDsOfElement(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
// std::vector<int> ids;
//
// switch (dftElement->type()) {
// case storm::storage::DFTElementType::AND:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement)->children();
//
// for (std::size_t i = 0; i < children.size(); i++) {
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::OR:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement)->children();
//
// for (std::size_t i = 0; i < children.size(); i++) {
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::VOT:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement)->children();
//
// for (std::size_t i = 0; i < children.size(); i++) {
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::PAND:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement)->children();
//
// for (std::size_t i = 0; i < children.size(); i++) {
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::SPARE:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement)->children();
//
// // Only regard the primary child of a SPARE. The spare childs are not allowed to be listed here.
// for (std::size_t i = 0; i < 1; i++) {
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::POR:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement)->children();
//
// for (std::size_t i = 0; i < children.size(); i++) {
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::BE:
// case storm::storage::DFTElementType::CONSTF:
// case storm::storage::DFTElementType::CONSTS:
// {
// ids.push_back(dftElement->id());
// break;
// }
// case storm::storage::DFTElementType::SEQ:
// case storm::storage::DFTElementType::MUTEX:
// case storm::storage::DFTElementType::PDEP:
// {
// break;
// }
// default:
// {
// STORM_LOG_ASSERT(false, "DFT type unknown.");
// break;
// }
// }
//
// return ids;
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::writeGspn(bool toFile) {
if (toFile) {
// Writing to file
std::ofstream file;
file.open("gspn.dot");
storm::gspn::GSPN* gspn = builder.buildGspn();
gspn->writeDotToStream(file);
delete gspn;
file.close();
} else {
// Writing to console
storm::gspn::GSPN* gspn = builder.buildGspn();
gspn->writeDotToStream(std::cout);
delete gspn;
}
}
// Explicitly instantiate the class.
template class DftToGspnTransformator<double>;
#ifdef STORM_HAVE_CARL
// template class DftToGspnTransformator<storm::RationalFunction>;
#endif
} // namespace dft
} // namespace transformations
} // namespace storm

170
src/transformations/dft/DftToGspnTransformator.h
View File

@ -1,170 +0,0 @@
#pragma once
#include <src/storage/dft/DFT.h>
#include "src/storage/gspn/GSPN.h"
#include "src/storage/gspn/GspnBuilder.h"
namespace storm {
namespace transformations {
namespace dft {
/*!
* Transformator for DFT -> GSPN.
*/
template<typename ValueType>
class DftToGspnTransformator {
public:
/*!
* Constructor.
*
* @param dft DFT
*/
DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft);
/*!
* Transform the DFT to a GSPN.
*/
void transform();
private:
/*!
* Write Gspn to file or console.
*
* @param toFile If true, the GSPN will be written to a file, otherwise it will
be written to the console.
*/
void writeGspn(bool toFile);
/*
* Draw all elements of the GSPN.
*/
void drawGSPNElements();
/*
* Draw the connections between the elements of the GSPN.
*/
void drawGSPNConnections();
/*
* Draw functional/probability dependencies into the GSPN.
*/
void drawGSPNDependencies();
/*
* Draw restrictions between the elements of the GSPN (i.e. SEQ or MUTEX).
*/
void drawGSPNRestrictions();
/*
* Draw a Petri net Basic Event.
*
* @param dftBE The Basic Event.
*/
void drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE);
/*
* Draw a Petri net AND.
*
* @param dftAnd The AND gate.
*/
void drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd);
/*
* Draw a Petri net OR.
*
* @param dftOr The OR gate.
*/
void drawOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr);
/*
* Draw a Petri net VOT.
*
* @param dftVot The VOT gate.
*/
void drawVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot);
/*
* Draw a Petri net PAND.
* This PAND is inklusive (children are allowed to fail simultaneously and the PAND will fail nevertheless).
*
* @param dftPand The PAND gate.
*/
void drawPAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand);
/*
* Draw a Petri net SPARE.
*
* @param dftSpare The SPARE gate.
*/
void drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare);
/*
* Draw a Petri net POR.
* This POR is inklusive (children are allowed to fail simultaneously and the POR will fail nevertheless).
*
* @param dftPor The POR gate.
*/
void drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor);
/*
* Draw a Petri net CONSTF (Constant Failure, a Basic Event that has already failed).
*
* @param dftPor The CONSTF Basic Event.
*/
void drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF);
/*
* Draw a Petri net CONSTS (Constant Save, a Basic Event that cannot fail).
*
* @param dftPor The CONSTS Basic Event.
*/
void drawCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS);
/*
* Draw a Petri net PDEP (FDEP is included with a firerate of 1).
*/
void drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const>(dftDependency));
/*
* Return true if BE is active (corresponding place contains one initial token) or false if BE is inactive (corresponding place contains no initial token).
*
* @param dFTElement DFT element.
*/
bool isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement);
/*
* Get the priority of the element.
* The priority is two times the length of the shortest path to the top event.
*
* @param priority The priority of the gate. Top Event has priority 0, its children 2, its grandchildren 4, ...
*
* @param dftElement The element whose priority shall be determined.
*/
uint64_t getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement);
/*
* Return all ids of BEs, that are successors of the given element and that are not the spare childs of a SPARE.
*
* @param dftElement The element which
*/
std::vector<int> getAllBEIDsOfElement(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement);
storm::storage::DFT<ValueType> const& mDft;
storm::gspn::GspnBuilder builder;
std::vector<uint64_t> failedNodes;
static constexpr const char* STR_FAILING = "_failing"; // Name standard for transitions that point towards a place, which in turn indicates the failure of a gate.
static constexpr const char* STR_FAILED = "_failed"; // Name standard for place which indicates the failure of a gate.
static constexpr const char* STR_FAILSAVING = "_failsaving"; // Name standard for transition that point towards a place, which in turn indicates the failsave state of a gate.
static constexpr const char* STR_FAILSAVE = "_failsave"; // Name standard for place which indicates the failsave state of a gate.
static constexpr const char* STR_ACTIVATED = "_activated"; // Name standard for place which indicates the activity.
static constexpr const char* STR_ACTIVATING = "_activating"; // Name standard for transition that point towards a place, which in turn indicates its activity.
};
}
}
}
Write Preview
Loading…
Cancel
Save