From e390e1c39d01c5ad6fc98d6a54dd0a87e1b0f680 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 14 Mar 2016 20:47:14 +0100 Subject: [PATCH] several updates for better modularisation and support for VOT-modularisation Former-commit-id: 97d5d03a868debcea7ae474b6ae070bfa9247ea4 --- src/modelchecker/DFTAnalyser.h | 74 +++++++++++++++++++++++++--------- src/storage/dft/DFT.cpp | 4 +- src/storage/dft/DFT.h | 4 ++ src/utility/bitoperations.h | 17 ++++++++ 4 files changed, 77 insertions(+), 22 deletions(-) create mode 100644 src/utility/bitoperations.h diff --git a/src/modelchecker/DFTAnalyser.h b/src/modelchecker/DFTAnalyser.h index 93bc7c7b1..de128af64 100644 --- a/src/modelchecker/DFTAnalyser.h +++ b/src/modelchecker/DFTAnalyser.h @@ -6,6 +6,7 @@ #include "modelchecker/results/CheckResult.h" #include "utility/storm.h" #include "storage/dft/DFTIsomorphism.h" +#include "utility/bitoperations.h" #include @@ -42,28 +43,42 @@ private: bool invResults = false; std::vector> dfts = {dft}; std::vector res; + size_t nrK = 0; // K out of M + size_t nrM = 0; // K out of M if(allowModularisation) { - std::cout << dft.topLevelType() << std::endl; if(dft.topLevelType() == storm::storage::DFTElementType::AND) { - std::cout << "top modularisation called AND" << std::endl; + STORM_LOG_TRACE("top modularisation called AND"); dfts = dft.topModularisation(); - if(dfts.size() > 1) { - for(auto const ft : dfts) { - res.push_back(checkHelper(ft, formula, symred, allowModularisation)); - } - } + STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); + nrK = dfts.size(); + nrM = dfts.size(); } if(dft.topLevelType() == storm::storage::DFTElementType::OR) { - std::cout << "top modularisation called OR" << std::endl; + STORM_LOG_TRACE("top modularisation called OR"); dfts = dft.topModularisation(); - if(dfts.size() > 1) { - for(auto const ft : dfts) { - res.push_back(checkHelper(ft, formula, symred, allowModularisation)); - } - } + STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); + nrK = 0; + nrM = dfts.size(); invResults = true; } + if(dft.topLevelType() == storm::storage::DFTElementType::VOT) { + STORM_LOG_TRACE("top modularisation called VOT"); + dfts = dft.topModularisation(); + STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); + nrK = std::static_pointer_cast const>(dft.getTopLevelGate())->threshold(); + nrM = dfts.size(); + if(nrK <= nrM/2) { + nrK -= 1; + invResults = true; + } + } + if(dfts.size() > 1) { + STORM_LOG_TRACE("Recursive CHECK Call"); + for(auto const ft : dfts) { + res.push_back(checkHelper(ft, formula, symred, allowModularisation)); + } + } } if(res.empty()) { // Model based modularisation. @@ -82,14 +97,33 @@ private: res.push_back(result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second); } } + if(nrM <= 1) { + // No modularisation done. + assert(res.size()==1); + return res[0]; + } - ValueType result = storm::utility::one(); - for(auto const& r : res) { - if(invResults) { - result *= storm::utility::one() - r; - } else { - result *= r; - } + STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" << (invResults?"On":"Off")); + ValueType result = storm::utility::zero(); + int limK = invResults ? -1 : nrM+1; + int chK = invResults ? -1 : 1; + for(int cK = nrK; cK != limK; cK += chK ) { + assert(cK >= 0); + size_t permutation = smallestIntWithNBitsSet(static_cast(cK)); + do { + STORM_LOG_TRACE("Permutation="<(); + for(size_t i = 0; i < res.size(); ++i) { + if(permutation & (1 << i)) { + permResult *= res[i]; + } else { + permResult *= storm::utility::one() - res[i]; + } + } + STORM_LOG_TRACE("Result for permutation:"<() - result; diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 482e8203c..4111a2113 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -261,8 +261,8 @@ namespace storm { isubdft = getGate(child->id())->independentSubDft(false); } else { assert(isBasicElement(child->id())); - if(!getBasicElement(child->id())->hasIngoingDependencies()) { - isubdft = {child->id()}; + if(getBasicElement(child->id())->hasIngoingDependencies()) { + return {*this}; } } diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 0f4832fb5..d82c45dfa 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -167,6 +167,10 @@ namespace storm { return std::static_pointer_cast const>(mElements[index]); } + std::shared_ptr const> getTopLevelGate() const { + return getGate(mTopLevelIndex); + } + std::shared_ptr const> getGate(size_t index) const { assert(isGate(index)); return std::static_pointer_cast const>(mElements[index]); diff --git a/src/utility/bitoperations.h b/src/utility/bitoperations.h new file mode 100644 index 000000000..55456dd61 --- /dev/null +++ b/src/utility/bitoperations.h @@ -0,0 +1,17 @@ +#pragma once + +inline size_t smallestIntWithNBitsSet(size_t n) { + assert(sizeof(size_t) == 8); + assert(n < 64); // TODO fix this for 32 bit architectures! + if(n==0) return static_cast(0); + return (1 << n) - 1; +} + +inline size_t nextBitPermutation(size_t v) { + if(v==0) return static_cast(0); + // From https://graphics.stanford.edu/~seander/bithacks.html#NextBitPermutation + unsigned int t = (v | (v - 1)) + 1; + return t | ((((t & -t) / (v & -v)) >> 1) - 1); +} + + \ No newline at end of file