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

Added option for merging DC and Failed places

tempestpy_adaptions
Matthias Volk 7 years ago
parent
ad8350c684
commit
0674f88cf5
3 changed files with 158 additions and 147 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. 4
      src/storm-dft/api/storm-dft.cpp
  2. 297
      src/storm-dft/transformations/DftToGspnTransformator.cpp
  3. 4
      src/storm-dft/transformations/DftToGspnTransformator.h

4
src/storm-dft/api/storm-dft.cpp
View File

@ -29,7 +29,9 @@ namespace storm {
template<>
void transformToGSPN(storm::storage::DFT<double> const& dft) {
// TODO make choosable
bool smart = true;
bool mergeDCFailed = true;
// Set Don't Care elements
std::set<uint64_t> dontCareElements;
@ -43,7 +45,7 @@ namespace storm {
// Transform to GSPN
storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(dft);
gspnTransformator.transform(dontCareElements, smart);
gspnTransformator.transform(dontCareElements, smart, mergeDCFailed);
storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();

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

@ -5,48 +5,49 @@
namespace storm {
namespace transformations {
namespace dft {
// Prevent some magic constants
static constexpr const uint64_t defaultPriority = 1;
static constexpr const uint64_t defaultCapacity = 1;
template <typename ValueType>
DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft) : mDft(dft) {
template<typename ValueType>
DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::storage::DFT<ValueType> const &dft) : mDft(dft) {
// Intentionally left empty.
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::transform(std::set<uint64_t> const& dontCareElements, bool smart) {
template<typename ValueType>
void DftToGspnTransformator<ValueType>::transform(std::set<uint64_t> const &dontCareElements, bool smart, bool mergeDCFailed) {
this->dontCareElements = dontCareElements;
this->smart = smart;
this->mergedDCFailed = mergeDCFailed;
builder.setGspnName("DftToGspnTransformation");
// Translate all GSPN elements
// Translate all GSPN elements
translateGSPNElements();
// Create initial template
// TODO
}
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::toplevelFailedPlaceId() {
STORM_LOG_ASSERT(failedPlaces.size() > mDft.getTopLevelIndex(), "Failed place for top level element does not exist.");
return failedPlaces.at(mDft.getTopLevelIndex());
}
template <typename ValueType>
gspn::GSPN* DftToGspnTransformator<ValueType>::obtainGSPN() {
template<typename ValueType>
gspn::GSPN *DftToGspnTransformator<ValueType>::obtainGSPN() {
return builder.buildGspn();
}
template <typename ValueType>
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateGSPNElements() {
// Loop through every DFT element and create its corresponding GSPN template.
// Loop through every DFT element and create its corresponding GSPN template.
for (std::size_t i = 0; i < mDft.nrElements(); i++) {
auto dftElement = mDft.getElement(i);
auto dftElement = mDft.getElement(i);
// Check which type the element is and call the corresponding translate-function.
switch (dftElement->type()) {
// Check which type the element is and call the corresponding translate-function.
switch (dftElement->type()) {
case storm::storage::DFTElementType::BE:
translateBE(std::static_pointer_cast<storm::storage::DFTBE<ValueType> const>(dftElement));
break;
@ -57,38 +58,40 @@ namespace storm {
translateCONSTS(dftElement);
break;
case storm::storage::DFTElementType::AND:
translateAND(std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::OR:
translateOR(std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::VOT:
translateVOT(std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::PAND:
translatePAND(std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement), std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement)->isInclusive());
break;
translateAND(std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::OR:
translateOR(std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::VOT:
translateVOT(std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::PAND:
translatePAND(std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement),
std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement)->isInclusive());
break;
case storm::storage::DFTElementType::POR:
translatePOR(std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement), std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement)->isInclusive());
translatePOR(std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement),
std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement)->isInclusive());
break;
case storm::storage::DFTElementType::SPARE:
translateSPARE(std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::SPARE:
translateSPARE(std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::PDEP:
translatePDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::SEQ:
case storm::storage::DFTElementType::SEQ:
translateSeq(std::static_pointer_cast<storm::storage::DFTSeq<ValueType> const>(dftElement));
break;
default:
STORM_LOG_ASSERT(false, "DFT type " << dftElement->type() << " unknown.");
break;
}
}
}
template <typename ValueType>
default:
STORM_LOG_ASSERT(false, "DFT type " << dftElement->type() << " unknown.");
break;
}
}
}
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE) {
double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y;
@ -111,21 +114,21 @@ namespace storm {
builder.addInhibitionArc(activePlace, tPassive);
builder.addInhibitionArc(failedPlace, tPassive);
builder.addOutputArc(tPassive, failedPlace);
if (!smart || dftBE->nrRestrictions() > 0) {
uint64_t disabledPlace = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter-9.0, ycenter));
uint64_t disabledPlace = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter - 9.0, ycenter));
builder.addInhibitionArc(disabledPlace, tActive);
builder.addInhibitionArc(disabledPlace, tPassive);
}
if (!smart || mDft.isRepresentative(dftBE->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftBE, storm::gspn::LayoutInfo(xcenter+9.0, ycenter));
uint64_t unavailablePlace = addUnavailablePlace(dftBE, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter));
builder.addOutputArc(tActive, unavailablePlace);
builder.addOutputArc(tPassive, unavailablePlace);
}
}
template <typename ValueType>
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF) {
double xcenter = mDft.getElementLayoutInfo(dftConstF->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftConstF->id()).y;
@ -137,7 +140,7 @@ namespace storm {
}
}
template <typename ValueType>
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS) {
double xcenter = mDft.getElementLayoutInfo(dftConstS->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftConstS->id()).y;
@ -156,46 +159,46 @@ namespace storm {
}
}
template <typename ValueType>
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd) {
double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y;
uint64_t failedPlace = addFailedPlace(dftAnd, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
uint64_t failedPlace = addFailedPlace(dftAnd, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftAnd), 0.0, dftAnd->name() + STR_FAILING );
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftAnd), 0.0, dftAnd->name() + STR_FAILING);
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0));
builder.addInhibitionArc(failedPlace, tFailed);
builder.addOutputArc(tFailed, failedPlace);
if (!smart || mDft.isRepresentative(dftAnd->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftAnd, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
uint64_t unavailablePlace = addUnavailablePlace(dftAnd, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0));
builder.addOutputArc(tFailed, unavailablePlace);
}
for (auto const& child : dftAnd->children()) {
for (auto const &child : dftAnd->children()) {
builder.addInputArc(getFailedPlace(child), tFailed);
builder.addOutputArc(tFailed, getFailedPlace(child));
}
}
}
template <typename ValueType>
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr) {
double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y;
uint64_t failedPlace = addFailedPlace(dftOr, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
uint64_t failedPlace = addFailedPlace(dftOr, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
bool isRepresentative = mDft.isRepresentative(dftOr->id());
uint64_t unavailablePlace = 0;
if (!smart || isRepresentative) {
unavailablePlace = addUnavailablePlace(dftOr, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
unavailablePlace = addUnavailablePlace(dftOr, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0));
}
for (size_t i = 0; i < dftOr->nrChildren(); ++i) {
auto const& child = dftOr->children().at(i);
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftOr), 0.0, dftOr->name() + STR_FAILING + std::to_string(i) );
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0));
for (size_t i = 0; i < dftOr->nrChildren(); ++i) {
auto const &child = dftOr->children().at(i);
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftOr), 0.0, dftOr->name() + STR_FAILING + std::to_string(i));
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter + 3.0));
builder.addInhibitionArc(failedPlace, tFailed);
builder.addOutputArc(tFailed, failedPlace);
if (!smart || isRepresentative) {
@ -204,23 +207,23 @@ namespace storm {
builder.addInputArc(getFailedPlace(child), tFailed);
builder.addOutputArc(tFailed, getFailedPlace(child));
}
}
template <typename ValueType>
}
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot) {
// TODO: finish layouting
double xcenter = mDft.getElementLayoutInfo(dftVot->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftVot->id()).y;
uint64_t failedPlace = addFailedPlace(dftVot, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
uint64_t failedPlace = addFailedPlace(dftVot, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING);
builder.addOutputArc(tFailed, failedPlace);
builder.addInhibitionArc(failedPlace, tFailed);
if (!smart || mDft.isRepresentative(dftVot->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftVot, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
uint64_t unavailablePlace = addUnavailablePlace(dftVot, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0));
builder.addOutputArc(tFailed, unavailablePlace);
}
@ -228,8 +231,8 @@ namespace storm {
builder.setPlaceLayoutInfo(collectorPlace, storm::gspn::LayoutInfo(xcenter, ycenter));
builder.addInputArc(collectorPlace, tFailed, dftVot->threshold());
for (size_t i = 0; i < dftVot->nrChildren(); ++i) {
auto const& child = dftVot->children().at(i);
for (size_t i = 0; i < dftVot->nrChildren(); ++i) {
auto const &child = dftVot->children().at(i);
uint64_t childNextPlace = builder.addPlace(defaultCapacity, 1, dftVot->name() + "_child_next" + std::to_string(i));
uint64_t tCollect = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + "_child_collect" + std::to_string(i));
@ -238,46 +241,46 @@ namespace storm {
builder.addInputArc(getFailedPlace(child), tCollect);
builder.addOutputArc(tCollect, getFailedPlace(child));
}
}
}
template <typename ValueType>
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translatePAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool inclusive) {
double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y;
uint64_t failedPlace = addFailedPlace(dftPand, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0));
uint64_t failedPlace = addFailedPlace(dftPand, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter - 3.0));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING);
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING);
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter + 3.0));
builder.addInhibitionArc(failedPlace, tFailed);
builder.addOutputArc(tFailed, failedPlace);
if (!smart || mDft.isRepresentative(dftPand->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftPand, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0));
uint64_t unavailablePlace = addUnavailablePlace(dftPand, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter - 3.0));
builder.addOutputArc(tFailed, unavailablePlace);
}
if (inclusive) {
// Inclusive PAND
uint64_t failSafePlace = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE);
builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0));
builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter - 3.0));
builder.addInhibitionArc(failSafePlace, tFailed);
// Transitions for failed place
for (auto const& child : dftPand->children()) {
for (auto const &child : dftPand->children()) {
builder.addInputArc(getFailedPlace(child), tFailed);
builder.addOutputArc(tFailed, getFailedPlace(child));
}
// Transitions for fail-safe place
for (uint64_t i = 1; i < dftPand->nrChildren(); ++i) {
auto const& child = dftPand->children().at(i);
auto const &child = dftPand->children().at(i);
uint64_t tFailSafe = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(i));
builder.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter-6.0+i*3.0, ycenter+3.0));
builder.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter - 6.0 + i * 3.0, ycenter + 3.0));
builder.addInputArc(getFailedPlace(child), tFailSafe);
builder.addOutputArc(tFailSafe, getFailedPlace(child));
builder.addInhibitionArc(getFailedPlace(dftPand->children().at(i-1)), tFailSafe);
builder.addInhibitionArc(getFailedPlace(dftPand->children().at(i - 1)), tFailSafe);
builder.addOutputArc(tFailSafe, failSafePlace);
builder.addInhibitionArc(failSafePlace, tFailSafe);
}
@ -286,7 +289,7 @@ namespace storm {
uint64_t failSafeXPlace = 0;
uint64_t tFailSafeX = 0;
for (size_t i = 0; i < dftPand->nrChildren(); ++i) {
auto const& child = dftPand->children().at(i);
auto const &child = dftPand->children().at(i);
if (i > 0) {
// Set inhibition arc to previous transition
@ -295,8 +298,8 @@ namespace storm {
if (i < dftPand->nrChildren() - 1) {
// Not last child
tFailSafeX = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(i));
builder.setTransitionLayoutInfo(tFailSafeX, storm::gspn::LayoutInfo(xcenter-3.0, ycenter+3.0));
tFailSafeX = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" + std::to_string(i));
builder.setTransitionLayoutInfo(tFailSafeX, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter + 3.0));
} else {
// Last child
tFailSafeX = tFailed;
@ -311,7 +314,7 @@ namespace storm {
if (i < dftPand->nrChildren() - 1) {
// Add fail-safe X place
failSafeXPlace = builder.addPlace(defaultCapacity, 0, dftPand->name() + "_F_" + std::to_string(i));
builder.setPlaceLayoutInfo(failSafeXPlace, storm::gspn::LayoutInfo(xcenter-3.0+i*3.0, ycenter));
builder.setPlaceLayoutInfo(failSafeXPlace, storm::gspn::LayoutInfo(xcenter - 3.0 + i * 3.0, ycenter));
builder.addOutputArc(tFailSafeX, failSafeXPlace);
builder.addInhibitionArc(failSafeXPlace, tFailSafeX);
}
@ -319,15 +322,15 @@ namespace storm {
}
}
template <typename ValueType>
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translatePOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool inclusive) {
double xcenter = mDft.getElementLayoutInfo(dftPor->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftPor->id()).y;
uint64_t failedPlace = addFailedPlace(dftPor, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0));
uint64_t failedPlace = addFailedPlace(dftPor, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter - 3.0));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILING);
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0));
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter + 3.0));
builder.addOutputArc(tFailed, failedPlace);
builder.addInhibitionArc(failedPlace, tFailed);
@ -336,22 +339,22 @@ namespace storm {
builder.addOutputArc(tFailed, getFailedPlace(dftPor->children().front()));
if (!smart || mDft.isRepresentative(dftPor->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftPor, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0));
uint64_t unavailablePlace = addUnavailablePlace(dftPor, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter - 3.0));
builder.addOutputArc(tFailed, unavailablePlace);
}
if (inclusive) {
// Inclusive POR
uint64_t failSafePlace = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE);
builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0));
builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter - 3.0));
builder.addInhibitionArc(failSafePlace, tFailed);
// For all children except the first one
for (size_t i = 1; i < dftPor->nrChildren(); ++i) {
auto const& child = dftPor->children().at(i);
auto const &child = dftPor->children().at(i);
uint64_t tFailSafe = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(i));
builder.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter-3.0+i*3.0, ycenter+3.0));
builder.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter - 3.0 + i * 3.0, ycenter + 3.0));
builder.addInputArc(getFailedPlace(child), tFailSafe);
builder.addOutputArc(tFailSafe, getFailedPlace(child));
@ -363,38 +366,38 @@ namespace storm {
// Exclusive POR
// For all children except the first one
for (auto const& child : dftPor->children()) {
for (auto const &child : dftPor->children()) {
builder.addInhibitionArc(getFailedPlace(child), tFailed);
}
}
}
template <typename ValueType>
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {
double xcenter = mDft.getElementLayoutInfo(dftSpare->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftSpare->id()).y;
uint64_t failedPlace = addFailedPlace(dftSpare, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0));
uint64_t failedPlace = addFailedPlace(dftSpare, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
bool isRepresentative = mDft.isRepresentative(dftSpare->id());
uint64_t unavailablePlace = 0;
if (!smart || isRepresentative) {
unavailablePlace = addUnavailablePlace(dftSpare, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0));
unavailablePlace = addUnavailablePlace(dftSpare, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0));
}
uint64_t activePlace = builder.addPlace(defaultCapacity, isActiveInitially(dftSpare) ? 1 : 0, dftSpare->name() + STR_ACTIVATED);
builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter-20.0, ycenter-12.0));
builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter - 20.0, ycenter - 12.0));
activePlaces.emplace(dftSpare->id(), activePlace);
std::vector<uint64_t> tNextClaims;
std::vector<uint64_t> tNextConsiders;
for (size_t i = 0; i < dftSpare->nrChildren(); ++i) {
auto const& child = dftSpare->children().at(i);
auto const &child = dftSpare->children().at(i);
// Consider next child
size_t considerPlace = builder.addPlace(defaultCapacity, i == 0 ? 1 : 0, dftSpare->name()+ "_consider_" + child->name());
builder.setPlaceLayoutInfo(considerPlace, storm::gspn::LayoutInfo(xcenter-15.0+i*14.0, ycenter-8.0));
size_t considerPlace = builder.addPlace(defaultCapacity, i == 0 ? 1 : 0, dftSpare->name() + "_consider_" + child->name());
builder.setPlaceLayoutInfo(considerPlace, storm::gspn::LayoutInfo(xcenter - 15.0 + i * 14.0, ycenter - 8.0));
if (i > 0) {
// Set output transition from previous next_claim
@ -405,7 +408,7 @@ namespace storm {
// Cannot claim child
uint64_t tConsiderNext = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_cannot_claim_" + child->name());
builder.setTransitionLayoutInfo(tConsiderNext, storm::gspn::LayoutInfo(xcenter-7.0+i*14.0, ycenter-8.0));
builder.setTransitionLayoutInfo(tConsiderNext, storm::gspn::LayoutInfo(xcenter - 7.0 + i * 14.0, ycenter - 8.0));
builder.addInputArc(considerPlace, tConsiderNext);
builder.addInputArc(unavailablePlaces.at(child->id()), tConsiderNext);
builder.addOutputArc(tConsiderNext, unavailablePlaces.at(child->id()));
@ -413,9 +416,9 @@ namespace storm {
// Claimed child
size_t claimedPlace = builder.addPlace(defaultCapacity, 0, dftSpare->name() + "_claimed_" + child->name());
builder.setPlaceLayoutInfo(claimedPlace, storm::gspn::LayoutInfo(xcenter-15.0+i*14.0, ycenter+5.0));
builder.setPlaceLayoutInfo(claimedPlace, storm::gspn::LayoutInfo(xcenter - 15.0 + i * 14.0, ycenter + 5.0));
uint64_t tClaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name());
builder.setTransitionLayoutInfo(tClaim, storm::gspn::LayoutInfo(xcenter-15.0+i*14.0, ycenter));
builder.setTransitionLayoutInfo(tClaim, storm::gspn::LayoutInfo(xcenter - 15.0 + i * 14.0, ycenter));
builder.addInhibitionArc(unavailablePlaces.at(child->id()), tClaim);
builder.addInputArc(considerPlace, tClaim);
builder.addOutputArc(tClaim, claimedPlace);
@ -423,7 +426,7 @@ namespace storm {
// Claim next
uint64_t tClaimNext = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_next_claim_" + std::to_string(i));
builder.setTransitionLayoutInfo(tClaimNext, storm::gspn::LayoutInfo(xcenter-7.0+i*14.0, ycenter+5.0));
builder.setTransitionLayoutInfo(tClaimNext, storm::gspn::LayoutInfo(xcenter - 7.0 + i * 14.0, ycenter + 5.0));
builder.addInputArc(claimedPlace, tClaimNext);
builder.addInputArc(getFailedPlace(child), tClaimNext);
builder.addOutputArc(tClaimNext, getFailedPlace(child));
@ -432,8 +435,8 @@ namespace storm {
// Activate all elements in spare module
uint64_t l = 0;
for (uint64_t k : mDft.module(child->id())) {
uint64_t tActivate = builder.addImmediateTransition(defaultPriority, 0.0, dftSpare->name() + "_activate_" + std::to_string(i) + "_" + std::to_string(k));
builder.setTransitionLayoutInfo(tActivate, storm::gspn::LayoutInfo(xcenter-18.0+(i+l)*3, ycenter-12.0));
uint64_t tActivate = builder.addImmediateTransition(defaultPriority, 0.0, dftSpare->name() + "_activate_" + std::to_string(i) + "_" + std::to_string(k));
builder.setTransitionLayoutInfo(tActivate, storm::gspn::LayoutInfo(xcenter - 18.0 + (i + l) * 3, ycenter - 12.0));
builder.addInhibitionArc(activePlaces.at(k), tActivate);
builder.addInputArc(claimedPlace, tActivate);
builder.addInputArc(activePlace, tActivate);
@ -452,26 +455,26 @@ namespace storm {
builder.addOutputArc(tNextConsiders.back(), unavailablePlace);
builder.addOutputArc(tNextClaims.back(), unavailablePlace);
}
}
}
template <typename ValueType>
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translatePDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency) {
double xcenter = mDft.getElementLayoutInfo(dftDependency->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftDependency->id()).y;
if (!smart) {
addFailedPlace(dftDependency, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0));
addUnavailablePlace(dftDependency, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0));
addFailedPlace(dftDependency, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
addUnavailablePlace(dftDependency, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0));
}
uint64_t forwardPlace = 0;
if (dftDependency->probability() < 1.0) {
// PDEP
forwardPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_forward");
builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter+1.0, ycenter+2.0));
builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter + 1.0, ycenter + 2.0));
uint64_t coinPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_coin");
builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter-5.0, ycenter+2.0));
builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter - 5.0, ycenter + 2.0));
uint64_t tStartFlip = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_start_flip");
builder.addInputArc(coinPlace, tStartFlip);
@ -479,7 +482,7 @@ namespace storm {
builder.addOutputArc(tStartFlip, getFailedPlace(dftDependency->triggerEvent()));
uint64_t flipPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_flip");
builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter-2.0, ycenter+2.0));
builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter - 2.0, ycenter + 2.0));
builder.addOutputArc(tStartFlip, flipPlace);
uint64_t tWinFlip = builder.addImmediateTransition(defaultPriority, dftDependency->probability(), "_win_flip");
@ -493,7 +496,7 @@ namespace storm {
forwardPlace = getFailedPlace(dftDependency->triggerEvent());
}
for (auto const& child : dftDependency->dependentEvents()) {
for (auto const &child : dftDependency->dependentEvents()) {
uint64_t tForwardFailure = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_propagate_" + child->name());
builder.addInputArc(forwardPlace, tForwardFailure);
builder.addOutputArc(tForwardFailure, forwardPlace);
@ -506,43 +509,45 @@ namespace storm {
builder.addOutputArc(tForwardFailure, unavailablePlaces.at(child->id()));
}
}
}
template <typename ValueType>
}
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateSeq(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");
double xcenter = mDft.getElementLayoutInfo(dftSeq->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftSeq->id()).y;
if (!smart) {
addFailedPlace(dftSeq, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0));
addUnavailablePlace(dftSeq, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0));
addFailedPlace(dftSeq, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
addUnavailablePlace(dftSeq, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0));
}
uint64_t tEnable = 0;
uint64_t nextPlace = 0;
for (size_t i = 0; i < dftSeq->nrChildren(); ++i) {
auto const& child = dftSeq->children().at(i);
auto const &child = dftSeq->children().at(i);
nextPlace = builder.addPlace(defaultCapacity, i==0 ? 1 : 0, dftSeq->name() + "_next_" + child->name());
builder.setPlaceLayoutInfo(nextPlace, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter-3.0));
nextPlace = builder.addPlace(defaultCapacity, i == 0 ? 1 : 0, dftSeq->name() + "_next_" + child->name());
builder.setPlaceLayoutInfo(nextPlace, storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter - 3.0));
if (i>0) {
if (i > 0) {
builder.addOutputArc(tEnable, nextPlace);
}
tEnable = builder.addImmediateTransition(defaultPriority, 0.0, dftSeq->name() + "_unblock_" +child->name());
builder.setTransitionLayoutInfo(tEnable, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0));
tEnable = builder.addImmediateTransition(defaultPriority, 0.0, dftSeq->name() + "_unblock_" + child->name());
builder.setTransitionLayoutInfo(tEnable, storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter + 3.0));
builder.addInputArc(nextPlace, tEnable);
builder.addInputArc(disabledPlaces.at(child->id()), tEnable);
if (i>0) {
builder.addInputArc(getFailedPlace(dftSeq->children().at(i-1)), tEnable);
if (i > 0) {
builder.addInputArc(getFailedPlace(dftSeq->children().at(i - 1)), tEnable);
}
}
}
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::addFailedPlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialFailed) {
uint64_t
DftToGspnTransformator<ValueType>::addFailedPlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const &layoutInfo,
bool initialFailed) {
uint64_t failedPlace = builder.addPlace(defaultCapacity, initialFailed ? 1 : 0, dftElement->name() + STR_FAILED);
assert(failedPlaces.size() == dftElement->id());
failedPlaces.push_back(failedPlace);
@ -552,42 +557,44 @@ namespace storm {
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::addUnavailablePlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable) {
uint64_t DftToGspnTransformator<ValueType>::addUnavailablePlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement,
storm::gspn::LayoutInfo const &layoutInfo, bool initialAvailable) {
uint64_t unavailablePlace = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavail");
unavailablePlaces.emplace(dftElement->id(), unavailablePlace);
builder.setPlaceLayoutInfo(unavailablePlace, layoutInfo);
return unavailablePlace;
}
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::addDisabledPlace(std::shared_ptr<const storm::storage::DFTBE<ValueType> > dftBe, storm::gspn::LayoutInfo const& layoutInfo) {
uint64_t
DftToGspnTransformator<ValueType>::addDisabledPlace(std::shared_ptr<const storm::storage::DFTBE<ValueType> > dftBe, storm::gspn::LayoutInfo const &layoutInfo) {
uint64_t disabledPlace = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(), dftBe->name() + "_dabled");
disabledPlaces.emplace(dftBe->id(), disabledPlace);
builder.setPlaceLayoutInfo(disabledPlace, layoutInfo);
return disabledPlace;
}
template <typename ValueType>
template<typename ValueType>
bool DftToGspnTransformator<ValueType>::isActiveInitially(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
// If element is in the top module, return true.
// If element is in the top module, return true.
return !mDft.hasRepresentant(dftElement->id());
}
template <typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement)
{
}
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
// Temporariliy use one priority for all
return defaultPriority;
//return mDft.maxRank() - dftElement->rank() + 2;
}
}
// Explicitly instantiate the class.
template class DftToGspnTransformator<double>;
template
class DftToGspnTransformator<double>;
#ifdef STORM_HAVE_CARL
#ifdef STORM_HAVE_CARL
// template class DftToGspnTransformator<storm::RationalFunction>;
#endif
#endif
} // namespace dft
} // namespace transformations

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

@ -28,8 +28,9 @@ namespace storm {
* @param dontCareElements Set of DFT elements which should have Don't Care propagation.
* @param smart Flag indicating if smart semantics should be used.
* Smart semantics will only generate necessary parts of the GSPNs.
* @param mergeDCFailed Flag indicating if Don't Care places and Failed places should be merged.
*/
void transform(std::set<uint64_t> const& dontCareElements, bool smart = true);
void transform(std::set<uint64_t> const& dontCareElements, bool smart = true, bool mergeDCFailed = true);
/*!
* Extract Gspn by building
@ -194,6 +195,7 @@ namespace storm {
// Options
bool smart;
bool mergedDCFailed;
std::set<uint64_t> dontCareElements;
// Interface places for DFT elements

Write Preview
Loading…
Cancel
Save