From 53f2fdf51e1387e1bc5e9d0d0c32a8ab3a6bbf65 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Fri, 10 Apr 2015 16:08:59 +0200 Subject: [PATCH] Changed implementation of LRA to be weighted with the probability to reach BSCCs instead of choosing min/max Former-commit-id: 347fda8e2226b08a30265b4ad39715454efc4889 --- .../prctl/SparseDtmcPrctlModelChecker.cpp | 66 +++++++------------ .../prctl/SparseDtmcPrctlModelChecker.h | 2 +- 2 files changed, 24 insertions(+), 44 deletions(-) diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 4e35fef9c..1f8642b54 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -301,7 +301,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlModelChecker::computeLongRunAverageHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const { + std::vector SparseDtmcPrctlModelChecker::computeLongRunAverageHelper(storm::storage::BitVector const& psiStates, bool qualitative) const { // If there are no goal states, we avoid the computation and directly return zero. auto numOfStates = this->getModel().getNumberOfStates(); if (psiStates.empty()) { @@ -319,71 +319,51 @@ namespace storm { // Get some data members for convenience. typename storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); - // Now start with compute the long-run average for all BSCCs in isolation. - std::vector lraValuesForBsccs; - - // While doing so, we already gather some information for the following steps. - std::vector stateToBsccIndexMap(numOfStates); - storm::storage::BitVector statesInBsccs(numOfStates); + // First we check which states are in BSCCs. We use this later to speed up reachability analysis + storm::storage::BitVector statesNotInBsccs(numOfStates, true); for (uint_fast64_t currentBsccIndex = 0; currentBsccIndex < bsccDecomposition.size(); ++currentBsccIndex) { storm::storage::StronglyConnectedComponent const& bscc = bsccDecomposition[currentBsccIndex]; // Gather information for later use. for (auto const& state : bscc) { - statesInBsccs.set(state); - stateToBsccIndexMap[state] = currentBsccIndex; + statesNotInBsccs.set(state, false); } - - // Compute the LRA value for the current BSCC - lraValuesForBsccs.push_back(this->computeLraForBSCC(transitionMatrix, psiStates, bscc)); } - // For fast transition rewriting, we build some auxiliary data structures. - storm::storage::BitVector statesNotContainedInAnyBscc = ~statesInBsccs; - // Prepare result vector. std::vector result(numOfStates); - //Set the values for all states in BSCCs. - for (auto state : statesInBsccs) { - result[state] = lraValuesForBsccs[stateToBsccIndexMap[state]]; - } + //now we calculate the long run average for each BSCC in isolation and compute the weighted contribution of the BSCC to the LRA value of all states + for (uint_fast64_t currentBsccIndex = 0; currentBsccIndex < bsccDecomposition.size(); ++currentBsccIndex) { + storm::storage::StronglyConnectedComponent const& bscc = bsccDecomposition[currentBsccIndex]; - //for all states not in any bscc set the result to the minimal/maximal value of the reachable BSCCs - //there might be a more efficient way to do this... - for (auto state : statesNotContainedInAnyBscc){ - - //calculate what result values the reachable states in BSCCs have - storm::storage::BitVector currentState(numOfStates); - currentState.set(state); - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates( - transitionMatrix, currentState, storm::storage::BitVector(numOfStates, true), statesInBsccs - ); - - storm::storage::BitVector reachableBsccStates = statesInBsccs & reachableStates; - std::vector reachableResults(reachableBsccStates.getNumberOfSetBits()); - storm::utility::vector::selectVectorValues(reachableResults, reachableBsccStates, result); - - //now select the minimal/maximal element - if (minimize){ - result[state] = *std::min_element(reachableResults.begin(), reachableResults.end()); - } else { - result[state] = *std::max_element(reachableResults.begin(), reachableResults.end()); + storm::storage::BitVector statesInThisBsccs(numOfStates); + for (auto const& state : bscc) { + statesInThisBsccs.set(state); } + + ValueType lraForThisBscc = this->computeLraForBSCC(transitionMatrix, psiStates, bscc); + + //the LRA value of a BSCC contributes to the LRA value of a state with the probability of reaching that BSCC from that state + //thus we add Prob(Eventually statesInThisBscc) * lraForThisBscc to the result vector + + //the reachability probabilities will be zero in other BSCCs, thus we can set the left operand of the until formula to statesNotInBsccs as an optimization + std::vector reachProbThisBscc = this->computeUntilProbabilitiesHelper(statesNotInBsccs, statesInThisBsccs, false); + + storm::utility::vector::scaleVectorInPlace(reachProbThisBscc, lraForThisBscc); + storm::utility::vector::addVectorsInPlace(result, reachProbThisBscc); } return result; } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - + std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType = boost::optional()) { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeLongRunAverageHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeLongRunAverageHelper(subResult.getTruthValuesVector(), qualitative))); } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index d1e880e1a..d1f3edb60 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -37,7 +37,7 @@ namespace storm { std::vector computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const; std::vector computeCumulativeRewardsHelper(uint_fast64_t stepBound) const; std::vector computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const; - std::vector computeLongRunAverageHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const; + std::vector computeLongRunAverageHelper(storm::storage::BitVector const& psiStates, bool qualitative) const; static ValueType computeLraForBSCC(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& goalStates, storm::storage::StronglyConnectedComponent const& bscc);