From 8cbfccba225ef5d00c16aa4e1cc578333db69ebe Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 10 Mar 2017 23:03:25 +0100 Subject: [PATCH] Hacked approximation for probabilities --- .../builder/DftExplorationHeuristic.h | 4 +- .../builder/ExplicitDFTModelBuilderApprox.cpp | 76 +++++++++++++++++-- .../builder/ExplicitDFTModelBuilderApprox.h | 17 +++-- .../modelchecker/dft/DFTModelChecker.cpp | 7 +- src/storm-dft/storage/BucketPriorityQueue.h | 2 +- 5 files changed, 87 insertions(+), 19 deletions(-) diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h index 874cfb586..f4cc3c1ce 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.h +++ b/src/storm-dft/builder/DftExplorationHeuristic.h @@ -107,8 +107,8 @@ namespace storm { } bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType, ValueType) override { - if (predecessor.getDepth() < this->depth) { - this->depth = predecessor.getDepth(); + if (predecessor.getDepth() + 1 < this->depth) { + this->depth = predecessor.getDepth() + 1; return true; } return false; diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 65d9f838b..8483aa3fd 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -65,7 +65,7 @@ namespace storm { { // Intentionally left empty. // TODO Matthias: remove again - usedHeuristic = storm::builder::ApproximationHeuristic::NONE; + usedHeuristic = storm::builder::ApproximationHeuristic::DEPTH; // Compute independent subtrees if (dft.topLevelType() == storm::storage::DFTElementType::OR) { @@ -349,8 +349,8 @@ namespace storm { // Try to explore the next state generator.load(currentState); - if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) { - //if (currentExplorationHeuristic->isSkip(approximationThreshold)) { + //if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) { + if (approximationThreshold > 0.0 && currentExplorationHeuristic->isSkip(approximationThreshold)) { // Skip the current state ++nrSkippedStates; STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); @@ -397,6 +397,7 @@ namespace storm { STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state."); // Initialize bounds + // TODO Mathias: avoid hack ValueType lowerBound = getLowerBound(state); ValueType upperBound = getUpperBound(state); heuristic->setBounds(lowerBound, upperBound); @@ -478,10 +479,70 @@ namespace storm { } template - std::shared_ptr> ExplicitDFTModelBuilderApprox::getModelApproximation(bool lowerBound) { - // TODO Matthias: handle case with no skipped states - changeMatrixBound(modelComponents.transitionMatrix, lowerBound); - return createModel(true); + std::shared_ptr> ExplicitDFTModelBuilderApprox::getModelApproximation(bool lowerBound, bool expectedTime) { + if (expectedTime) { + // TODO Matthias: handle case with no skipped states + changeMatrixBound(modelComponents.transitionMatrix, lowerBound); + return createModel(true); + } else { + // Change model for probabilities + // TODO Matthias: make nicer + storm::storage::SparseMatrix matrix = modelComponents.transitionMatrix; + storm::models::sparse::StateLabeling labeling = modelComponents.stateLabeling; + if (lowerBound) { + // Set self loop for lower bound + for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { + auto matrixEntry = matrix.getRow(it->first, 0).begin(); + STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state."); + STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); + matrixEntry->setValue(storm::utility::one()); + matrixEntry->setColumn(it->first); + } + } else { + // Make skipped states failed states for upper bound + storm::storage::BitVector failedStates = modelComponents.stateLabeling.getStates("failed"); + for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { + failedStates.set(it->first); + } + labeling.setStates("failed", failedStates); + } + + std::shared_ptr> model; + if (modelComponents.deterministicModel) { + model = std::make_shared>(std::move(matrix), std::move(labeling)); + } else { + // Build MA + // Compute exit rates + // TODO Matthias: avoid computing multiple times + modelComponents.exitRates = std::vector(modelComponents.markovianStates.size()); + std::vector::index_type> indices = matrix.getRowGroupIndices(); + for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) { + if (modelComponents.markovianStates[stateIndex]) { + modelComponents.exitRates[stateIndex] = matrix.getRowSum(indices[stateIndex]); + } else { + modelComponents.exitRates[stateIndex] = storm::utility::zero(); + } + } + STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); + + std::shared_ptr> ma = std::make_shared>(std::move(matrix), std::move(labeling), modelComponents.markovianStates, modelComponents.exitRates); + if (ma->hasOnlyTrivialNondeterminism()) { + // Markov automaton can be converted into CTMC + // TODO Matthias: change components which were not moved accordingly + model = ma->convertToCTMC(); + } else { + model = ma; + } + + } + + if (model->getNumberOfStates() <= 15) { + STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix()); + } else { + STORM_LOG_TRACE("Transition matrix: too big to print"); + } + return model; + } } template @@ -573,6 +634,7 @@ namespace storm { if (state->hasFailed(dft.getTopLevelIndex())) { return storm::utility::zero(); } + // Get the upper bound by considering the failure of all BEs ValueType upperBound = storm::utility::one(); ValueType rateSum = storm::utility::zero(); diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h index d7ee37de5..97439f47a 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h @@ -29,7 +29,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicNone; + using ExplorationHeuristic = DFTExplorationHeuristicDepth; using ExplorationHeuristicPointer = std::shared_ptr; @@ -197,11 +197,12 @@ namespace storm { /*! * Get the built approximation model for either the lower or upper bound. * - * @param lowerBound If true, the lower bound model is returned, else the upper bound model + * @param lowerBound If true, the lower bound model is returned, else the upper bound model + * @param expectedTime If true, the bounds for expected time are computed, else the bounds for probabilities. * * @return The model built from the DFT. */ - std::shared_ptr> getModelApproximation(bool lowerBound = true); + std::shared_ptr> getModelApproximation(bool lowerBound, bool expectedTime); private: @@ -243,14 +244,16 @@ namespace storm { /** * Change matrix to reflect the lower or upper approximation bound. * - * @param matrix Matrix to change. The change are reflected here. - * @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used. + * @param matrix Matrix to change. The change are reflected here. + * @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used. */ void changeMatrixBound(storm::storage::SparseMatrix & matrix, bool lowerBound) const; /*! * Get lower bound approximation for state. * + * @param state The state. + * * @return Lower bound approximation. */ ValueType getLowerBound(DFTStatePointer const& state) const; @@ -258,6 +261,8 @@ namespace storm { /*! * Get upper bound approximation for state. * + * @param state The state. + * * @return Upper bound approximation. */ ValueType getUpperBound(DFTStatePointer const& state) const; @@ -310,7 +315,7 @@ namespace storm { bool enableDC = true; //TODO Matthias: make changeable - const bool mergeFailedStates = false; + const bool mergeFailedStates = true; // Heuristic used for approximation storm::builder::ApproximationHeuristic usedHeuristic; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 0ecf2718f..79ed0ef95 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -303,7 +303,7 @@ namespace storm { // Build model for lower bound STORM_LOG_INFO("Getting model for lower bound..."); - model = builder.getModelApproximation(probabilityFormula ? false : true); + model = builder.getModelApproximation(true, !probabilityFormula); // We only output the info from the lower bound as the info for the upper bound is the same model->printModelInformationToStream(std::cout); buildingTimer.stop(); @@ -317,15 +317,16 @@ namespace storm { // Build model for upper bound STORM_LOG_INFO("Getting model for upper bound..."); buildingTimer.start(); - model = builder.getModelApproximation(probabilityFormula ? true : false); + model = builder.getModelApproximation(false, !probabilityFormula); buildingTimer.stop(); // Check upper bound - newResult = checkModel(model, {properties}); + newResult = checkModel(model, {property}); STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second); approxResult.second = newResult[0]; ++iteration; + STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second), "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second); STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); totalTimer.stop(); printTimings(); diff --git a/src/storm-dft/storage/BucketPriorityQueue.h b/src/storm-dft/storage/BucketPriorityQueue.h index 5acd178d6..004469f9a 100644 --- a/src/storm-dft/storage/BucketPriorityQueue.h +++ b/src/storm-dft/storage/BucketPriorityQueue.h @@ -13,7 +13,7 @@ namespace storm { template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio);