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

initial support for seq in dft->gspn

tempestpy_adaptions
Sebastian Junges 8 years ago
parent
0bf00ff7ac
commit
92584d577f
3 changed files with 58 additions and 24 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. 9
      src/storm-dft/storage/dft/elements/DFTRestriction.h
  2. 65
      src/storm-dft/transformations/DftToGspnTransformator.cpp
  3. 8
      src/storm-dft/transformations/DftToGspnTransformator.h

9
src/storm-dft/storage/dft/elements/DFTRestriction.h
View File

@ -36,6 +36,15 @@ namespace storm {
virtual bool isSeqEnforcer() const {
return false;
}
bool allChildrenBEs() const {
for(auto const& elem : mChildren) {
if (!elem->isBasicElement()) {
return false;
}
}
return true;
}
virtual std::string typestring() const = 0;

65
src/storm-dft/transformations/DftToGspnTransformator.cpp
View File

@ -63,8 +63,8 @@ namespace storm {
drawPOR(std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement), isRepresentative);
break;
case storm::storage::DFTElementType::SEQ:
// No method call needed here. SEQ only consists of restrictions, which are handled later.
break;
drawSeq(std::static_pointer_cast<storm::storage::DFTSeq<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::MUTEX:
// No method call needed here. MUTEX only consists of restrictions, which are handled later.
break;
@ -78,7 +78,7 @@ namespace storm {
drawCONSTS(dftElement, isRepresentative);
break;
case storm::storage::DFTElementType::PDEP:
drawPDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement), isRepresentative);
drawPDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement));
break;
default:
STORM_LOG_ASSERT(false, "DFT type unknown.");
@ -96,9 +96,13 @@ namespace storm {
activeNodes.emplace(dftBE->id(), beActive);
uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED);
uint64_t disabledNode = 0;
if (!smart || dftBE->nrRestrictions() > 0) {
disabledNode = addDisabledPlace(dftBE);
}
uint64_t unavailableNode = 0;
if (isRepresentative) {
if (!smart || isRepresentative) {
unavailableNode = addUnavailableNode(dftBE);
}
@ -114,7 +118,12 @@ namespace storm {
builder.addInhibitionArc(beFailed, tPassive);
builder.addOutputArc(tPassive, beFailed);
if (isRepresentative) {
if (!smart || dftBE->nrRestrictions() > 0) {
builder.addInhibitionArc(disabledNode, tActive);
builder.addInhibitionArc(disabledNode, tPassive);
}
if (!smart || isRepresentative) {
builder.addOutputArc(tActive, unavailableNode);
builder.addOutputArc(tPassive, unavailableNode);
}
@ -350,26 +359,29 @@ namespace storm {
}
//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency, bool isRepresentative) {
// // 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);
// }
void DftToGspnTransformator<ValueType>::drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency) {
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawSeq(std::shared_ptr<storm::storage::DFTSeq<ValueType> const> dftSeq) {
STORM_LOG_THROW(dftSeq->allChildrenBEs(), storm::exceptions::NotImplementedException, "Sequence enforcers with gates as children are currently not supported");
bool first = true;
uint64_t tEnable = 0;
uint64_t nextPlace = 0;
for(auto const& child : dftSeq->children()) {
nextPlace = builder.addPlace(defaultCapacity, first ? 1 : 0, dftSeq->name() + "_next_" + child->name());
if(!first) {
builder.addOutputArc(tEnable, nextPlace);
}
tEnable = builder.addImmediateTransition(defaultPriority, 0.0, dftSeq->name() + "_unblock_" +child->name() );
builder.addInputArc(nextPlace, tEnable);
builder.addInputArc(disabledNodes.at(child->id()), tEnable);
first = false;
}
}
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, bool initialAvailable) {
uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavailable");
@ -377,6 +389,13 @@ namespace storm {
unavailableNodes.emplace(dftElement->id(), unavailableNode);
return unavailableNode;
}
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::addDisabledPlace(std::shared_ptr<const storm::storage::DFTBE<ValueType> > dftBe) {
uint64_t disabledNode = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(), dftBe->name() + "_dabled");
disabledNodes.emplace(dftBe->id(), disabledNode);
return disabledNode;
}
//
template <typename ValueType>

8
src/storm-dft/transformations/DftToGspnTransformator.h
View File

@ -114,8 +114,10 @@ namespace storm {
/*
* Draw a Petri net PDEP (FDEP is included with a firerate of 1).
*/
void drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency, bool isRepresentative);
void drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency);
void drawSeq(std::shared_ptr<storm::storage::DFTSeq<ValueType> const> dftSeq);
/*
* Return true if BE is active (corresponding place contains one initial token) or false if BE is inactive (corresponding place contains no initial token).
*
@ -136,11 +138,15 @@ namespace storm {
uint64_t addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, bool initialAvailable = true);
uint64_t addDisabledPlace(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBe);
storm::storage::DFT<ValueType> const& mDft;
storm::gspn::GspnBuilder builder;
std::vector<uint64_t> failedNodes;
std::map<uint64_t, uint64_t> unavailableNodes;
std::map<uint64_t, uint64_t> activeNodes;
std::map<uint64_t, uint64_t> disabledNodes;
bool smart = true;
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.

Write Preview
Loading…
Cancel
Save