diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 91632739e..e05b13210 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -1,5 +1,7 @@ #include "storm-dft/api/storm-dft.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" + namespace storm { namespace api { @@ -27,13 +29,25 @@ namespace storm { template<> void transformToGSPN(storm::storage::DFT const& dft) { + bool smart = true; + + // Set Don't Care elements + std::set dontCareElements; + storm::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule(); + if (!ftSettings.isDisableDC()) { + // Insert all elements as Don't Care elements + for (std::size_t i = 0; i < dft.nrElements(); i++) { + dontCareElements.insert(dft.getElement(i)->id()); + } + } + // Transform to GSPN storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); - bool smart = true; - gspnTransformator.transform(smart); + gspnTransformator.transform(dontCareElements, smart); storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); + // Export storm::api::handleGSPNExportSettings(*gspn); std::shared_ptr const& exprManager = gspn->getExpressionManager(); diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 7a2b0f360..a9b761c52 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -16,7 +16,8 @@ namespace storm { } template - void DftToGspnTransformator::transform(bool smart) { + void DftToGspnTransformator::transform(std::set const& dontCareElements, bool smart) { + this->dontCareElements = dontCareElements; this->smart = smart; builder.setGspnName("DftToGspnTransformation"); diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h index 3d49505c9..22ba384c7 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.h +++ b/src/storm-dft/transformations/DftToGspnTransformator.h @@ -24,8 +24,12 @@ namespace storm { /*! * Transform the DFT to a GSPN. + * + * @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. */ - void transform(bool smart = true); + void transform(std::set const& dontCareElements, bool smart = true); /*! * Extract Gspn by building @@ -188,13 +192,16 @@ namespace storm { storm::storage::DFT const& mDft; storm::gspn::GspnBuilder builder; + // Options + bool smart; + std::set dontCareElements; + // Interface places for DFT elements std::vector failedPlaces; std::map unavailablePlaces; std::map activePlaces; std::map disabledPlaces; - bool smart; - + 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.