From 8ce9e56af8f09b4ce6e778025bffca6304d39a12 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 18 Jun 2016 14:53:58 +0200 Subject: [PATCH] some refactoring of state-elimination-related things Former-commit-id: c51fd9c47c6154efdb8ab39672c75e30a179b812 --- src/adapters/EigenAdapter.cpp | 4 +- .../SparseDtmcEliminationModelChecker.cpp | 344 ++++-------------- .../SparseDtmcEliminationModelChecker.h | 69 +--- src/models/sparse/MarkovAutomaton.cpp | 4 +- .../ConditionalEliminator.cpp | 56 ++- .../stateelimination/ConditionalEliminator.h | 29 +- .../DynamicStatePriorityQueue.cpp | 75 ++++ .../DynamicStatePriorityQueue.h | 48 +++ .../LongRunAverageEliminator.cpp | 39 +- .../LongRunAverageEliminator.h | 20 +- src/solver/stateelimination/MAEliminator.cpp | 46 --- src/solver/stateelimination/MAEliminator.h | 32 -- .../PrioritizedEliminator.cpp | 46 --- .../stateelimination/PrioritizedEliminator.h | 35 -- .../PrioritizedStateEliminator.cpp | 39 ++ .../PrioritizedStateEliminator.h | 33 ++ .../stateelimination/StateEliminator.cpp | 66 ++-- src/solver/stateelimination/StateEliminator.h | 29 +- .../stateelimination/StatePriorityQueue.cpp | 13 + .../stateelimination/StatePriorityQueue.h | 21 ++ .../StaticStatePriorityQueue.cpp | 28 ++ .../StaticStatePriorityQueue.h | 26 ++ src/utility/stateelimination.cpp | 160 ++++++++ src/utility/stateelimination.h | 60 +++ 24 files changed, 702 insertions(+), 620 deletions(-) create mode 100644 src/solver/stateelimination/DynamicStatePriorityQueue.cpp create mode 100644 src/solver/stateelimination/DynamicStatePriorityQueue.h delete mode 100644 src/solver/stateelimination/MAEliminator.cpp delete mode 100644 src/solver/stateelimination/MAEliminator.h delete mode 100644 src/solver/stateelimination/PrioritizedEliminator.cpp delete mode 100644 src/solver/stateelimination/PrioritizedEliminator.h create mode 100644 src/solver/stateelimination/PrioritizedStateEliminator.cpp create mode 100644 src/solver/stateelimination/PrioritizedStateEliminator.h create mode 100644 src/solver/stateelimination/StatePriorityQueue.cpp create mode 100644 src/solver/stateelimination/StatePriorityQueue.h create mode 100644 src/solver/stateelimination/StaticStatePriorityQueue.cpp create mode 100644 src/solver/stateelimination/StaticStatePriorityQueue.h create mode 100644 src/utility/stateelimination.cpp create mode 100644 src/utility/stateelimination.h diff --git a/src/adapters/EigenAdapter.cpp b/src/adapters/EigenAdapter.cpp index aebdcd0ef..45f5206bd 100644 --- a/src/adapters/EigenAdapter.cpp +++ b/src/adapters/EigenAdapter.cpp @@ -4,7 +4,7 @@ namespace storm { namespace adapters { template - static std::unique_ptr> toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix) { // Build a list of triplets and let Eigen care about the insertion. std::vector> triplets; triplets.reserve(matrix.getNonzeroEntryCount()); @@ -20,6 +20,6 @@ namespace storm { return result; } - template std::unique_ptr> toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); + template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); } } \ No newline at end of file diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 5a6045f66..d2a58b68c 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -18,67 +18,27 @@ #include "src/logic/FragmentSpecification.h" +#include "src/solver/stateelimination/LongRunAverageEliminator.h" +#include "src/solver/stateelimination/ConditionalEliminator.h" +#include "src/solver/stateelimination/PrioritizedStateEliminator.h" +#include "src/solver/stateelimination/StaticStatePriorityQueue.h" +#include "src/solver/stateelimination/DynamicStatePriorityQueue.h" + +#include "src/utility/stateelimination.h" #include "src/utility/graph.h" #include "src/utility/vector.h" #include "src/utility/macros.h" +#include "src/utility/constants.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/IllegalArgumentException.h" -#include "src/solver/stateelimination/LongRunAverageEliminator.h" -#include "src/solver/stateelimination/ConditionalEliminator.h" -#include "src/solver/stateelimination/PrioritizedEliminator.h" - namespace storm { namespace modelchecker { - template - uint_fast64_t estimateComplexity(ValueType const& value) { - return 1; - } - -#ifdef STORM_HAVE_CARL - template<> - uint_fast64_t estimateComplexity(storm::RationalFunction const& value) { - if (storm::utility::isConstant(value)) { - return 1; - } - if (value.denominator().isConstant()) { - return value.nominator().complexity(); - } else { - return value.denominator().complexity() * value.nominator().complexity(); - } - } -#endif - - bool eliminationOrderNeedsDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { - return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || - order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed || - order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Backward || - order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed; - } - - bool eliminationOrderNeedsForwardDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { - return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || - order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed; - } - - bool eliminationOrderNeedsReversedDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { - return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed || - order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed; - } - - bool eliminationOrderIsPenaltyBased(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { - return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::StaticPenalty || - order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::DynamicPenalty || - order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::RegularExpression; - } - - bool eliminationOrderIsStatic(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { - return eliminationOrderNeedsDistances(order) || order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::StaticPenalty; - } + using namespace storm::utility::stateelimination; template SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model) : SparsePropositionalModelChecker(model) { @@ -98,7 +58,7 @@ namespace storm { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - + storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); if (psiStates.empty()) { @@ -157,7 +117,7 @@ namespace storm { // Do some sanity checks to establish some required properties. RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); - + storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); STORM_LOG_THROW(initialStates.getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); @@ -167,7 +127,7 @@ namespace storm { // Get the state-reward values from the reward model. std::vector stateRewardValues = rewardModel.getTotalRewardVector(this->getModel().getTransitionMatrix()); - + storm::storage::BitVector maybeStates(stateRewardValues.size()); uint_fast64_t index = 0; for (auto const& value : stateRewardValues) { @@ -183,7 +143,7 @@ namespace storm { maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, allStates, maybeStates); std::vector result(numberOfStates, storm::utility::zero()); - + // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; if (checkTask.isOnlyInitialStatesRelevantSet() && initialStates.isDisjointFrom(maybeStates)) { @@ -221,7 +181,7 @@ namespace storm { std::chrono::high_resolution_clock::time_point sccDecompositionStart = std::chrono::high_resolution_clock::now(); storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowCount(), true), false, true); auto sccDecompositionEnd = std::chrono::high_resolution_clock::now(); - + std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. @@ -232,7 +192,7 @@ namespace storm { auto conversionEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); - + storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); boost::optional> distanceBasedPriorities; if (eliminationOrderNeedsDistances(order)) { @@ -265,11 +225,11 @@ namespace storm { std::vector averageTimeInStates(stateValues.size(), storm::utility::one()); // First, we eliminate all states in BSCCs (except for the representative states). - std::shared_ptr> priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs); - storm::solver::stateelimination::LongRunAverageEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, stateValues, averageTimeInStates); + std::shared_ptr priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs); + storm::solver::stateelimination::LongRunAverageEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, stateValues, averageTimeInStates); - while (priorityQueue->hasNextState()) { - storm::storage::sparse::state_type state = priorityQueue->popNextState(); + while (priorityQueue->hasNext()) { + storm::storage::sparse::state_type state = priorityQueue->pop(); stateEliminator.eliminateState(state, true); #ifdef STORM_DEV STORM_LOG_ASSERT(checkConsistent(flexibleMatrix, flexibleBackwardTransitions), "The forward and backward transition matrices became inconsistent."); @@ -294,7 +254,7 @@ namespace storm { } stateValues[*representativeIt] = bsccValue; } - + FlexibleRowType& representativeForwardRow = flexibleMatrix.getRow(*representativeIt); representativeForwardRow.clear(); representativeForwardRow.shrink_to_fit(); @@ -307,10 +267,10 @@ namespace storm { } } representativeBackwardRow.erase(it); - + ++representativeIt; } - + // If there are states remaining that are not in BSCCs, we need to eliminate them now. storm::storage::BitVector remainingStates = maybeStates & ~regularStatesInBsccs; @@ -388,7 +348,7 @@ namespace storm { storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); - + if (furtherComputationNeeded) { uint_fast64_t timeBound = pathFormula.getDiscreteTimeBound(); @@ -399,7 +359,7 @@ namespace storm { // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). statesWithProbabilityGreater0 &= reachableStates; } - + // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true); @@ -408,7 +368,7 @@ namespace storm { if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of initial states of the sub-model. storm::storage::BitVector subInitialStates = this->getModel().getInitialStates() % statesWithProbabilityGreater0; - + // Precompute the distances of the relevant states to the initial states. distancesFromInitialStates = storm::utility::graph::getDistances(submatrix, subInitialStates, statesWithProbabilityGreater0); @@ -471,23 +431,23 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - + std::vector result = computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet()); - + // Construct check result. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); return checkResult; } - + template std::vector SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly) { - + // Then, compute the subset of states that has a probability of 0 or 1, respectively. std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - + // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; if (computeForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) { @@ -497,7 +457,7 @@ namespace storm { STORM_LOG_DEBUG("The probability for all states was found in a preprocessing step."); furtherComputationNeeded = false; } - + 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 @@ -505,29 +465,29 @@ namespace storm { if (computeForInitialStatesOnly) { // 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(probabilityMatrix, initialStates, 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 = probabilityMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1); - + // Determine the set of initial states of the sub-model. storm::storage::BitVector newInitialStates = initialStates % maybeStates; - + // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - + std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, phiStates, psiStates, oneStepProbabilities); 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()); - + if (computeForInitialStatesOnly) { // 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. @@ -547,19 +507,19 @@ namespace storm { // Do some sanity checks to establish some required properties. RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); - + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); std::vector result = computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); }, checkTask.isOnlyInitialStatesRelevantSet()); - + // Construct check result. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); return checkResult; } - + template std::vector SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, bool computeForInitialStatesOnly) { return computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates, @@ -570,10 +530,10 @@ namespace storm { }, computeForInitialStatesOnly); } - + template std::vector SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly) { - + uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); // Compute the subset of states that has a reachability reward less than infinity. @@ -594,7 +554,7 @@ namespace storm { furtherComputationNeeded = false; } } - + 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 @@ -609,14 +569,14 @@ namespace storm { // Determine the set of initial states of the sub-model. storm::storage::BitVector newInitialStates = initialStates % maybeStates; - + // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); // Project the state reward vector to all maybe-states. std::vector stateRewardValues = totalStateRewardVectorGetter(submatrix.getRowCount(), probabilityMatrix, maybeStates); - + std::vector subresult = computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, trueStates, targetStates, probabilityMatrix.getConstrainedRowSumVector(maybeStates, targetStates)); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } @@ -711,21 +671,21 @@ namespace storm { storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); if (eliminationOrderNeedsDistances(order)) { distanceBasedPriorities = getDistanceBasedPriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities, - eliminationOrderNeedsForwardDistances(order), - eliminationOrderNeedsReversedDistances(order)); + eliminationOrderNeedsForwardDistances(order), + eliminationOrderNeedsReversedDistances(order)); } storm::storage::FlexibleSparseMatrix flexibleMatrix(submatrix); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(submatrixTransposed, true); - std::shared_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); - + std::shared_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); + STORM_LOG_INFO("Computing conditional probilities." << std::endl); uint_fast64_t numberOfStatesToEliminate = statePriorities->size(); STORM_LOG_INFO("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl); performPrioritizedStateElimination(statePriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, this->getModel().getInitialStates(), true); - storm::solver::stateelimination::ConditionalEliminator stateEliminator = storm::solver::stateelimination::ConditionalEliminator(flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, phiStates, psiStates); + storm::solver::stateelimination::ConditionalEliminator stateEliminator = storm::solver::stateelimination::ConditionalEliminator(flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, phiStates, psiStates); // Eliminate the transitions going into the initial state (if there are any). if (!flexibleBackwardTransitions.getRow(*newInitialStates.begin()).empty()) { @@ -752,6 +712,7 @@ namespace storm { // to eliminate all chains of non-psi states between the current state and psi states. bool hasNonPsiSuccessor = true; while (hasNonPsiSuccessor) { + stateEliminator.setFilterPhi(); hasNonPsiSuccessor = false; // Only treat the state if it has an outgoing transition other than a self-loop. @@ -764,9 +725,7 @@ namespace storm { // Eliminate the successor only if there possibly is a psi state reachable through it. if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) { STORM_LOG_TRACE("Found non-psi successor " << element.getColumn() << " that needs to be eliminated."); - stateEliminator.setStatePhi(); stateEliminator.eliminateState(element.getColumn(), false); - stateEliminator.clearState(); hasNonPsiSuccessor = true; } } @@ -774,6 +733,7 @@ namespace storm { STORM_LOG_ASSERT(!flexibleMatrix.getRow(initialStateSuccessor).empty(), "(1) New transitions expected to be non-empty."); } } + stateEliminator.unsetFilter(); } else { STORM_LOG_ASSERT(psiStates.get(initialStateSuccessor), "Expected psi state."); STORM_LOG_TRACE("Is a psi state."); @@ -784,6 +744,7 @@ namespace storm { bool hasNonPhiSuccessor = true; while (hasNonPhiSuccessor) { + stateEliminator.setFilterPsi(); hasNonPhiSuccessor = false; // Only treat the state if it has an outgoing transition other than a self-loop. @@ -795,15 +756,14 @@ namespace storm { FlexibleRowType const& successorRow = flexibleMatrix.getRow(element.getColumn()); if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) { STORM_LOG_TRACE("Found non-phi successor " << element.getColumn() << " that needs to be eliminated."); - stateEliminator.setStatePsi(); stateEliminator.eliminateState(element.getColumn(), false); - stateEliminator.clearState(); hasNonPhiSuccessor = true; } } } } } + stateEliminator.unsetFilter(); } } @@ -844,62 +804,12 @@ namespace storm { } template - std::shared_ptr> SparseDtmcEliminationModelChecker::createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states) { - - STORM_LOG_TRACE("Creating state priority queue for states " << states); - - // Get the settings to customize the priority queue. - storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); - - std::vector sortedStates(states.begin(), states.end()); - - if (order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Random) { - std::random_device randomDevice; - std::mt19937 generator(randomDevice()); - std::shuffle(sortedStates.begin(), sortedStates.end(), generator); - return std::make_unique(sortedStates); - } else { - if (eliminationOrderNeedsDistances(order)) { - STORM_LOG_THROW(static_cast(distanceBasedStatePriorities), storm::exceptions::InvalidStateException, "Unable to build state priority queue without distance-based priorities."); - std::sort(sortedStates.begin(), sortedStates.end(), [&distanceBasedStatePriorities] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distanceBasedStatePriorities.get()[state1] < distanceBasedStatePriorities.get()[state2]; } ); - return std::make_unique(sortedStates); - } else if (eliminationOrderIsPenaltyBased(order)) { - std::vector> statePenalties(sortedStates.size()); - PenaltyFunctionType penaltyFunction = order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression : computeStatePenalty; - for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) { - statePenalties[index] = std::make_pair(sortedStates[index], penaltyFunction(sortedStates[index], transitionMatrix, backwardTransitions, oneStepProbabilities)); - } - - std::sort(statePenalties.begin(), statePenalties.end(), [] (std::pair const& statePenalty1, std::pair const& statePenalty2) { return statePenalty1.second < statePenalty2.second; } ); - - if (eliminationOrderIsStatic(order)) { - // For the static penalty version, we need to strip the penalties to create the queue. - for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) { - sortedStates[index] = statePenalties[index].first; - } - return std::make_unique(sortedStates); - } else { - // For the dynamic penalty version, we need to give the full state-penalty pairs. - return std::make_unique(statePenalties, penaltyFunction); - } - } - } - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Illegal elimination order selected."); - } - - template - std::shared_ptr> SparseDtmcEliminationModelChecker::createNaivePriorityQueue(storm::storage::BitVector const& states) { - std::vector sortedStates(states.begin(), states.end()); - return std::shared_ptr>(new StaticStatePriorityQueue(sortedStates)); - } - - template - void SparseDtmcEliminationModelChecker::performPrioritizedStateElimination(std::shared_ptr>& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) { + void SparseDtmcEliminationModelChecker::performPrioritizedStateElimination(std::shared_ptr& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) { - storm::solver::stateelimination::PrioritizedEliminator stateEliminator(transitionMatrix, backwardTransitions, priorityQueue, values); + storm::solver::stateelimination::PrioritizedStateEliminator stateEliminator(transitionMatrix, backwardTransitions, priorityQueue, values); - while (priorityQueue->hasNextState()) { - storm::storage::sparse::state_type state = priorityQueue->popNextState(); + while (priorityQueue->hasNext()) { + storm::storage::sparse::state_type state = priorityQueue->pop(); bool removeForwardTransitions = computeResultsForInitialStatesOnly && !initialStates.get(state); stateEliminator.eliminateState(state, removeForwardTransitions); if (removeForwardTransitions) { @@ -913,7 +823,7 @@ namespace storm { template void SparseDtmcEliminationModelChecker::performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { - std::shared_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); + std::shared_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); std::size_t numberOfStatesToEliminate = statePriorities->size(); STORM_LOG_DEBUG("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl); @@ -932,7 +842,7 @@ namespace storm { if (storm::settings::getModule().isEliminateEntryStatesLastSet()) { STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); std::vector sortedStates(entryStateQueue.begin(), entryStateQueue.end()); - std::shared_ptr> queuePriorities = std::shared_ptr>(new StaticStatePriorityQueue(sortedStates)); + std::shared_ptr queuePriorities = std::make_shared(sortedStates); performPrioritizedStateElimination(queuePriorities, transitionMatrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); } STORM_LOG_DEBUG("Eliminated " << subsystem.size() << " states." << std::endl); @@ -944,7 +854,7 @@ namespace storm { // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions); - + storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); boost::optional> distanceBasedPriorities; if (eliminationOrderNeedsDistances(order)) { @@ -961,7 +871,7 @@ namespace storm { } else if (storm::settings::getModule().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { maximalDepth = performHybridStateElimination(transitionMatrix, flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities); } - + STORM_LOG_ASSERT(flexibleMatrix.empty(), "Not all transitions were eliminated."); STORM_LOG_ASSERT(flexibleBackwardTransitions.empty(), "Not all transitions were eliminated."); @@ -1000,11 +910,11 @@ namespace storm { } } - std::shared_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs); + std::shared_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs); STORM_LOG_TRACE("Eliminating " << statePriorities->size() << " trivial SCCs."); performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated all trivial SCCs."); - + // And then recursively treat the remaining sub-SCCs. STORM_LOG_TRACE("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << "."); for (auto sccIndex : remainingSccs) { @@ -1030,7 +940,7 @@ namespace storm { } else { // In this case, we perform simple state elimination in the current SCC. STORM_LOG_TRACE("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly."); - std::shared_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates); + std::shared_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates); performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated all states of SCC."); } @@ -1038,7 +948,7 @@ namespace storm { // Finally, eliminate the entry states (if we are required to do so). if (eliminateEntryStates) { STORM_LOG_TRACE("Finally, eliminating entry states."); - std::shared_ptr> naivePriorities = createNaivePriorityQueue(entryStates); + std::shared_ptr naivePriorities = createNaivePriorityQueue(entryStates); performPrioritizedStateElimination(naivePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated/added entry states."); } else { @@ -1098,120 +1008,6 @@ namespace storm { } } - template - uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { - uint_fast64_t penalty = 0; - bool hasParametricSelfLoop = false; - - for (auto const& predecessor : backwardTransitions.getRow(state)) { - for (auto const& successor : transitionMatrix.getRow(state)) { - penalty += estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue()); -// STORM_LOG_TRACE("1) penalty += " << (estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue())) << " because of " << predecessor.getValue() << " and " << successor.getValue() << "."); - } - if (predecessor.getColumn() == state) { - hasParametricSelfLoop = !storm::utility::isConstant(predecessor.getValue()); - } - penalty += estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state]); -// STORM_LOG_TRACE("2) penalty += " << (estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state])) << " because of " << oneStepProbabilities[predecessor.getColumn()] << ", " << predecessor.getValue() << " and " << oneStepProbabilities[state] << "."); - } - - // If it is a self-loop that is parametric, we increase the penalty a lot. - if (hasParametricSelfLoop) { - penalty *= 10; -// STORM_LOG_TRACE("3) penalty *= 100, because of parametric self-loop."); - } - -// STORM_LOG_TRACE("New penalty of state " << state << " is " << penalty << "."); - return penalty; - } - - template - uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { - return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size(); - } - - template - void StatePriorityQueue::update(storm::storage::sparse::state_type, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { - // Intentionally left empty. - } - - template - SparseDtmcEliminationModelChecker::StaticStatePriorityQueue::StaticStatePriorityQueue(std::vector const& sortedStates) : StatePriorityQueue(), sortedStates(sortedStates), currentPosition(0) { - // Intentionally left empty. - } - - template - bool SparseDtmcEliminationModelChecker::StaticStatePriorityQueue::hasNextState() const { - return currentPosition < sortedStates.size(); - } - - template - storm::storage::sparse::state_type SparseDtmcEliminationModelChecker::StaticStatePriorityQueue::popNextState() { - ++currentPosition; - return sortedStates[currentPosition - 1]; - } - - template - std::size_t SparseDtmcEliminationModelChecker::StaticStatePriorityQueue::size() const { - return sortedStates.size() - currentPosition; - } - - template - SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::DynamicPenaltyStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, PenaltyFunctionType const& penaltyFunction) : StatePriorityQueue(), priorityQueue(), stateToPriorityMapping(), penaltyFunction(penaltyFunction) { - // Insert all state-penalty pairs into our priority queue. - for (auto const& statePenalty : sortedStatePenaltyPairs) { - priorityQueue.insert(priorityQueue.end(), statePenalty); - } - - // Insert all state-penalty pairs into auxiliary mapping. - for (auto const& statePenalty : sortedStatePenaltyPairs) { - stateToPriorityMapping.emplace(statePenalty); - } - } - - template - bool SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::hasNextState() const { - return !priorityQueue.empty(); - } - - template - storm::storage::sparse::state_type SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::popNextState() { - auto it = priorityQueue.begin(); - STORM_LOG_TRACE("Popping state " << it->first << " with priority " << it->second << "."); - storm::storage::sparse::state_type result = it->first; - priorityQueue.erase(priorityQueue.begin()); - return result; - } - - template - void SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { - // First, we need to find the priority until now. - auto priorityIt = stateToPriorityMapping.find(state); - - // If the priority queue does not store the priority of the given state, we must not update it. - if (priorityIt == stateToPriorityMapping.end()) { - return; - } - uint_fast64_t lastPriority = priorityIt->second; - - uint_fast64_t newPriority = penaltyFunction(state, transitionMatrix, backwardTransitions, oneStepProbabilities); - - if (lastPriority != newPriority) { - // Erase and re-insert into the priority queue with the new priority. - auto queueIt = priorityQueue.find(std::make_pair(state, lastPriority)); - priorityQueue.erase(queueIt); - priorityQueue.emplace(state, newPriority); - - // Finally, update the probability in the mapping. - priorityIt->second = newPriority; - } - } - - template - std::size_t SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::size() const { - return priorityQueue.size(); - } - template bool SparseDtmcEliminationModelChecker::checkConsistent(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions) { for (uint_fast64_t forwardIndex = 0; forwardIndex < transitionMatrix.getRowCount(); ++forwardIndex) { @@ -1235,13 +1031,9 @@ namespace storm { return true; } - template class StatePriorityQueue; template class SparseDtmcEliminationModelChecker>; - template uint_fast64_t estimateComplexity(double const& value); - - + #ifdef STORM_HAVE_CARL - template class StatePriorityQueue; template class SparseDtmcEliminationModelChecker>; #endif } // namespace modelchecker diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 7359ac93f..73f419425 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -1,26 +1,18 @@ #ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_ #define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_ +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" + +#include "src/models/sparse/Dtmc.h" + #include "src/storage/sparse/StateType.h" #include "src/storage/FlexibleSparseMatrix.h" -#include "src/models/sparse/Dtmc.h" -#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "src/utility/constants.h" +#include "src/solver/stateelimination/StatePriorityQueue.h" namespace storm { namespace modelchecker { - template - uint_fast64_t estimateComplexity(ValueType const& value); - - template - class StatePriorityQueue { - public: - virtual bool hasNextState() const = 0; - virtual storm::storage::sparse::state_type popNextState() = 0; - virtual void update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); - virtual std::size_t size() const = 0; - }; + using namespace storm::solver::stateelimination; template class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker { @@ -52,54 +44,13 @@ namespace storm { static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, bool computeForInitialStatesOnly); private: - - class StaticStatePriorityQueue : public StatePriorityQueue { - public: - StaticStatePriorityQueue(std::vector const& sortedStates); - - virtual bool hasNextState() const override; - virtual storm::storage::sparse::state_type popNextState() override; - virtual std::size_t size() const override; - - private: - std::vector sortedStates; - uint_fast64_t currentPosition; - }; - - struct PriorityComparator { - bool operator()(std::pair const& first, std::pair const& second) { - return (first.second < second.second) || (first.second == second.second && first.first < second.first) ; - } - }; - - typedef std::function const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities)> PenaltyFunctionType; - - class DynamicPenaltyStatePriorityQueue : public StatePriorityQueue { - public: - DynamicPenaltyStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, PenaltyFunctionType const& penaltyFunction); - - virtual bool hasNextState() const override; - virtual storm::storage::sparse::state_type popNextState() override; - virtual void update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) override; - virtual std::size_t size() const override; - - private: - std::set, PriorityComparator> priorityQueue; - std::unordered_map stateToPriorityMapping; - PenaltyFunctionType penaltyFunction; - }; - static std::vector computeLongRunValues(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, bool computeResultsForInitialStatesOnly, std::vector& stateValues); static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly); static std::vector computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& oneStepProbabilitiesToTarget); - static std::shared_ptr> createStatePriorityQueue(boost::optional> const& stateDistances, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); - - static std::shared_ptr> createNaivePriorityQueue(storm::storage::BitVector const& states); - - static void performPrioritizedStateElimination(std::shared_ptr>& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly); + static void performPrioritizedStateElimination(std::shared_ptr& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly); static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional>& additionalStateValues, boost::optional> const& distanceBasedPriorities); @@ -112,11 +63,7 @@ namespace storm { static std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); 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, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); - - static uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); - + static bool checkConsistent(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions); }; diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index b3b416cfc..b9739203f 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -5,7 +5,7 @@ #include "src/adapters/CarlAdapter.h" #include "src/storage/FlexibleSparseMatrix.h" #include "src/models/sparse/Dtmc.h" -#include "src/solver/stateelimination/MAEliminator.h" +#include "src/solver/stateelimination/StateEliminator.h" #include "src/utility/vector.h" namespace storm { @@ -273,7 +273,7 @@ namespace storm { // Initialize storm::storage::FlexibleSparseMatrix flexibleMatrix(this->getTransitionMatrix()); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(this->getTransitionMatrix().transpose()); - storm::solver::stateelimination::MAEliminator> stateEliminator(flexibleMatrix, flexibleBackwardTransitions); + storm::solver::stateelimination::StateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions); for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { assert(!this->isHybridState(state)); diff --git a/src/solver/stateelimination/ConditionalEliminator.cpp b/src/solver/stateelimination/ConditionalEliminator.cpp index f1e1c5df6..c45a31cb7 100644 --- a/src/solver/stateelimination/ConditionalEliminator.cpp +++ b/src/solver/stateelimination/ConditionalEliminator.cpp @@ -1,35 +1,38 @@ #include "src/solver/stateelimination/ConditionalEliminator.h" +#include "src/utility/macros.h" +#include "src/utility/constants.h" + namespace storm { namespace solver { namespace stateelimination { - template - ConditionalEliminator::ConditionalEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector& phiStates, storm::storage::BitVector& psiStates) : StateEliminator(transitionMatrix, backwardTransitions), oneStepProbabilities(oneStepProbabilities), phiStates(phiStates), psiStates(psiStates), specificState(NONE) { + template + ConditionalEliminator::ConditionalEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector& phiStates, storm::storage::BitVector& psiStates) : StateEliminator(transitionMatrix, backwardTransitions), oneStepProbabilities(oneStepProbabilities), phiStates(phiStates), psiStates(psiStates), filterLabel(StateLabel::NONE) { } - template - void ConditionalEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { + template + void ConditionalEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { oneStepProbabilities[state] = storm::utility::simplify(loopProbability * oneStepProbabilities[state]); } - template - void ConditionalEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { + template + void ConditionalEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { oneStepProbabilities[predecessor] = storm::utility::simplify(oneStepProbabilities[predecessor] * storm::utility::simplify(probability * oneStepProbabilities[state])); } - template - void ConditionalEliminator::updatePriority(storm::storage::sparse::state_type const& state) { + template + void ConditionalEliminator::updatePriority(storm::storage::sparse::state_type const& state) { // Do nothing } - template - bool ConditionalEliminator::filterPredecessor(storm::storage::sparse::state_type const& state) { + template + bool ConditionalEliminator::filterPredecessor(storm::storage::sparse::state_type const& state) { // TODO find better solution than flag - switch (specificState) { - case PHI: + switch (filterLabel) { + case StateLabel::PHI: return phiStates.get(state); - case PSI: + case StateLabel::PSI: return psiStates.get(state); default: STORM_LOG_ASSERT(false, "Specific state not set."); @@ -37,16 +40,35 @@ namespace storm { } } - template - bool ConditionalEliminator::isFilterPredecessor() const { + template + bool ConditionalEliminator::isFilterPredecessor() const { return true; } + template + void ConditionalEliminator::setFilterPhi() { + filterLabel = StateLabel::PHI; + } + + template + void ConditionalEliminator::setFilterPsi() { + filterLabel = StateLabel::PSI; + } + + template + void ConditionalEliminator::setFilter(StateLabel const& stateLabel) { + filterLabel = stateLabel; + } + + template + void ConditionalEliminator::unsetFilter() { + filterLabel = StateLabel::NONE; + } - template class ConditionalEliminator>; + template class ConditionalEliminator; #ifdef STORM_HAVE_CARL - template class ConditionalEliminator>; + template class ConditionalEliminator; #endif } // namespace stateelimination diff --git a/src/solver/stateelimination/ConditionalEliminator.h b/src/solver/stateelimination/ConditionalEliminator.h index b98066d3f..ead6afeec 100644 --- a/src/solver/stateelimination/ConditionalEliminator.h +++ b/src/solver/stateelimination/ConditionalEliminator.h @@ -9,14 +9,11 @@ namespace storm { namespace solver { namespace stateelimination { - template - class ConditionalEliminator : public StateEliminator { - - typedef typename SparseModelType::ValueType ValueType; - - enum SpecificState { NONE, PHI, PSI}; - + template + class ConditionalEliminator : public StateEliminator { public: + enum class StateLabel { NONE, PHI, PSI }; + ConditionalEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector& phiStates, storm::storage::BitVector& psiStates); // Instantiaton of Virtual methods @@ -26,24 +23,16 @@ namespace storm { bool filterPredecessor(storm::storage::sparse::state_type const& state) override; bool isFilterPredecessor() const override; - void setStatePsi() { - specificState = PSI; - } - - void setStatePhi() { - specificState = PHI; - } - - void clearState() { - specificState = NONE; - } + void setFilterPhi(); + void setFilterPsi(); + void setFilter(StateLabel const& stateLabel); + void unsetFilter(); private: std::vector& oneStepProbabilities; storm::storage::BitVector& phiStates; storm::storage::BitVector& psiStates; - SpecificState specificState; - + StateLabel filterLabel; }; } // namespace stateelimination diff --git a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp new file mode 100644 index 000000000..8c4d0a83d --- /dev/null +++ b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp @@ -0,0 +1,75 @@ +#include "src/solver/stateelimination/DynamicStatePriorityQueue.h" + +#include "src/adapters/CarlAdapter.h" + +#include "src/utility/macros.h" +#include "src/utility/constants.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + DynamicStatePriorityQueue::DynamicStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, PenaltyFunctionType const& penaltyFunction) : StatePriorityQueue(), transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions), oneStepProbabilities(oneStepProbabilities), priorityQueue(), stateToPriorityMapping(), penaltyFunction(penaltyFunction) { + // Insert all state-penalty pairs into our priority queue. + for (auto const& statePenalty : sortedStatePenaltyPairs) { + priorityQueue.insert(priorityQueue.end(), statePenalty); + } + + // Insert all state-penalty pairs into auxiliary mapping. + for (auto const& statePenalty : sortedStatePenaltyPairs) { + stateToPriorityMapping.emplace(statePenalty); + } + } + + template + bool DynamicStatePriorityQueue::hasNext() const { + return !priorityQueue.empty(); + } + + template + storm::storage::sparse::state_type DynamicStatePriorityQueue::pop() { + auto it = priorityQueue.begin(); + STORM_LOG_TRACE("Popping state " << it->first << " with priority " << it->second << "."); + storm::storage::sparse::state_type result = it->first; + priorityQueue.erase(priorityQueue.begin()); + return result; + } + + template + void DynamicStatePriorityQueue::update(storm::storage::sparse::state_type state) { + // First, we need to find the priority until now. + auto priorityIt = stateToPriorityMapping.find(state); + + // If the priority queue does not store the priority of the given state, we must not update it. + if (priorityIt == stateToPriorityMapping.end()) { + return; + } + uint_fast64_t lastPriority = priorityIt->second; + + uint_fast64_t newPriority = penaltyFunction(state, transitionMatrix, backwardTransitions, oneStepProbabilities); + + if (lastPriority != newPriority) { + // Erase and re-insert into the priority queue with the new priority. + auto queueIt = priorityQueue.find(std::make_pair(state, lastPriority)); + priorityQueue.erase(queueIt); + priorityQueue.emplace(state, newPriority); + + // Finally, update the probability in the mapping. + priorityIt->second = newPriority; + } + } + + template + std::size_t DynamicStatePriorityQueue::size() const { + return priorityQueue.size(); + } + + template class DynamicStatePriorityQueue; + +#ifdef STORM_HAVE_CARL + template class DynamicStatePriorityQueue; +#endif + } + } +} diff --git a/src/solver/stateelimination/DynamicStatePriorityQueue.h b/src/solver/stateelimination/DynamicStatePriorityQueue.h new file mode 100644 index 000000000..b5675440b --- /dev/null +++ b/src/solver/stateelimination/DynamicStatePriorityQueue.h @@ -0,0 +1,48 @@ +#pragma once + +#include +#include +#include +#include + +#include "src/solver/stateelimination/StatePriorityQueue.h" + +namespace storm { + namespace storage { + template + class FlexibleSparseMatrix; + } + + namespace solver { + namespace stateelimination { + + struct PriorityComparator { + bool operator()(std::pair const& first, std::pair const& second) { + return (first.second < second.second) || (first.second == second.second && first.first < second.first) ; + } + }; + + template + class DynamicStatePriorityQueue : public StatePriorityQueue { + public: + typedef std::function const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities)> PenaltyFunctionType; + + DynamicStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, PenaltyFunctionType const& penaltyFunction); + + virtual bool hasNext() const override; + virtual storm::storage::sparse::state_type pop() override; + virtual void update(storm::storage::sparse::state_type state) override; + virtual std::size_t size() const override; + + private: + storm::storage::FlexibleSparseMatrix const& transitionMatrix; + storm::storage::FlexibleSparseMatrix const& backwardTransitions; + std::vector const& oneStepProbabilities; + std::set, PriorityComparator> priorityQueue; + std::unordered_map stateToPriorityMapping; + PenaltyFunctionType penaltyFunction; + }; + + } + } +} \ No newline at end of file diff --git a/src/solver/stateelimination/LongRunAverageEliminator.cpp b/src/solver/stateelimination/LongRunAverageEliminator.cpp index 1757b87fa..c06fed5bb 100644 --- a/src/solver/stateelimination/LongRunAverageEliminator.cpp +++ b/src/solver/stateelimination/LongRunAverageEliminator.cpp @@ -1,46 +1,31 @@ #include "src/solver/stateelimination/LongRunAverageEliminator.h" +#include "src/utility/constants.h" + namespace storm { namespace solver { namespace stateelimination { - template - LongRunAverageEliminator::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues, std::vector& averageTimeInStates) : StateEliminator(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues), averageTimeInStates(averageTimeInStates) { + template + LongRunAverageEliminator::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues, std::vector& averageTimeInStates) : PrioritizedStateEliminator(transitionMatrix, backwardTransitions, priorityQueue, stateValues), averageTimeInStates(averageTimeInStates) { } - template - void LongRunAverageEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { - stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]); + template + void LongRunAverageEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { + this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]); averageTimeInStates[state] = storm::utility::simplify(loopProbability * averageTimeInStates[state]); } - template - void LongRunAverageEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { - stateValues[predecessor] = storm::utility::simplify(stateValues[predecessor] + storm::utility::simplify(probability * stateValues[state])); + template + void LongRunAverageEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { + this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state])); averageTimeInStates[predecessor] = storm::utility::simplify(averageTimeInStates[predecessor] + storm::utility::simplify(probability * averageTimeInStates[state])); } - template - void LongRunAverageEliminator::updatePriority(storm::storage::sparse::state_type const& state) { - priorityQueue->update(state, StateEliminator::transitionMatrix, StateEliminator::backwardTransitions, stateValues); - } - - template - bool LongRunAverageEliminator::filterPredecessor(storm::storage::sparse::state_type const& state) { - STORM_LOG_ASSERT(false, "Filter should not be applied."); - return false; - } - - template - bool LongRunAverageEliminator::isFilterPredecessor() const { - return false; - } - - - template class LongRunAverageEliminator>; + template class LongRunAverageEliminator; #ifdef STORM_HAVE_CARL - template class LongRunAverageEliminator>; + template class LongRunAverageEliminator; #endif } // namespace stateelimination diff --git a/src/solver/stateelimination/LongRunAverageEliminator.h b/src/solver/stateelimination/LongRunAverageEliminator.h index f9b1e9cce..d56e53e98 100644 --- a/src/solver/stateelimination/LongRunAverageEliminator.h +++ b/src/solver/stateelimination/LongRunAverageEliminator.h @@ -1,32 +1,26 @@ #ifndef STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_ #define STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_ -#include "src/solver/stateelimination/StateEliminator.h" +#include "src/solver/stateelimination/PrioritizedStateEliminator.h" namespace storm { namespace solver { namespace stateelimination { - template - class LongRunAverageEliminator : public StateEliminator { - - typedef typename SparseModelType::ValueType ValueType; - typedef typename std::shared_ptr> PriorityQueuePointer; + class StatePriorityQueue; + template + class LongRunAverageEliminator : public PrioritizedStateEliminator { public: + typedef typename std::shared_ptr PriorityQueuePointer; + LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues, std::vector& averageTimeInStates); - // Instantiaton of Virtual methods + // Instantiaton of virtual methods. void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override; void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override; - void updatePriority(storm::storage::sparse::state_type const& state) override; - bool filterPredecessor(storm::storage::sparse::state_type const& state) override; - bool isFilterPredecessor() const override; private: - - PriorityQueuePointer priorityQueue; - std::vector& stateValues; std::vector& averageTimeInStates; }; diff --git a/src/solver/stateelimination/MAEliminator.cpp b/src/solver/stateelimination/MAEliminator.cpp deleted file mode 100644 index 911364ac7..000000000 --- a/src/solver/stateelimination/MAEliminator.cpp +++ /dev/null @@ -1,46 +0,0 @@ -#include "src/solver/stateelimination/MAEliminator.h" - -namespace storm { - namespace solver { - namespace stateelimination { - - template - MAEliminator::MAEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions) : StateEliminator(transitionMatrix, backwardTransitions){ - } - - template - void MAEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { - // Do nothing - } - - template - void MAEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { - // Do nothing - } - - template - void MAEliminator::updatePriority(storm::storage::sparse::state_type const& state) { - // Do nothing - } - - template - bool MAEliminator::filterPredecessor(storm::storage::sparse::state_type const& state) { - STORM_LOG_ASSERT(false, "Filter should not be applied."); - return false; - } - - template - bool MAEliminator::isFilterPredecessor() const { - return false; - } - - - template class MAEliminator>; - -#ifdef STORM_HAVE_CARL - template class MAEliminator>; -#endif - - } // namespace stateelimination - } // namespace storage -} // namespace storm diff --git a/src/solver/stateelimination/MAEliminator.h b/src/solver/stateelimination/MAEliminator.h deleted file mode 100644 index d4db284c3..000000000 --- a/src/solver/stateelimination/MAEliminator.h +++ /dev/null @@ -1,32 +0,0 @@ -#ifndef STORM_SOLVER_STATEELIMINATION_MAELIMINATOR_H_ -#define STORM_SOLVER_STATEELIMINATION_MAELIMINATOR_H_ - -#include "src/solver/stateelimination/StateEliminator.h" - -namespace storm { - namespace solver { - namespace stateelimination { - - template - class MAEliminator : public StateEliminator { - - typedef typename SparseModelType::ValueType ValueType; - - public: - MAEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions); - - // Instantiaton of Virtual methods - void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override; - void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override; - void updatePriority(storm::storage::sparse::state_type const& state) override; - bool filterPredecessor(storm::storage::sparse::state_type const& state) override; - bool isFilterPredecessor() const override; - - private: - }; - - } // namespace stateelimination - } // namespace storage -} // namespace storm - -#endif // STORM_SOLVER_STATEELIMINATION_MAELIMINATOR_H_ diff --git a/src/solver/stateelimination/PrioritizedEliminator.cpp b/src/solver/stateelimination/PrioritizedEliminator.cpp deleted file mode 100644 index 17a9c0825..000000000 --- a/src/solver/stateelimination/PrioritizedEliminator.cpp +++ /dev/null @@ -1,46 +0,0 @@ -#include "src/solver/stateelimination/PrioritizedEliminator.h" - -namespace storm { - namespace solver { - namespace stateelimination { - - template - PrioritizedEliminator::PrioritizedEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues) : StateEliminator(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) { - } - - template - void PrioritizedEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { - stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]); - } - - template - void PrioritizedEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { - stateValues[predecessor] = storm::utility::simplify(stateValues[predecessor] + storm::utility::simplify(probability * stateValues[state])); - } - - template - void PrioritizedEliminator::updatePriority(storm::storage::sparse::state_type const& state) { - priorityQueue->update(state, StateEliminator::transitionMatrix, StateEliminator::backwardTransitions, stateValues); - } - - template - bool PrioritizedEliminator::filterPredecessor(storm::storage::sparse::state_type const& state) { - STORM_LOG_ASSERT(false, "Filter should not be applied."); - return false; - } - - template - bool PrioritizedEliminator::isFilterPredecessor() const { - return false; - } - - - template class PrioritizedEliminator>; - -#ifdef STORM_HAVE_CARL - template class PrioritizedEliminator>; -#endif - - } // namespace stateelimination - } // namespace storage -} // namespace storm diff --git a/src/solver/stateelimination/PrioritizedEliminator.h b/src/solver/stateelimination/PrioritizedEliminator.h deleted file mode 100644 index 1180fad09..000000000 --- a/src/solver/stateelimination/PrioritizedEliminator.h +++ /dev/null @@ -1,35 +0,0 @@ -#ifndef STORM_SOLVER_STATEELIMINATION_PRIORITIZEDELIMINATOR_H_ -#define STORM_SOLVER_STATEELIMINATION_PRIORITIZEDELIMINATOR_H_ - -#include "src/solver/stateelimination/StateEliminator.h" - -namespace storm { - namespace solver { - namespace stateelimination { - - template - class PrioritizedEliminator : public StateEliminator { - - typedef typename SparseModelType::ValueType ValueType; - typedef typename std::shared_ptr> PriorityQueuePointer; - - public: - PrioritizedEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues); - - // Instantiaton of Virtual methods - void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override; - void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override; - void updatePriority(storm::storage::sparse::state_type const& state) override; - bool filterPredecessor(storm::storage::sparse::state_type const& state) override; - bool isFilterPredecessor() const override; - - private: - PriorityQueuePointer priorityQueue; - std::vector& stateValues; - }; - - } // namespace stateelimination - } // namespace storage -} // namespace storm - -#endif // STORM_SOLVER_STATEELIMINATION_PRIORITIZEDELIMINATOR_H_ diff --git a/src/solver/stateelimination/PrioritizedStateEliminator.cpp b/src/solver/stateelimination/PrioritizedStateEliminator.cpp new file mode 100644 index 000000000..b5915b659 --- /dev/null +++ b/src/solver/stateelimination/PrioritizedStateEliminator.cpp @@ -0,0 +1,39 @@ +#include "src/solver/stateelimination/PrioritizedStateEliminator.h" + +#include "src/solver/stateelimination/StatePriorityQueue.h" + +#include "src/utility/macros.h" +#include "src/utility/constants.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + PrioritizedStateEliminator::PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues) : StateEliminator(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) { + } + + template + void PrioritizedStateEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { + stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]); + } + + template + void PrioritizedStateEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { + stateValues[predecessor] = storm::utility::simplify(stateValues[predecessor] + storm::utility::simplify(probability * stateValues[state])); + } + + template + void PrioritizedStateEliminator::updatePriority(storm::storage::sparse::state_type const& state) { + priorityQueue->update(state); + } + + template class PrioritizedStateEliminator; + +#ifdef STORM_HAVE_CARL + template class PrioritizedStateEliminator; +#endif + + } // namespace stateelimination + } // namespace storage +} // namespace storm diff --git a/src/solver/stateelimination/PrioritizedStateEliminator.h b/src/solver/stateelimination/PrioritizedStateEliminator.h new file mode 100644 index 000000000..b31c58932 --- /dev/null +++ b/src/solver/stateelimination/PrioritizedStateEliminator.h @@ -0,0 +1,33 @@ +#ifndef STORM_SOLVER_STATEELIMINATION_PRIORITIZEDSTATEELIMINATOR_H_ +#define STORM_SOLVER_STATEELIMINATION_PRIORITIZEDSTATEELIMINATOR_H_ + +#include "src/solver/stateelimination/StateEliminator.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + class StatePriorityQueue; + + template + class PrioritizedStateEliminator : public StateEliminator { + public: + typedef typename std::shared_ptr PriorityQueuePointer; + + PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues); + + // Instantiaton of virtual methods. + void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override; + void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override; + void updatePriority(storm::storage::sparse::state_type const& state) override; + + protected: + PriorityQueuePointer priorityQueue; + std::vector& stateValues; + }; + + } // namespace stateelimination + } // namespace storage +} // namespace storm + +#endif // STORM_SOLVER_STATEELIMINATION_PRIORITIZEDSTATEELIMINATOR_H_ diff --git a/src/solver/stateelimination/StateEliminator.cpp b/src/solver/stateelimination/StateEliminator.cpp index 01dc8a5af..eebe90bbc 100644 --- a/src/solver/stateelimination/StateEliminator.cpp +++ b/src/solver/stateelimination/StateEliminator.cpp @@ -1,6 +1,11 @@ #include "src/solver/stateelimination/StateEliminator.h" +#include "src/adapters/CarlAdapter.h" + #include "src/storage/BitVector.h" + +#include "src/utility/stateelimination.h" +#include "src/utility/macros.h" #include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidStateException.h" @@ -9,13 +14,15 @@ namespace storm { namespace solver { namespace stateelimination { - template - StateEliminator::StateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions) : transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions) { + using namespace storm::utility::stateelimination; + + template + StateEliminator::StateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions) : transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions) { + // Intentionally left empty. } - template - void StateEliminator::eliminateState(storm::storage::sparse::state_type state, bool removeForwardTransitions, storm::storage::BitVector predecessorConstraint) { - + template + void StateEliminator::eliminateState(storm::storage::sparse::state_type state, bool removeForwardTransitions, storm::storage::BitVector predecessorConstraint) { STORM_LOG_TRACE("Eliminating state " << state << "."); // Start by finding loop probability. @@ -124,7 +131,6 @@ namespace storm { auto successorEntry = storm::utility::simplify(std::move(*first2 * multiplyFactor)); *result = successorEntry; newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, successorEntry.getValue()); - // std::cout << "(1) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; ++first2; ++successorOffsetInNewBackwardTransitions; } else if (first1->getColumn() < first2->getColumn()) { @@ -134,7 +140,6 @@ namespace storm { auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue())); *result = storm::storage::MatrixEntry::index_type, typename storm::storage::FlexibleSparseMatrix::value_type>(first1->getColumn(), probability); newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability); - // std::cout << "(2) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; ++first1; ++first2; ++successorOffsetInNewBackwardTransitions; @@ -145,7 +150,6 @@ namespace storm { auto stateProbability = storm::utility::simplify(std::move(*first2 * multiplyFactor)); *result = stateProbability; newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, stateProbability.getValue()); - // std::cout << "(3) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; ++successorOffsetInNewBackwardTransitions; } } @@ -168,10 +172,6 @@ namespace storm { } FlexibleRowType& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn()); - // std::cout << "old backward trans of " << successorEntry.getColumn() << std::endl; - // for (auto const& trans : successorBackwardTransitions) { - // std::cout << trans << std::endl; - // } // Delete the current state as a predecessor of the successor state only if we are going to remove the // current state's forward transitions. @@ -186,11 +186,6 @@ namespace storm { FlexibleRowIterator first2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].begin(); FlexibleRowIterator last2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].end(); - // std::cout << "adding backward trans " << successorEntry.getColumn() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; - // for (auto const& trans : newBackwardProbabilities[successorOffsetInNewBackwardTransitions]) { - // std::cout << trans << std::endl; - // } - FlexibleRowType newPredecessors; newPredecessors.reserve((last1 - first1) + (last2 - first2)); std::insert_iterator result(newPredecessors, newPredecessors.end()); @@ -206,7 +201,7 @@ namespace storm { } ++first2; } else if (first1->getColumn() == first2->getColumn()) { - if (storm::modelchecker::estimateComplexity(first1->getValue()) > storm::modelchecker::estimateComplexity(first2->getValue())) { + if (estimateComplexity(first1->getValue()) > estimateComplexity(first2->getValue())) { *result = *first1; } else { *result = *first2; @@ -225,10 +220,6 @@ namespace storm { } // Now move the new predecessors in place. successorBackwardTransitions = std::move(newPredecessors); - // std::cout << "new backward trans of " << successorEntry.getColumn() << std::endl; - // for (auto const& trans : successorBackwardTransitions) { - // std::cout << trans << std::endl; - // } ++successorOffsetInNewBackwardTransitions; } STORM_LOG_TRACE("Fixed predecessor lists of successor states."); @@ -244,13 +235,38 @@ namespace storm { currentStatePredecessors.clear(); currentStatePredecessors.shrink_to_fit(); } - } - template class StateEliminator>; + template + void StateEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { + // Intentionally left empty. + } + + template + void StateEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { + // Intentionally left empty. + } + + template + void StateEliminator::updatePriority(storm::storage::sparse::state_type const& state) { + // Intentionally left empty. + } + + template + bool StateEliminator::filterPredecessor(storm::storage::sparse::state_type const& state) { + STORM_LOG_ASSERT(false, "Must not filter predecessors."); + return false; + } + + template + bool StateEliminator::isFilterPredecessor() const { + return false; + } + + template class StateEliminator; #ifdef STORM_HAVE_CARL - template class StateEliminator>; + template class StateEliminator; #endif } // namespace stateelimination diff --git a/src/solver/stateelimination/StateEliminator.h b/src/solver/stateelimination/StateEliminator.h index 35c7b0521..bf2abd695 100644 --- a/src/solver/stateelimination/StateEliminator.h +++ b/src/solver/stateelimination/StateEliminator.h @@ -1,42 +1,35 @@ #ifndef STORM_SOLVER_STATEELIMINATION_STATEELIMINATOR_H_ #define STORM_SOLVER_STATEELIMINATION_STATEELIMINATOR_H_ -#include "src/storage/FlexibleSparseMatrix.h" -#include "src/storage/SparseMatrix.h" #include "src/storage/sparse/StateType.h" -#include "src/models/sparse/Dtmc.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/adapters/CarlAdapter.h" -#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" -#include "src/utility/macros.h" + +#include "src/storage/FlexibleSparseMatrix.h" +#include "src/storage/BitVector.h" namespace storm { namespace solver { namespace stateelimination { - template + template class StateEliminator { - typedef typename SparseModelType::ValueType ValueType; + public: typedef typename storm::storage::FlexibleSparseMatrix::row_type FlexibleRowType; typedef typename FlexibleRowType::iterator FlexibleRowIterator; - public: StateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions); void eliminateState(storm::storage::sparse::state_type state, bool removeForwardTransitions, storm::storage::BitVector predecessorConstraint = storm::storage::BitVector()); - // Virtual methods for base classes to distinguish between different state elimination approaches - virtual void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) = 0; - virtual void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) = 0; - virtual void updatePriority(storm::storage::sparse::state_type const& state) = 0; - virtual bool filterPredecessor(storm::storage::sparse::state_type const& state) = 0; - virtual bool isFilterPredecessor() const = 0; - + // Provide virtual methods that can be customized by subclasses to govern side-effect of the elimination. + virtual void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability); + virtual void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state); + virtual void updatePriority(storm::storage::sparse::state_type const& state); + virtual bool filterPredecessor(storm::storage::sparse::state_type const& state); + virtual bool isFilterPredecessor() const; protected: storm::storage::FlexibleSparseMatrix& transitionMatrix; storm::storage::FlexibleSparseMatrix& backwardTransitions; - }; } // namespace stateelimination diff --git a/src/solver/stateelimination/StatePriorityQueue.cpp b/src/solver/stateelimination/StatePriorityQueue.cpp new file mode 100644 index 000000000..3db9d0db7 --- /dev/null +++ b/src/solver/stateelimination/StatePriorityQueue.cpp @@ -0,0 +1,13 @@ +#include "src/solver/stateelimination/StatePriorityQueue.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + void StatePriorityQueue::update(storm::storage::sparse::state_type state) { + // Intentionally left empty. + } + + } + } +} \ No newline at end of file diff --git a/src/solver/stateelimination/StatePriorityQueue.h b/src/solver/stateelimination/StatePriorityQueue.h new file mode 100644 index 000000000..9f1a9ac44 --- /dev/null +++ b/src/solver/stateelimination/StatePriorityQueue.h @@ -0,0 +1,21 @@ +#pragma once + +#include + +#include "src/storage/sparse/StateType.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + class StatePriorityQueue { + public: + virtual bool hasNext() const = 0; + virtual storm::storage::sparse::state_type pop() = 0; + virtual void update(storm::storage::sparse::state_type state); + virtual std::size_t size() const = 0; + }; + + } + } +} \ No newline at end of file diff --git a/src/solver/stateelimination/StaticStatePriorityQueue.cpp b/src/solver/stateelimination/StaticStatePriorityQueue.cpp new file mode 100644 index 000000000..43efe9dcf --- /dev/null +++ b/src/solver/stateelimination/StaticStatePriorityQueue.cpp @@ -0,0 +1,28 @@ +#include "src/solver/stateelimination/StaticStatePriorityQueue.h" + +#include "src/adapters/CarlAdapter.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + StaticStatePriorityQueue::StaticStatePriorityQueue(std::vector const& sortedStates) : StatePriorityQueue(), sortedStates(sortedStates), currentPosition(0) { + // Intentionally left empty. + } + + bool StaticStatePriorityQueue::hasNext() const { + return currentPosition < sortedStates.size(); + } + + storm::storage::sparse::state_type StaticStatePriorityQueue::pop() { + ++currentPosition; + return sortedStates[currentPosition - 1]; + } + + std::size_t StaticStatePriorityQueue::size() const { + return sortedStates.size() - currentPosition; + } + + } + } +} \ No newline at end of file diff --git a/src/solver/stateelimination/StaticStatePriorityQueue.h b/src/solver/stateelimination/StaticStatePriorityQueue.h new file mode 100644 index 000000000..887c32141 --- /dev/null +++ b/src/solver/stateelimination/StaticStatePriorityQueue.h @@ -0,0 +1,26 @@ +#pragma once + +#include + +#include "src/solver/stateelimination/StatePriorityQueue.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + class StaticStatePriorityQueue : public StatePriorityQueue { + public: + StaticStatePriorityQueue(std::vector const& sortedStates); + + virtual bool hasNext() const override; + virtual storm::storage::sparse::state_type pop() override; + virtual std::size_t size() const override; + + private: + std::vector sortedStates; + uint_fast64_t currentPosition; + }; + + } + } +} \ No newline at end of file diff --git a/src/utility/stateelimination.cpp b/src/utility/stateelimination.cpp new file mode 100644 index 000000000..f71e08a5b --- /dev/null +++ b/src/utility/stateelimination.cpp @@ -0,0 +1,160 @@ +#include "src/utility/stateelimination.h" + +#include + +#include "src/solver/stateelimination/StatePriorityQueue.h" +#include "src/solver/stateelimination/StaticStatePriorityQueue.h" +#include "src/solver/stateelimination/DynamicStatePriorityQueue.h" + +#include "src/storage/BitVector.h" +#include "src/storage/FlexibleSparseMatrix.h" + +#include "src/settings/SettingsManager.h" + +#include "src/utility/macros.h" +#include "src/utility/constants.h" +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidSettingsException.h" + +namespace storm { + namespace utility { + namespace stateelimination { + + bool eliminationOrderNeedsDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { + return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Backward || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed; + } + + bool eliminationOrderNeedsForwardDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { + return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed; + } + + bool eliminationOrderNeedsReversedDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { + return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed; + } + + bool eliminationOrderIsPenaltyBased(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { + return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::StaticPenalty || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::DynamicPenalty || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::RegularExpression; + } + + bool eliminationOrderIsStatic(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { + return eliminationOrderNeedsDistances(order) || order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::StaticPenalty; + } + + template + uint_fast64_t estimateComplexity(ValueType const& value) { + return 1; + } + +#ifdef STORM_HAVE_CARL + template<> + uint_fast64_t estimateComplexity(storm::RationalFunction const& value) { + if (storm::utility::isConstant(value)) { + return 1; + } + if (value.denominator().isConstant()) { + return value.nominator().complexity(); + } else { + return value.denominator().complexity() * value.nominator().complexity(); + } + } +#endif + + template + uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + uint_fast64_t penalty = 0; + bool hasParametricSelfLoop = false; + + for (auto const& predecessor : backwardTransitions.getRow(state)) { + for (auto const& successor : transitionMatrix.getRow(state)) { + penalty += estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue()); + } + if (predecessor.getColumn() == state) { + hasParametricSelfLoop = !storm::utility::isConstant(predecessor.getValue()); + } + penalty += estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state]); + } + + // If it is a self-loop that is parametric, we increase the penalty a lot. + if (hasParametricSelfLoop) { + penalty *= 10; + } + + return penalty; + } + + template + uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size(); + } + + template + std::shared_ptr createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states) { + + STORM_LOG_TRACE("Creating state priority queue for states " << states); + + // Get the settings to customize the priority queue. + storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); + + std::vector sortedStates(states.begin(), states.end()); + + if (order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Random) { + std::random_device randomDevice; + std::mt19937 generator(randomDevice()); + std::shuffle(sortedStates.begin(), sortedStates.end(), generator); + return std::make_unique(sortedStates); + } else { + if (eliminationOrderNeedsDistances(order)) { + STORM_LOG_THROW(static_cast(distanceBasedStatePriorities), storm::exceptions::InvalidStateException, "Unable to build state priority queue without distance-based priorities."); + std::sort(sortedStates.begin(), sortedStates.end(), [&distanceBasedStatePriorities] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distanceBasedStatePriorities.get()[state1] < distanceBasedStatePriorities.get()[state2]; } ); + return std::make_unique(sortedStates); + } else if (eliminationOrderIsPenaltyBased(order)) { + std::vector> statePenalties(sortedStates.size()); + typename DynamicStatePriorityQueue::PenaltyFunctionType penaltyFunction = order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression : computeStatePenalty; + for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) { + statePenalties[index] = std::make_pair(sortedStates[index], penaltyFunction(sortedStates[index], transitionMatrix, backwardTransitions, oneStepProbabilities)); + } + + std::sort(statePenalties.begin(), statePenalties.end(), [] (std::pair const& statePenalty1, std::pair const& statePenalty2) { return statePenalty1.second < statePenalty2.second; } ); + + if (eliminationOrderIsStatic(order)) { + // For the static penalty version, we need to strip the penalties to create the queue. + for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) { + sortedStates[index] = statePenalties[index].first; + } + return std::make_unique(sortedStates); + } else { + // For the dynamic penalty version, we need to give the full state-penalty pairs. + return std::make_unique>(statePenalties, transitionMatrix, backwardTransitions, oneStepProbabilities, penaltyFunction); + } + } + } + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Illegal elimination order selected."); + } + + std::shared_ptr createNaivePriorityQueue(storm::storage::BitVector const& states) { + std::vector sortedStates(states.begin(), states.end()); + return std::make_shared(sortedStates); + } + + template uint_fast64_t estimateComplexity(double const& value); + template std::shared_ptr createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); + template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + + +#ifdef STORM_HAVE_CARL + template uint_fast64_t estimateComplexity(storm::RationalFunction const& value); + template std::shared_ptr createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); + template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); +#endif + } + } +} \ No newline at end of file diff --git a/src/utility/stateelimination.h b/src/utility/stateelimination.h new file mode 100644 index 000000000..8dc3ab600 --- /dev/null +++ b/src/utility/stateelimination.h @@ -0,0 +1,60 @@ +#pragma once + +#include +#include + +#include + +#include "src/storage/sparse/StateType.h" + +#include "src/adapters/CarlAdapter.h" + +#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h" + +namespace storm { + namespace solver { + namespace stateelimination { + class StatePriorityQueue; + } + } + + namespace storage { + class BitVector; + + template + class FlexibleSparseMatrix; + } + + namespace utility { + namespace stateelimination { + + using namespace storm::solver::stateelimination; + + bool eliminationOrderNeedsDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order); + bool eliminationOrderNeedsForwardDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order); + bool eliminationOrderNeedsReversedDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order); + bool eliminationOrderIsPenaltyBased(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order); + bool eliminationOrderIsStatic(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order); + + template + uint_fast64_t estimateComplexity(ValueType const& value); + +#ifdef STORM_HAVE_CARL + template<> + uint_fast64_t estimateComplexity(storm::RationalFunction const& value); +#endif + + template + uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + + template + uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + + template + std::shared_ptr createStatePriorityQueue(boost::optional> const& stateDistances, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); + + std::shared_ptr createNaivePriorityQueue(storm::storage::BitVector const& states); + + } + } +} \ No newline at end of file