From 349b0404ba8c6e8ace97dbcee2317be4d3c52f8c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 14 Dec 2016 22:32:23 +0100 Subject: [PATCH 1/8] restrictions are now topo-sorted correctly --- src/storm-dft/storage/dft/DFTBuilder.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index 10c84f5f6..69b100783 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -175,7 +175,13 @@ namespace storm { } else if(visited[n] == topoSortColour::WHITE) { if(n->isGate()) { visited[n] = topoSortColour::GREY; - for(DFTElementPointer const& c : std::static_pointer_cast>(n)->children()) { + for (DFTElementPointer const& c : std::static_pointer_cast>(n)->children()) { + topoVisit(c, visited, L); + } + } + if(n->isRestriction()) { + visited[n] = topoSortColour::GREY; + for (DFTElementPointer const& c : std::static_pointer_cast>(n)->children()) { topoVisit(c, visited, L); } } From 6e5a316f1d70be83d983aef90ec7045edce11fa1 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 14 Dec 2016 22:37:37 +0100 Subject: [PATCH 2/8] fix in dft::maxrank --- src/storm-dft/storage/dft/DFT.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 8f19119a2..3e06299f1 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -284,7 +284,13 @@ namespace storm { template uint64_t DFT::maxRank() const { - return mElements.back()->rank(); + uint64_t max = 0; + for (auto const& e : mElements) { + if(e->rank() > max) { + max = e->rank(); + } + } + return max; } template From 99428f9a7b87268da07c48bdd750c1a324edfad1 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 14 Dec 2016 22:38:23 +0100 Subject: [PATCH 3/8] priorities updated such that 0 is not used as this is often reserved, e.g. in greatspn --- src/storm-dft/transformations/DftToGspnTransformator.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index f3a113215..14b037025 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -7,7 +7,7 @@ namespace storm { namespace dft { // Prevent some magic constants - static constexpr const uint64_t defaultPriority = 0; + static constexpr const uint64_t defaultPriority = 1; static constexpr const uint64_t defaultCapacity = 1; template @@ -436,7 +436,7 @@ namespace storm { template uint64_t DftToGspnTransformator::getFailPriority(std::shared_ptr const> dftElement) { - return mDft.maxRank() - dftElement->rank(); + return mDft.maxRank() - dftElement->rank() + 2; } From 80d578d1303cca9d63597f71348c76b55971e6dc Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 14 Dec 2016 23:04:41 +0100 Subject: [PATCH 4/8] POR[inclusive] support seems to be working now --- .../DftToGspnTransformator.cpp | 60 +++++++++++-------- 1 file changed, 35 insertions(+), 25 deletions(-) diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 14b037025..ccfa5bdf4 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -232,27 +232,32 @@ namespace storm { if (isRepresentative) { unavailableNode = addUnavailableNode(dftPand); } - - 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); - if (isRepresentative) { + + if(dftPand->isInclusive()) { + + 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); - builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); - } - 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.addOutputArc(tfs, failedNodes[dftPand->children().at(j)->id()]); - builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs); - builder.addOutputArc(tfs, nodeFS); - builder.addInhibitionArc(nodeFS, tfs); - + if (isRepresentative) { + builder.addOutputArc(tNodeFailed, nodeFailed); + } + for(auto const& child : dftPand->children()) { + builder.addInputArc(failedNodes[child->id()], tNodeFailed); + builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); + } + 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.addOutputArc(tfs, failedNodes[dftPand->children().at(j)->id()]); + builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs); + builder.addOutputArc(tfs, nodeFS); + builder.addInhibitionArc(nodeFS, tfs); + + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NOt yet implemented"); } } // @@ -318,6 +323,7 @@ namespace storm { template void DftToGspnTransformator::drawPOR(std::shared_ptr const> dftPor, bool isRepresentative) { uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILED); + failedNodes.push_back(nodeFailed); uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE); @@ -329,11 +335,15 @@ namespace storm { builder.addInhibitionArc(nodeFailed, tfail); uint64_t j = 0; for (auto const& child : dftPor->children()) { - uint64_t tfailsf = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(j)); - builder.addInputArc(failedNodes.at(child->id()), tfailsf); - builder.addOutputArc(tfailsf, failedNodes.at(child->id())); - // TODO -// builder.addInhibitionArc(<#const uint_fast64_t &from#>, <#const uint_fast64_t &to#>) + if(j > 0) { + uint64_t tfailsf = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(j)); + builder.addInputArc(failedNodes.at(child->id()), tfailsf); + builder.addOutputArc(tfailsf, failedNodes.at(child->id())); + builder.addOutputArc(tfailsf, nodeFS); + builder.addInhibitionArc(nodeFS, tfailsf); + builder.addInhibitionArc(failedNodes.at(dftPor->children().front()->id()), tfailsf); + } + ++j; } } From fac77c0a3eac62f4a6873733de2b1468af3964c9 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 14 Dec 2016 23:14:54 +0100 Subject: [PATCH 5/8] fixed seq, now correct... --- .../transformations/DftToGspnTransformator.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index ccfa5bdf4..4a4432f78 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -376,18 +376,21 @@ namespace storm { template void DftToGspnTransformator::drawSeq(std::shared_ptr 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 j = 0; 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) { + nextPlace = builder.addPlace(defaultCapacity, j==0 ? 1 : 0, dftSeq->name() + "_next_" + child->name()); + if (j>0) { 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; + if (j>0) { + builder.addInputArc(failedNodes.at(dftSeq->children().at(j-1)->id()), tEnable); + } + ++j; } } From 9c5444e059623d2654ebc0749578a489c2c7993d Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 14 Dec 2016 23:44:19 +0100 Subject: [PATCH 6/8] better inclusive/exclusive support, including parsing --- src/storm-dft/parser/DFTGalileoParser.cpp | 8 ++++++++ src/storm-dft/storage/dft/DFTBuilder.h | 9 +++++++++ src/storm-dft/storage/dft/elements/DFTPand.h | 6 +++++- src/storm-dft/storage/dft/elements/DFTPor.h | 9 +++++++-- 4 files changed, 29 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index ec0b446d9..f872f4526 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -110,8 +110,16 @@ namespace storm { success = builder.addVotElement(name, threshold, childNames); } else if (tokens[1] == "pand") { success = builder.addPandElement(name, childNames); + } else if (tokens[1] == "pand-inc") { + success = builder.addPandElement(name, childNames, true); + } else if (tokens[1] == "pand-ex") { + success = builder.addPandElement(name, childNames, false); } else if (tokens[1] == "por") { success = builder.addPorElement(name, childNames); + } else if (tokens[1] == "por-ex") { + success = builder.addPorElement(name, childNames, false); + } else if (tokens[1] == "por-inc") { + success = builder.addPorElement(name, childNames, true); } else if (tokens[1] == "wsp" || tokens[1] == "csp") { success = builder.addSpareElement(name, childNames); } else if (tokens[1] == "seq") { diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h index 55c1cb588..fbec0943e 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/src/storm-dft/storage/dft/DFTBuilder.h @@ -53,6 +53,7 @@ namespace storm { bool addPandElement(std::string const& name, std::vector const& children, bool inclusive) { bool tmpDefault = pandDefaultInclusive; + pandDefaultInclusive = inclusive; bool result = addStandardGate(name, children, DFTElementType::PAND); pandDefaultInclusive = tmpDefault; return result; @@ -62,6 +63,14 @@ namespace storm { return addStandardGate(name, children, DFTElementType::POR); } + bool addPorElement(std::string const& name, std::vector const& children, bool inclusive) { + bool tmpDefault = porDefaultInclusive; + porDefaultInclusive = inclusive; + bool result = addStandardGate(name, children, DFTElementType::POR); + pandDefaultInclusive = tmpDefault; + return result; + } + bool addSpareElement(std::string const& name, std::vector const& children) { return addStandardGate(name, children, DFTElementType::SPARE); } diff --git a/src/storm-dft/storage/dft/elements/DFTPand.h b/src/storm-dft/storage/dft/elements/DFTPand.h index d89e357b1..8e5e2716a 100644 --- a/src/storm-dft/storage/dft/elements/DFTPand.h +++ b/src/storm-dft/storage/dft/elements/DFTPand.h @@ -50,7 +50,11 @@ namespace storm { } std::string typestring() const override { - return "PAND" + inclusive ? "" : "-ex"; + if (inclusive) { + return "PAND-inc"; + } else { + return "PAND-ex"; + } } protected: bool inclusive; diff --git a/src/storm-dft/storage/dft/elements/DFTPor.h b/src/storm-dft/storage/dft/elements/DFTPor.h index 3adaf16fc..565b5dacd 100644 --- a/src/storm-dft/storage/dft/elements/DFTPor.h +++ b/src/storm-dft/storage/dft/elements/DFTPor.h @@ -42,10 +42,15 @@ namespace storm { } std::string typestring() const override { - return "POR" + inclusive ? "" : "-ex"; + if (inclusive) { + return "POR-inc"; + } else { + return "POR-ex"; + } + } - bool isInclusive() { + bool isInclusive() const { return inclusive; } protected: From c718b1caef03fe8ba7684d8a367c1fd6ec8b74a7 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 14 Dec 2016 23:44:55 +0100 Subject: [PATCH 7/8] dft-por exclusive added; also ensured that PORs work under SPAREs --- .../DftToGspnTransformator.cpp | 50 +++++++++++++------ 1 file changed, 36 insertions(+), 14 deletions(-) diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 4a4432f78..6d22c8184 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -324,28 +324,50 @@ namespace storm { void DftToGspnTransformator::drawPOR(std::shared_ptr const> dftPor, bool isRepresentative) { uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILED); failedNodes.push_back(nodeFailed); - uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE); + uint64_t unavailableNode = 0; + if (!smart || isRepresentative) { + unavailableNode = addUnavailableNode(dftPor); + } uint64_t tfail = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILING); - builder.addInhibitionArc(nodeFS, tfail); - builder.addInputArc(failedNodes.at(dftPor->children().front()->id()), tfail); - builder.addOutputArc(tfail, failedNodes.at(dftPor->children().front()->id())); builder.addOutputArc(tfail, nodeFailed); builder.addInhibitionArc(nodeFailed, tfail); - uint64_t j = 0; - for (auto const& child : dftPor->children()) { - if(j > 0) { - uint64_t tfailsf = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(j)); - builder.addInputArc(failedNodes.at(child->id()), tfailsf); - builder.addOutputArc(tfailsf, failedNodes.at(child->id())); - builder.addOutputArc(tfailsf, nodeFS); - builder.addInhibitionArc(nodeFS, tfailsf); - builder.addInhibitionArc(failedNodes.at(dftPor->children().front()->id()), tfailsf); + + builder.addInputArc(failedNodes.at(dftPor->children().front()->id()), tfail); + builder.addOutputArc(tfail, failedNodes.at(dftPor->children().front()->id())); + + if(!smart || isRepresentative) { + builder.addOutputArc(tfail, unavailableNode); + } + + if(dftPor->isInclusive()) { + uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE); + builder.addInhibitionArc(nodeFS, tfail); + uint64_t j = 0; + for (auto const& child : dftPor->children()) { + if(j > 0) { + uint64_t tfailsf = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(j)); + builder.addInputArc(failedNodes.at(child->id()), tfailsf); + builder.addOutputArc(tfailsf, failedNodes.at(child->id())); + builder.addOutputArc(tfailsf, nodeFS); + builder.addInhibitionArc(nodeFS, tfailsf); + builder.addInhibitionArc(failedNodes.at(dftPor->children().front()->id()), tfailsf); + } + + ++j; + } + } else { + uint64_t j = 0; + for (auto const& child : dftPor->children()) { + if(j > 0) { + builder.addInhibitionArc(failedNodes.at(child->id()), tfail); + } + ++j; } - ++j; } + } // From 44082fbc37ba9d0a514c8c8fa485a89bc5178f9a Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 15 Dec 2016 00:08:00 +0100 Subject: [PATCH 8/8] pand-ex support --- .../DftToGspnTransformator.cpp | 40 +++++++++++++++---- 1 file changed, 32 insertions(+), 8 deletions(-) diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 6d22c8184..9028db24c 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -229,20 +229,22 @@ namespace storm { assert(failedNodes.size() == dftPand->id()); failedNodes.push_back(nodeFailed); uint64_t unavailableNode = 0; - if (isRepresentative) { + if (!smart || isRepresentative) { unavailableNode = addUnavailableNode(dftPand); } + uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING); + builder.addInhibitionArc(nodeFailed, tNodeFailed); + builder.addOutputArc(tNodeFailed, nodeFailed); + if (!smart || isRepresentative) { + builder.addOutputArc(tNodeFailed, nodeFailed); + } + + if(dftPand->isInclusive()) { 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); - if (isRepresentative) { - builder.addOutputArc(tNodeFailed, nodeFailed); - } for(auto const& child : dftPand->children()) { builder.addInputArc(failedNodes[child->id()], tNodeFailed); builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); @@ -257,7 +259,29 @@ namespace storm { } } else { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NOt yet implemented"); + uint64_t fi = 0; + uint64_t tn = 0; + for(uint64_t j = 0; j < dftPand->nrChildren(); ++j) { + auto const& child = dftPand->children()[j]; + if (j > 0) { + builder.addInhibitionArc(failedNodes.at(child->id()), tn); + } + if (j != dftPand->nrChildren() - 1) { + tn = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(j)); + } else { + tn = tNodeFailed; + } + builder.addInputArc(failedNodes.at(child->id()), tn); + builder.addOutputArc(tn, failedNodes.at(child->id())); + if (j > 0) { + builder.addInputArc(fi, tn); + } + if (j != dftPand->nrChildren() - 1) { + fi = builder.addPlace(defaultCapacity, 0, dftPand->name() + "_F_" + std::to_string(j)); + builder.addOutputArc(tn, fi); + } + + } } } //