From 8ed4a5f849356a5995dee92e6095c7a8cc3587d0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 22 Dec 2015 15:48:50 +0100 Subject: [PATCH] some refactoring in elimination-based model checker Former-commit-id: 1fb6741479da84e959188ea29884da93a46c8e90 --- .../SparseDtmcEliminationModelChecker.cpp | 172 +++++++++++------- .../SparseDtmcEliminationModelChecker.h | 20 +- src/utility/constants.cpp | 4 +- 3 files changed, 126 insertions(+), 70 deletions(-) diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index be8819d86..d5d0f16b8 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -75,7 +75,7 @@ namespace storm { } template - SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model) : SparsePropositionalModelChecker(model) { + SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model, bool computeResultsForInitialStatesOnly) : SparsePropositionalModelChecker(model), computeResultsForInitialStatesOnly(computeResultsForInitialStatesOnly) { // Intentionally left empty. } @@ -123,40 +123,61 @@ namespace storm { storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - // Do some sanity checks to establish some required properties. - STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); - // Then, compute the subset of states that has a probability of 0 or 1, respectively. std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - - // If the initial state is known to have either probability 0 or 1, we can directly return the result. - if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { - STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step."); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, statesWithProbability0.get(*this->getModel().getInitialStates().begin()) ? storm::utility::zero() : storm::utility::one())); + + // Determine whether we need to perform some further computation. + bool furtherComputationNeeded = true; + if (computeResultsForInitialStatesOnly && this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { + STORM_LOG_DEBUG("The probability for all initial states was found in a preprocessing step."); + furtherComputationNeeded = false; + } else if (maybeStates.empty()) { + STORM_LOG_DEBUG("The probability for all states was found in a preprocessing step."); + furtherComputationNeeded = false; } - // Determine the set of states that is reachable from the initial state without jumping over a target state. - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, statesWithProbability1); - - // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). - maybeStates &= reachableStates; - - // Create a vector for the probabilities to go to a state with probability 1 in one step. - std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); - - // Determine the set of initial states of the sub-model. - storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; - - // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); - storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - - boost::optional> missingStateRewards; - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards))); + std::vector result(maybeStates.size()); + if (furtherComputationNeeded) { + // If we compute the results for the initial states only, we can cut off all maybe state that are not + // reachable from them. + if (computeResultsForInitialStatesOnly) { + // Determine the set of states that is reachable from the initial state without jumping over a target state. + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, statesWithProbability1); + + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). + maybeStates &= reachableStates; + } + + // Create a vector for the probabilities to go to a state with probability 1 in one step. + std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); + + // Determine the set of initial states of the sub-model. + storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; + + // We then build the submatrix that only has the transitions of the maybe states. + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); + + boost::optional> missingStateRewards; + std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards); + storm::utility::vector::setVectorValues(result, maybeStates, subresult); + } + + // Construct full result. + storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); + storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); + + // Construct check result based on whether we have computed values for all states or just the initial states. + std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); + if (computeResultsForInitialStatesOnly) { + // If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the + // result to only communicate these results. + checkResult->filter(ExplicitQualitativeCheckResult(~maybeStates | this->getModel().getInitialStates())); + } + return checkResult; } template @@ -169,8 +190,6 @@ namespace storm { // Do some sanity checks to establish some required properties. RewardModelType const& rewardModel = this->getModel().getRewardModel(rewardModelName ? rewardModelName.get() : ""); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); - STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); // Then, compute the subset of states that has a reachability reward less than infinity. storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); @@ -178,37 +197,60 @@ namespace storm { infinityStates.complement(); storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates; - // If the initial state is known to have 0 reward or an infinite reward value, we can directly return the result. - if (infinityStates.get(initialState)) { - STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); - // This is a work around, because not all (e.g. storm::RationalFunction) data types can represent an - // infinity value. - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, storm::utility::infinity())); + // Determine whether we need to perform some further computation. + bool furtherComputationNeeded = true; + if (computeResultsForInitialStatesOnly) { + if (this->getModel().getInitialStates().isSubsetOf(infinityStates)) { + STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); + furtherComputationNeeded = false; + } + if (this->getModel().getInitialStates().isSubsetOf(psiStates)) { + STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); + furtherComputationNeeded = false; + } } - if (psiStates.get(initialState)) { - STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, storm::utility::zero())); + + std::vector result(maybeStates.size()); + if (furtherComputationNeeded) { + // If we compute the results for the initial states only, we can cut off all maybe state that are not + // reachable from them. + if (computeResultsForInitialStatesOnly) { + // Determine the set of states that is reachable from the initial state without jumping over a target state. + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, psiStates); + + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). + maybeStates &= reachableStates; + } + + // Create a vector for the probabilities to go to a state with probability 1 in one step. + std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates); + + // Determine the set of initial states of the sub-model. + storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; + + // We then build the submatrix that only has the transitions of the maybe states. + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); + + // Project the state reward vector to all maybe-states. + boost::optional> optionalStateRewards = rewardModel.getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), maybeStates); + + std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, optionalStateRewards); + storm::utility::vector::setVectorValues(result, maybeStates, subresult); } - // Determine the set of states that is reachable from the initial state without jumping over a target state. - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, psiStates); - - // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). - maybeStates &= reachableStates; - - // Create a vector for the probabilities to go to a state with probability 1 in one step. - std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates); - - // Determine the set of initial states of the sub-model. - storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; - - // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); - storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - - // Project the state reward vector to all maybe-states. - boost::optional> optionalStateRewards = rewardModel.getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), maybeStates); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, optionalStateRewards))); + // Construct full result. + storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::zero()); + + // Construct check result based on whether we have computed values for all states or just the initial states. + std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); + if (computeResultsForInitialStatesOnly) { + // If we computed the results for the initial (and inf) states only, we need to filter the result to + // only communicate these results. + checkResult->filter(ExplicitQualitativeCheckResult(~maybeStates | this->getModel().getInitialStates())); + } + return checkResult; } template @@ -534,7 +576,7 @@ namespace storm { } template - typename SparseDtmcEliminationModelChecker::ValueType SparseDtmcEliminationModelChecker::computeReachabilityValue(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional>& stateRewards) { + std::vector::ValueType> SparseDtmcEliminationModelChecker::computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional>& stateRewards) { std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); @@ -622,9 +664,15 @@ namespace storm { // Now, we return the value for the only initial state. STORM_LOG_DEBUG("Simplifying and returning result."); if (stateRewards) { - return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]); + for (auto& reward : stateRewards.get()) { + reward = storm::utility::simplify(reward); + } + return stateRewards.get(); } else { - return oneStepProbabilities[*initialStates.begin()]; + for (auto& probability : oneStepProbabilities) { + probability = storm::utility::simplify(probability); + } + return oneStepProbabilities; } } @@ -746,7 +794,7 @@ namespace storm { } } if (!stateRewards) { - oneStepProbabilities[state] = oneStepProbabilities[state] * loopProbability; + oneStepProbabilities[state] = storm::utility::simplify(oneStepProbabilities[state] * loopProbability); } } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 0d85cd906..a52ef227f 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -15,7 +15,13 @@ namespace storm { typedef typename SparseDtmcModelType::ValueType ValueType; typedef typename SparseDtmcModelType::RewardModelType RewardModelType; - explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model); + /*! + * Creates an elimination-based model checker for the given model. + * + * @param model The model to analyze. + * @param computeResultsForInitialStatesOnly If set to true, the results are only computed for + */ + explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model, bool computeResultsForInitialStatesOnly = true); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; @@ -45,11 +51,10 @@ namespace storm { void print() const; /*! - * Checks whether the given state has a self-loop with an arbitrary probability in the given probability matrix. + * Checks whether the given state has a self-loop with an arbitrary probability in the probability matrix. * * @param state The state for which to check whether it possesses a self-loop. - * @param matrix The matrix in which to look for the loop. - * @return True iff the given state has a self-loop with an arbitrary probability in the given probability matrix. + * @return True iff the given state has a self-loop with an arbitrary probability in the probability matrix. */ bool hasSelfLoop(storm::storage::sparse::state_type state); @@ -101,7 +106,7 @@ namespace storm { PenaltyFunctionType penaltyFunction; }; - static ValueType computeReachabilityValue(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional>& stateRewards); + static std::vector computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional>& stateRewards); static std::unique_ptr createStatePriorityQueue(boost::optional> const& stateDistances, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); @@ -122,11 +127,14 @@ namespace storm { static std::vector getStateDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward); static uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); - + static uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); static bool checkConsistent(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions); + // A flag that indicates whether this model checker is supposed to produce results for all states or just for the initial states. + bool computeResultsForInitialStatesOnly; + }; } // namespace modelchecker diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index bba5fd160..900482a72 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -73,8 +73,8 @@ namespace storm { template<> storm::RationalFunction infinity() { - // FIXME: this does not work. - return storm::RationalFunction(carl::rationalize(std::numeric_limits::infinity())); + // FIXME: this should be treated more properly. + return storm::RationalFunction(-1.0); } #endif