diff --git a/benchmark_dft.py b/benchmark_dft.py deleted file mode 100644 index 6f25e08ed..000000000 --- a/benchmark_dft.py +++ /dev/null @@ -1,136 +0,0 @@ -import os -import os.path -import sys -import subprocess -import re -import time -import argparse - -DIR=os.getcwd() -STORM_PATH=os.path.join(DIR, "build/src/storm-dft") -EXAMPLE_DIR=os.path.join(DIR, "examples/dft/") - -benchmarks = [ - ("and", False, [3, 1]), - ("and_param", True, ["(4*x^2+2*x+1)/((x) * (2*x+1))", "1"]), - ("cardiac", False, [8597.360004, 1]), - ("cas", False, [0.859736, 1]), - ("cm2", False, [0.256272, 1]), - #("cm4", False, [0.338225, 1]), # big - ("cps", False, ["inf", 0.333333]), - #("deathegg", False, [24.642857, 1]), # contains fdep to gate - #("fdep", False, [0.666667, 1]), # contains fdep to two elements - ("fdep2", False, [2, 1]), - ("fdep3", False, [2.5, 1]), - #("ftpp_complex", False, [0, 1]), # Compute - #("ftpp_large", False, [0, 1]), # Compute - #("ftpp_standard", False, [0, 1]), # Compute - ("mdcs", False, [2.85414, 1]), - ("mdcs2", False, [2.85414, 1]), - ("mp", False, [1.66667, 1]), - ("or", False, [1, 1]), - ("pand", False, ["inf", 0.666667]), - ("pand_param", True, ["-1", "(x)/(y+x)"]), - ("pdep", False, [2.66667, 1]), - #("pdep2", False, [0, 1]), #Compute # contains pdep to two elements - ("pdep3", False, [2.79167, 1]), - ("spare", False, [3.53846, 1]), - ("spare2", False, [1.86957, 1]), - ("spare3", False, [1.27273, 1]), - ("spare4", False, [4.8459, 1]), - ("spare5", False, [2.66667, 1]), - ("spare6", False, [1.4, 1]), - ("spare7", False, [3.67333, 1]), - ("symmetry", False, [4.16667, 1]), - ("symmetry2", False, [3.06111, 1]), - ("tripple_and1", False, [4.16667, 1]), - ("tripple_and2", False, [3.66667, 1]), - ("tripple_and2_c", False, [3.6667, 1]), - ("tripple_and_c", False, [4.16667, 1]), - ("tripple_or", False, [0.5, 1]), - ("tripple_or2", False, [0.666667, 1]), - ("tripple_or2_c", False, [0.66667, 1]), - ("tripple_or_c", False, [0.5, 1]), - ("tripple_pand", False, ["inf", 0.0416667]), - ("tripple_pand2", False, ["inf", 0.166667]), - ("tripple_pand2_c", False, ["inf", 0.166667]), - ("tripple_pand_c", False, ["inf", 0.0416667]), - ("voting", False, [1.66667, 1]), - ("voting2", False, [0.588235, 1]) -] - -def run_storm_dft(filename, prop, parametric, quiet): - # Run storm-dft on filename and return result - dft_file = os.path.join(EXAMPLE_DIR, filename + ".dft") - args = [STORM_PATH, - dft_file, - prop] - if parametric: - args.append('--parametric') - - output = run_tool(args, quiet) - # Get result - match = re.search(r'Result: \[(.*)\]', output) - if not match: - return None - - result = match.group(1) - return result - -def run_tool(args, quiet=False): - """ - Executes a process, - :returns: the `stdout` - """ - pipe = subprocess.Popen(args, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - result = ""; - for line in iter(pipe.stdout.readline, ""): - if not line and pipe.poll() is not None: - break - output = line.decode(encoding='UTF-8').rstrip() - if output != "": - if not quiet: - print("\t * " + output) - result = output - return result - -def isclose(a, b, rel_tol=1e-09, abs_tol=0.0): - if a == b: - return True - return abs(a-b) <= max(rel_tol * max(abs(a), abs(b)), abs_tol) - -if __name__ == "__main__": - parser = argparse.ArgumentParser(description='Benchmarking DFTs via Storm') - parser.add_argument('--debuglevel', type=int, default=0, help='the debug level (0=silent, 1=print benchmarks, 2=print output from storm') - args = parser.parse_args() - count = 0 - correct = 0 - properties = ['--expectedtime', '--probability'] - start = time.time() - for index, prop in enumerate(properties): - for (benchmark, parametric, result_original) in benchmarks: - expected_result = result_original[index] - # Run benchmark and check result - count += 1; - if args.debuglevel > 0: - print("Running '{}' with property '{}'".format(benchmark, prop)) - result = run_storm_dft(benchmark, prop, parametric, args.debuglevel<2) - if result is None: - print("Error occurred on example '{}' with property '{}'".format(benchmark, prop)) - continue - - if not parametric: - # Float - result = float(result) - if not isclose(result, float(expected_result), rel_tol=1e-05): - print("Wrong result on example '{}' with property '{}': result: {}, Expected: {}".format(benchmark, prop, result, expected_result)) - else: - correct += 1 - else: - # Parametric - if result != expected_result: - print("Wrong result on example '{}' with property '{}': result: {}, Expected: {}".format(benchmark, prop, result, expected_result)) - else: - correct += 1 - end = time.time() - print("Correct results for {} of {} DFT checks in {}s".format(correct, count, end-start)) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 48428d7cc..3aa121a0a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -37,13 +37,13 @@ file(GLOB STORM_SOLVER_STATEELIMINATION_FILES ${PROJECT_SOURCE_DIR}/src/solver/s file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp) file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) +file(GLOB STORM_STORAGE_DFT_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp) file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) -file(GLOB_RECURSE STORM_STORAGE_DFT_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp) # Additional include files like the storm-config.h diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 160535443..a7284cb9c 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -13,11 +13,52 @@ namespace storm { ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { // Intentionally left empty. } + + template + ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, std::pow(2, mDft.nrBasicElements())) { + // stateSize is bound for size of bitvector + // 2^nrBE is upper bound for state space + + // Find symmetries + // TODO activate + // Currently using hack to test + std::vector> symmetries; + std::vector vecB; + std::vector vecC; + std::vector vecD; + if (false) { + for (size_t i = 0; i < mDft.nrElements(); ++i) { + std::string name = mDft.getElement(i)->name(); + size_t id = mDft.getElement(i)->id(); + if (boost::starts_with(name, "B")) { + vecB.push_back(id); + } else if (boost::starts_with(name, "C")) { + vecC.push_back(id); + } else if (boost::starts_with(name, "D")) { + vecD.push_back(id); + } + } + symmetries.push_back(vecB); + symmetries.push_back(vecC); + symmetries.push_back(vecD); + std::cout << "Found the following symmetries:" << std::endl; + for (auto const& symmetry : symmetries) { + for (auto const& elem : symmetry) { + std::cout << elem << " -> "; + } + std::cout << std::endl; + } + } else { + vecB.push_back(mDft.getTopLevelIndex()); + } + mStateGenerationInfo = std::make_shared(mDft.buildStateGenerationInfo(vecB, symmetries)); + } + template std::shared_ptr> ExplicitDFTModelBuilder::buildModel() { // Initialize - DFTStatePointer state = std::make_shared>(mDft, newIndex++); + DFTStatePointer state = std::make_shared>(mDft, *mStateGenerationInfo, newIndex++); mStates.findOrAdd(state->status(), state); std::queue stateQueue; @@ -73,22 +114,22 @@ namespace storm { } std::shared_ptr> model; - // Turn the probabilities into rates by multiplying each row with the exit rate of the state. - // TODO Matthias: avoid transforming back and forth - storm::storage::SparseMatrix rateMatrix(modelComponents.transitionMatrix); - for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) { - assert(row < modelComponents.markovianStates.size()); - if (modelComponents.markovianStates.get(row)) { - for (auto& entry : rateMatrix.getRow(row)) { - entry.setValue(entry.getValue() * modelComponents.exitRates[row]); - } - } - } if (deterministic) { + // Turn the probabilities into rates by multiplying each row with the exit rate of the state. + // TODO Matthias: avoid transforming back and forth + storm::storage::SparseMatrix rateMatrix(modelComponents.transitionMatrix); + for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) { + assert(row < modelComponents.markovianStates.size()); + if (modelComponents.markovianStates.get(row)) { + for (auto& entry : rateMatrix.getRow(row)) { + entry.setValue(entry.getValue() * modelComponents.exitRates[row]); + } + } + } model = std::make_shared>(std::move(rateMatrix), std::move(modelComponents.stateLabeling)); } else { - model = std::make_shared>(std::move(rateMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates)); + model = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true); } model->printModelInformationToStream(std::cout); diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index 67dec3dc4..eacf2568c 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -44,15 +44,13 @@ namespace storm { boost::optional>> choiceLabeling; }; - storm::storage::DFT const &mDft; + storm::storage::DFT const& mDft; + std::shared_ptr mStateGenerationInfo; storm::storage::BitVectorHashMap mStates; size_t newIndex = 0; public: - ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft), mStates(((mDft.stateSize() / 64) + 1) * 64, std::pow(2, mDft.nrBasicElements())) { - // stateSize is bound for size of bitvector - // 2^nrBE is upper bound for state space - } + ExplicitDFTModelBuilder(storm::storage::DFT const& dft); std::shared_ptr> buildModel(); diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index c757af1a0..8276f519d 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -34,6 +34,19 @@ namespace storm { this->turnRatesToProbabilities(); } + template + MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, + storm::models::sparse::StateLabeling&& stateLabeling, + storm::storage::BitVector const& markovianStates, + std::vector const& exitRates, + bool probabilities, + std::unordered_map&& rewardModels, + boost::optional>&& optionalChoiceLabeling) + : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) { + assert(probabilities); + assert(this->getTransitionMatrix().isProbabilistic()); + } + template bool MarkovAutomaton::isClosed() const { return closed; diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index ed807ab84..e335f5050 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -49,6 +49,25 @@ namespace storm { std::unordered_map&& rewardModels = std::unordered_map(), boost::optional>&& optionalChoiceLabeling = boost::optional>()); + /*! + * Constructs a model by moving the given data. + * + * @param transitionMatrix The matrix representing the transitions in the model in terms of rates. + * @param stateLabeling The labeling of the states. + * @param markovianStates A bit vector indicating the Markovian states of the automaton. + * @param exitRates A vector storing the exit rates of the states. + * @param rewardModels A mapping of reward model names to reward models. + * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. + * @param probabilities Flag if transitions matrix contains probabilities or rates + */ + MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, + storm::models::sparse::StateLabeling&& stateLabeling, + storm::storage::BitVector const& markovianStates, + std::vector const& exitRates, + bool probabilities, + std::unordered_map&& rewardModels = std::unordered_map(), + boost::optional>&& optionalChoiceLabeling = boost::optional>()); + MarkovAutomaton(MarkovAutomaton const& other) = default; MarkovAutomaton& operator=(MarkovAutomaton const& other) = default; diff --git a/src/solver/AbstractEquationSolver.h b/src/solver/AbstractEquationSolver.h index 904e459bd..491570637 100644 --- a/src/solver/AbstractEquationSolver.h +++ b/src/solver/AbstractEquationSolver.h @@ -2,6 +2,7 @@ #define STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ #include "src/solver/TerminationCondition.h" +#include namespace storm { namespace solver { @@ -50,4 +51,4 @@ namespace storm { } } -#endif /* STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ */ \ No newline at end of file +#endif /* STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ */ diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index a52cf8984..a71b3aa2a 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -11,33 +11,27 @@ namespace storm { namespace storage { template - DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0) - { + DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()) { assert(elementIndicesCorrect()); - - size_t stateIndex = 0; - mUsageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1; - + size_t nrRepresentatives = 0; + for (auto& elem : mElements) { - mIdToFailureIndex.push_back(stateIndex); - stateIndex += 2; + if (isRepresentative(elem->id())) { + ++nrRepresentatives; + } if(elem->isBasicElement()) { ++mNrOfBEs; } else if (elem->isSpareGate()) { ++mNrOfSpares; + bool firstChild = true; for(auto const& spareReprs : std::static_pointer_cast>(elem)->children()) { - if(mActivationIndex.count(spareReprs->id()) == 0) { - mActivationIndex[spareReprs->id()] = stateIndex++; - } std::set module = {spareReprs->id()}; spareReprs->extendSpareModule(module); std::vector sparesAndBes; - bool secondSpare = false; - for(auto const& modelem : module) { - if (mElements[modelem]->isSpareGate()) { - STORM_LOG_THROW(!secondSpare, storm::exceptions::NotSupportedException, "Module for '" << spareReprs->name() << "' contains more than one spare."); - secondSpare = true; + for(size_t modelem : module) { + if (spareReprs->id() != modelem && (isRepresentative(modelem) || (!firstChild && mTopLevelIndex == modelem))) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Module for '" << spareReprs->name() << "' contains more than one representative."); } if(mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) { sparesAndBes.push_back(modelem); @@ -45,17 +39,14 @@ namespace storm { } } mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes)); - + firstChild = false; } - std::static_pointer_cast>(elem)->setUseIndex(stateIndex); - mUsageIndex.insert(std::make_pair(elem->id(), stateIndex)); - stateIndex += mUsageInfoBits; } else if (elem->isDependency()) { mDependencies.push_back(elem->id()); } } - + // For the top module, we assume, contrary to [Jun15], that we have all spare gates and basic elements which are not in another module. std::set topModuleSet; // Initialize with all ids. @@ -71,12 +62,81 @@ namespace storm { } } mTopModule = std::vector(topModuleSet.begin(), topModuleSet.end()); + + size_t usageInfoBits = mElements.size() > 1 ? storm::utility::math::uint64_log2(mElements.size()-1) + 1 : 1; + mStateVectorSize = nrElements() * 2 + mNrOfSpares * usageInfoBits + nrRepresentatives; + } - mStateSize = stateIndex; - mTopLevelIndex = tle->id(); + template + DFTStateGenerationInfo DFT::buildStateGenerationInfo(std::vector const& subTreeRoots, std::vector> const& symmetries) const { + // Use symmetry + // Collect all elements in the first subtree + // TODO make recursive to use for nested subtrees + + DFTStateGenerationInfo generationInfo(nrElements()); + // Perform DFS and insert all elements of subtree sequentially + size_t stateIndex = 0; + std::queue visitQueue; + std::set visited; + visitQueue.push(subTreeRoots[0]); + bool consideredDependencies = false; + while (true) { + while (!visitQueue.empty()) { + size_t id = visitQueue.front(); + visitQueue.pop(); + if (visited.count(id) == 1) { + // Already visited + continue; + } + visited.insert(id); + DFTElementPointer element = mElements[id]; + + // Insert children + if (element->isGate()) { + for (auto const& child : std::static_pointer_cast>(element)->children()) { + visitQueue.push(child->id()); + } + } + + // Reserve bits for element + generationInfo.addStateIndex(id, stateIndex); + stateIndex += 2; + + if (isRepresentative(id)) { + generationInfo.addSpareActivationIndex(id, stateIndex); + ++stateIndex; + } + + if (element->isSpareGate()) { + generationInfo.addSpareUsageIndex(id, stateIndex); + stateIndex += generationInfo.usageInfoBits(); + } + + } + + if (consideredDependencies) { + break; + } + + // Consider dependencies + for (size_t idDependency : getDependencies()) { + std::shared_ptr const> dependency = getDependency(idDependency); + visitQueue.push(dependency->id()); + visitQueue.push(dependency->triggerEvent()->id()); + visitQueue.push(dependency->dependentEvent()->id()); + } + consideredDependencies = true; + } + assert(stateIndex = mStateVectorSize); + + STORM_LOG_TRACE(generationInfo); + + return generationInfo; } + + template std::string DFT::getElementsString() const { std::stringstream stream; diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 61f286619..94d2d8186 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -33,6 +33,69 @@ namespace storm { // Forward declarations template class DFTColouring; + + class DFTStateGenerationInfo { + private: + const size_t mUsageInfoBits; + std::map mSpareUsageIndex; // id spare -> index first bit in state + std::map mSpareActivationIndex; // id spare representative -> index in state + std::vector mIdToStateIndex; // id -> index first bit in state + + public: + + DFTStateGenerationInfo(size_t nrElements) : mUsageInfoBits(nrElements > 1 ? storm::utility::math::uint64_log2(nrElements-1) + 1 : 1), mIdToStateIndex(nrElements) { + } + + size_t usageInfoBits() const { + return mUsageInfoBits; + } + + void addStateIndex(size_t id, size_t index) { + assert(id < mIdToStateIndex.size()); + mIdToStateIndex[id] = index; + } + + void addSpareActivationIndex(size_t id, size_t index) { + mSpareActivationIndex[id] = index; + } + + void addSpareUsageIndex(size_t id, size_t index) { + mSpareUsageIndex[id] = index; + } + + size_t getStateIndex(size_t id) const { + assert(id < mIdToStateIndex.size()); + return mIdToStateIndex[id]; + } + + size_t getSpareUsageIndex(size_t id) const { + assert(mSpareUsageIndex.count(id) > 0); + return mSpareUsageIndex.at(id); + } + + size_t getSpareActivationIndex(size_t id) const { + assert(mSpareActivationIndex.count(id) > 0); + return mSpareActivationIndex.at(id); + } + + friend std::ostream& operator<<(std::ostream& os, DFTStateGenerationInfo const& info) { + os << "Id to state index:" << std::endl; + for (size_t id = 0; id < info.mIdToStateIndex.size(); ++id) { + os << id << " -> " << info.getStateIndex(id) << std::endl; + } + os << "Spare usage index with usage InfoBits of size " << info.mUsageInfoBits << ":" << std::endl; + for (auto pair : info.mSpareUsageIndex) { + os << pair.first << " -> " << pair.second << std::endl; + } + os << "Spare activation index:" << std::endl; + for (auto pair : info.mSpareActivationIndex) { + os << pair.first << " -> " << pair.second << std::endl; + } + return os; + } + + }; + /** * Represents a Dynamic Fault Tree @@ -52,21 +115,20 @@ namespace storm { size_t mNrOfBEs; size_t mNrOfSpares; size_t mTopLevelIndex; - size_t mUsageInfoBits; - size_t mStateSize; - std::map mActivationIndex; + size_t mStateVectorSize; std::map> mSpareModules; std::vector mDependencies; std::vector mTopModule; - std::vector mIdToFailureIndex; - std::map mUsageIndex; - std::map mRepresentants; + std::map mRepresentants; // id element -> id representative + std::vector> mSymmetries; public: DFT(DFTElementVector const& elements, DFTElementPointer const& tle); + + DFTStateGenerationInfo buildStateGenerationInfo(std::vector const& subTreeRoots, std::vector> const& symmetries) const; - size_t stateSize() const { - return mStateSize; + size_t stateVectorSize() const { + return mStateVectorSize; } size_t nrElements() const { @@ -77,34 +139,8 @@ namespace storm { return mNrOfBEs; } - size_t usageInfoBits() const { - return mUsageInfoBits; - } - - size_t usageIndex(size_t id) const { - assert(mUsageIndex.find(id) != mUsageIndex.end()); - return mUsageIndex.find(id)->second; - } - - size_t failureIndex(size_t id) const { - return mIdToFailureIndex[id]; - } - - void initializeUses(DFTState& state) const { - for(auto const& elem : mElements) { - if(elem->isSpareGate()) { - std::static_pointer_cast>(elem)->initializeUses(state); - } - } - } - - void initializeActivation(DFTState& state) const { - state.activate(mTopLevelIndex); - for(auto const& elem : mTopModule) { - if(mElements[elem]->isSpareGate()) { - propagateActivation(state, state.uses(elem)); - } - } + size_t getTopLevelIndex() const { + return mTopLevelIndex; } std::vector getSpareIndices() const { @@ -130,15 +166,6 @@ namespace storm { return mDependencies; } - void propagateActivation(DFTState& state, size_t representativeId) const { - state.activate(representativeId); - for(size_t id : module(representativeId)) { - if(mElements[id]->isSpareGate()) { - propagateActivation(state, state.uses(id)); - } - } - } - std::vector nonColdBEs() const { std::vector result; for(DFTElementPointer elem : mElements) { @@ -170,10 +197,6 @@ namespace storm { return getElement(index)->isDependency(); } -// std::shared_ptr const> getGate(size_t index) const { -// return -// } - std::shared_ptr const> getBasicElement(size_t index) const { assert(isBasicElement(index)); return std::static_pointer_cast const>(mElements[index]); @@ -198,6 +221,15 @@ namespace storm { } return elements; } + + bool isRepresentative(size_t id) const { + for (auto const& parent : getElement(id)->parents()) { + if (parent->isSpareGate()) { + return true; + } + } + return false; + } bool hasRepresentant(size_t id) const { return mRepresentants.find(id) != mRepresentants.end(); diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 1a3c5b512..11fc31948 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -936,10 +936,6 @@ namespace storm { template class DFTSpare : public DFTGate { - private: - size_t mUseIndex; - size_t mActiveIndex; - public: DFTSpare(size_t id, std::string const& name, std::vector>> const& children = {}) : DFTGate(id, name, children) @@ -957,24 +953,11 @@ namespace storm { return true; } - void setUseIndex(size_t useIndex) { - mUseIndex = useIndex; - } - - void setActiveIndex(size_t activeIndex) { - mActiveIndex = activeIndex; - } - - void initializeUses(storm::storage::DFTState& state) { - assert(this->mChildren.size() > 0); - state.setUsesAtPosition(mUseIndex, this->mChildren[0]->id()); - } - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { if(state.isOperational(this->mId)) { - size_t uses = state.extractUses(mUseIndex); + size_t uses = state.uses(this->mId); if(!state.isOperational(uses)) { - bool claimingSuccessful = state.claimNew(this->mId, mUseIndex, uses, this->mChildren); + bool claimingSuccessful = state.claimNew(this->mId, uses, this->mChildren); if(!claimingSuccessful) { this->fail(state, queues); } @@ -984,7 +967,7 @@ namespace storm { void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { if(state.isOperational(this->mId)) { - if(state.isFailsafe(state.extractUses((mUseIndex)))) { + if(state.isFailsafe(state.uses(this->mId))) { this->failsafe(state, queues); this->childrenDontCare(state, queues); } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 9916bbe0e..c3f7c9f32 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -6,13 +6,27 @@ namespace storm { namespace storage { template - DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft) { + DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { mInactiveSpares = dft.getSpareIndices(); - dft.initializeUses(*this); - dft.initializeActivation(*this); + + // Initialize uses + for(size_t id : mDft.getSpareIndices()) { + std::shared_ptr const> elem = mDft.getGate(id); + assert(elem->isSpareGate()); + assert(elem->nrChildren() > 0); + this->setUses(id, elem->children()[0]->id()); + } + + // Initialize activation + this->activate(mDft.getTopLevelIndex()); + for(auto const& id : mDft.module(mDft.getTopLevelIndex())) { + if(mDft.getElement(id)->isSpareGate()) { + propagateActivation(uses(id)); + } + } + std::vector alwaysActiveBEs = dft.nonColdBEs(); mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); - } template @@ -27,7 +41,7 @@ namespace storm { template int DFTState::getElementStateInt(size_t id) const { - return mStatus.getAsInt(mDft.failureIndex(id), 2); + return mStatus.getAsInt(mStateGenerationInfo.getStateIndex(id), 2); } template @@ -47,12 +61,12 @@ namespace storm { template bool DFTState::hasFailed(size_t id) const { - return mStatus[mDft.failureIndex(id)]; + return mStatus[mStateGenerationInfo.getStateIndex(id)]; } template bool DFTState::isFailsafe(size_t id) const { - return mStatus[mDft.failureIndex(id)+1]; + return mStatus[mStateGenerationInfo.getStateIndex(id)+1]; } template @@ -67,38 +81,38 @@ namespace storm { template bool DFTState::dependencySuccessful(size_t id) const { - return mStatus[mDft.failureIndex(id)]; + return mStatus[mStateGenerationInfo.getStateIndex(id)]; } template bool DFTState::dependencyUnsuccessful(size_t id) const { - return mStatus[mDft.failureIndex(id)+1]; + return mStatus[mStateGenerationInfo.getStateIndex(id)+1]; } template void DFTState::setFailed(size_t id) { - mStatus.set(mDft.failureIndex(id)); + mStatus.set(mStateGenerationInfo.getStateIndex(id)); } template void DFTState::setFailsafe(size_t id) { - mStatus.set(mDft.failureIndex(id)+1); + mStatus.set(mStateGenerationInfo.getStateIndex(id)+1); } template void DFTState::setDontCare(size_t id) { - mStatus.setFromInt(mDft.failureIndex(id), 2, static_cast(DFTElementState::DontCare) ); + mStatus.setFromInt(mStateGenerationInfo.getStateIndex(id), 2, static_cast(DFTElementState::DontCare) ); } template void DFTState::setDependencySuccessful(size_t id) { // No distinction between successful dependency and no dependency at all - // -> we do not set bit - //mStatus.set(mDft.failureIndex(id)); + // => we do not set bit + //mStatus.set(mStateGenerationInfo.mIdToStateIndex(id)); } template void DFTState::setDependencyUnsuccessful(size_t id) { - mStatus.set(mDft.failureIndex(id)+1); + mStatus.set(mStateGenerationInfo.getStateIndex(id)+1); } template @@ -158,8 +172,7 @@ namespace storm { template void DFTState::activate(size_t repr) { - std::vector const& module = mDft.module(repr); - for(size_t elem : module) { + for(size_t elem : mDft.module(repr)) { if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) { mIsCurrentlyFailableBE.push_back(elem); } @@ -175,16 +188,26 @@ namespace storm { assert(mDft.getElement(id)->isSpareGate()); return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end()); } + + template + void DFTState::propagateActivation(size_t representativeId) { + activate(representativeId); + for(size_t id : mDft.module(representativeId)) { + if(mDft.getElement(id)->isSpareGate()) { + propagateActivation(uses(id)); + } + } + } template uint_fast64_t DFTState::uses(size_t id) const { - return extractUses(mDft.usageIndex(id)); + return extractUses(mStateGenerationInfo.getSpareUsageIndex(id)); } template uint_fast64_t DFTState::extractUses(size_t from) const { - assert(mDft.usageInfoBits() < 64); - return mStatus.getAsInt(from, mDft.usageInfoBits()); + assert(mStateGenerationInfo.usageInfoBits() < 64); + return mStatus.getAsInt(from, mStateGenerationInfo.usageInfoBits()); } template @@ -193,13 +216,13 @@ namespace storm { } template - void DFTState::setUsesAtPosition(size_t usageIndex, size_t child) { - mStatus.setFromInt(usageIndex, mDft.usageInfoBits(), child); + void DFTState::setUses(size_t spareId, size_t child) { + mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), child); mUsedRepresentants.push_back(child); } template - bool DFTState::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector>> const& children) { + bool DFTState::claimNew(size_t spareId, size_t currentlyUses, std::vector>> const& children) { auto it = children.begin(); while ((*it)->id() != currentlyUses) { assert(it != children.end()); @@ -209,9 +232,9 @@ namespace storm { while(it != children.end()) { size_t childId = (*it)->id(); if(!hasFailed(childId) && !isUsed(childId)) { - setUsesAtPosition(usageIndex, childId); + setUses(spareId, childId); if(isActiveSpare(spareId)) { - mDft.propagateActivation(*this, childId); + propagateActivation(childId); } return true; } diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 450953bd7..fcbcdc62d 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -17,6 +17,7 @@ namespace storm { class DFTBE; template class DFTElement; + class DFTStateGenerationInfo; template class DFTState { @@ -31,9 +32,10 @@ namespace storm { std::vector mUsedRepresentants; bool mValid = true; const DFT& mDft; + const DFTStateGenerationInfo& mStateGenerationInfo; public: - DFTState(DFT const& dft, size_t id); + DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id); DFTElementState getElementState(size_t id) const; @@ -75,6 +77,8 @@ namespace storm { bool isActiveSpare(size_t id) const; + void propagateActivation(size_t representativeId); + void markAsInvalid() { mValid = false; } @@ -109,13 +113,13 @@ namespace storm { bool isUsed(size_t child) const; /** - * Sets to to the usageIndex which child is now used. - * @param usageIndex - * @param child + * Sets for the spare which child is now used. + * @param spareId Id of the spare + * @param child Id of the child which is now used */ - void setUsesAtPosition(size_t usageIndex, size_t child); + void setUses(size_t spareId, size_t child); - bool claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector>> const& children); + bool claimNew(size_t spareId, size_t currentlyUses, std::vector>> const& children); bool hasOutgoingEdges() const { return !mIsCurrentlyFailableBE.empty(); diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 49b573f33..7b7cea029 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -6,6 +6,8 @@ #include "utility/storm.h" #include "storage/dft/DFTIsomorphism.h" +#include + /*! * Load DFT from filename, build corresponding Model and check against given property. * @@ -23,8 +25,8 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false) if(symred) { std::cout << dft.getElementsString() << std::endl; auto colouring = dft.colourDFT(); - auto res = dft.findSymmetries(colouring); - std::cout << res; + storm::storage::DFTIndependentSymmetries symmetries = dft.findSymmetries(colouring); + std::cout << symmetries; } // Building Markov Automaton @@ -74,6 +76,20 @@ int main(int argc, char** argv) { } else if (option == "--probability") { assert(pctlFormula.empty()); pctlFormula = "P=? [F \"failed\"]"; + } else if (option == "--timebound") { + assert(pctlFormula.empty()); + ++i; + assert(i < argc); + double timeBound; + try { + timeBound = boost::lexical_cast(argv[i]); + } catch (boost::bad_lexical_cast e) { + std::cerr << "The time bound '" << argv[i] << "' is not valid." << std::endl; + return 2; + } + std::stringstream stream; + stream << "P=? [F<=" << timeBound << " \"failed\"]"; + pctlFormula = stream.str(); } else if (option == "--trace") { level = log4cplus::TRACE_LOG_LEVEL; } else if (option == "--debug") {