diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 1905a26b6..d3eb05851 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -107,7 +107,8 @@ void processOptions() { std::shared_ptr> dft = loadDFT(); // Transform to GSPN storm::transformations::dft::DftToGspnTransformator gspnTransformator(*dft); - gspnTransformator.transform(); + bool smart = false; + gspnTransformator.transform(smart); storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 975d01f4a..1cb6673c7 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -16,14 +16,15 @@ namespace storm { } template - void DftToGspnTransformator::transform() { - + void DftToGspnTransformator::transform(bool smart) { + this->smart = smart; builder.setGspnName("DftToGspnTransformation"); // Loop through every DFT element and draw them as a GSPN. drawGSPNElements(); // Draw restrictions into the GSPN (i.e. SEQ or MUTEX). + // TODO //drawGSPNRestrictions(); } @@ -35,8 +36,7 @@ namespace storm { template void DftToGspnTransformator::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); @@ -81,7 +81,7 @@ namespace storm { drawPDEP(std::static_pointer_cast const>(dftElement)); break; default: - STORM_LOG_ASSERT(false, "DFT type unknown."); + STORM_LOG_ASSERT(false, "DFT type " << dftElement->type() << " unknown."); break; } } @@ -548,7 +548,7 @@ namespace storm { template uint64_t DftToGspnTransformator::addUnavailableNode(std::shared_ptr const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable) { - uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavailable"); + uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavail"); assert(unavailableNode != 0); unavailableNodes.emplace(dftElement->id(), unavailableNode); builder.setPlaceLayoutInfo(unavailableNode, layoutInfo); @@ -561,11 +561,9 @@ namespace storm { disabledNodes.emplace(dftBe->id(), disabledNode); return disabledNode; } -// template - bool DftToGspnTransformator::isBEActive(std::shared_ptr const> dftElement) - { + bool DftToGspnTransformator::isBEActive(std::shared_ptr const> dftElement) { // If element is the top element, return true. if (dftElement->id() == mDft.getTopLevelIndex()) { return true; @@ -607,6 +605,7 @@ namespace storm { template void DftToGspnTransformator::drawGSPNRestrictions() { + // TODO } template diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h index 4ec911b23..f2df6fcdd 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.h +++ b/src/storm-dft/transformations/DftToGspnTransformator.h @@ -25,7 +25,7 @@ namespace storm { /*! * Transform the DFT to a GSPN. */ - void transform(); + void transform(bool smart = true); /*! * Extract Gspn by building @@ -41,6 +41,7 @@ namespace storm { * Draw all elements of the GSPN. */ void drawGSPNElements(); + /* * Draw restrictions between the elements of the GSPN (i.e. SEQ or MUTEX). */ @@ -118,24 +119,24 @@ namespace storm { void drawSeq(std::shared_ptr 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). - * - * @param dFTElement DFT element. - */ - bool isBEActive(std::shared_ptr const> dFTElement); + + /* + * 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 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 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 const> dFTElement); - uint64_t addUnavailableNode(std::shared_ptr const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable = true); uint64_t addDisabledPlace(std::shared_ptr const> dftBe); @@ -146,16 +147,14 @@ namespace storm { std::map unavailableNodes; std::map activeNodes; std::map disabledNodes; - bool smart = true; + 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. 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. - - + static constexpr const char* STR_ACTIVATED = "_active"; // Name standard for place which indicates the activity. }; } }