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<typename ValueType>
- static std::unique_ptr<Eigen::SparseMatrix<ValueType>> toEigenSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
+ std::unique_ptr<Eigen::SparseMatrix<ValueType>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
// Build a list of triplets and let Eigen care about the insertion.
std::vector<Eigen::Triplet<ValueType>> triplets;
triplets.reserve(matrix.getNonzeroEntryCount());
@@ -20,6 +20,6 @@ namespace storm {
return result;
}
- template std::unique_ptr<Eigen::SparseMatrix<double>> toEigenSparseMatrix(storm::storage::SparseMatrix<double> const& matrix);
+ template std::unique_ptr<Eigen::SparseMatrix<double>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<double> 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<typename ValueType>
- 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<typename SparseDtmcModelType>
SparseDtmcEliminationModelChecker<SparseDtmcModelType>::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc<ValueType> const& model) : SparsePropositionalModelChecker<SparseDtmcModelType>(model) {
@@ -98,7 +58,7 @@ namespace storm {
storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
-
+
storm::storage::SparseMatrix<ValueType> 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<ValueType> 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<ValueType> result(numberOfStates, storm::utility::zero<ValueType>());
-
+
// 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<ValueType> 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<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
if (eliminationOrderNeedsDistances(order)) {
@@ -265,11 +225,11 @@ namespace storm {
std::vector<ValueType> averageTimeInStates(stateValues.size(), storm::utility::one<ValueType>());
// First, we eliminate all states in BSCCs (except for the representative states).
- std::shared_ptr<StatePriorityQueue<ValueType>> priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs);
- storm::solver::stateelimination::LongRunAverageEliminator<SparseDtmcModelType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, stateValues, averageTimeInStates);
+ std::shared_ptr<StatePriorityQueue> priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs);
+ storm::solver::stateelimination::LongRunAverageEliminator<ValueType> 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<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
-
+
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<ValueType> 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<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
-
+
std::vector<ValueType> result = computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet());
-
+
// Construct check result.
std::unique_ptr<CheckResult> checkResult(new ExplicitQuantitativeCheckResult<ValueType>(result));
return checkResult;
}
-
+
template<typename SparseDtmcModelType>
std::vector<typename SparseDtmcModelType::ValueType> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> 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<storm::storage::BitVector, storm::storage::BitVector> 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<ValueType> 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<ValueType> 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<ValueType> submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates);
storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose();
-
+
std::vector<ValueType> subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, phiStates, psiStates, oneStepProbabilities);
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, subresult);
}
-
+
// Construct full result.
storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>());
-
+
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<ValueType> result = computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates,
[&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates);
},
checkTask.isOnlyInitialStatesRelevantSet());
-
+
// Construct check result.
std::unique_ptr<CheckResult> checkResult(new ExplicitQuantitativeCheckResult<ValueType>(result));
return checkResult;
}
-
+
template<typename SparseDtmcModelType>
std::vector<typename SparseDtmcModelType::ValueType> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector<ValueType>& stateRewardValues, bool computeForInitialStatesOnly) {
return computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates,
@@ -570,10 +530,10 @@ namespace storm {
},
computeForInitialStatesOnly);
}
-
+
template<typename SparseDtmcModelType>
std::vector<typename SparseDtmcModelType::ValueType> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> 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<ValueType> 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<ValueType> submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates);
storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose();
// Project the state reward vector to all maybe-states.
std::vector<ValueType> stateRewardValues = totalStateRewardVectorGetter(submatrix.getRowCount(), probabilityMatrix, maybeStates);
-
+
std::vector<ValueType> subresult = computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, trueStates, targetStates, probabilityMatrix.getConstrainedRowSumVector(maybeStates, targetStates));
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, subresult);
}
@@ -711,21 +671,21 @@ namespace storm {
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
if (eliminationOrderNeedsDistances(order)) {
distanceBasedPriorities = getDistanceBasedPriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities,
- eliminationOrderNeedsForwardDistances(order),
- eliminationOrderNeedsReversedDistances(order));
+ eliminationOrderNeedsForwardDistances(order),
+ eliminationOrderNeedsReversedDistances(order));
}
storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(submatrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(submatrixTransposed, true);
- std::shared_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate);
-
+ std::shared_ptr<StatePriorityQueue> 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<SparseDtmcModelType> stateEliminator = storm::solver::stateelimination::ConditionalEliminator<SparseDtmcModelType>(flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, phiStates, psiStates);
+ storm::solver::stateelimination::ConditionalEliminator<ValueType> stateEliminator = storm::solver::stateelimination::ConditionalEliminator<ValueType>(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<typename SparseDtmcModelType>
- std::shared_ptr<StatePriorityQueue<typename SparseDtmcModelType::ValueType>> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType>& 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<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
-
- std::vector<storm::storage::sparse::state_type> 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<StaticStatePriorityQueue>(sortedStates);
- } else {
- if (eliminationOrderNeedsDistances(order)) {
- STORM_LOG_THROW(static_cast<bool>(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<StaticStatePriorityQueue>(sortedStates);
- } else if (eliminationOrderIsPenaltyBased(order)) {
- std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> 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<storm::storage::sparse::state_type, uint_fast64_t> const& statePenalty1, std::pair<storm::storage::sparse::state_type, uint_fast64_t> 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<StaticStatePriorityQueue>(sortedStates);
- } else {
- // For the dynamic penalty version, we need to give the full state-penalty pairs.
- return std::make_unique<DynamicPenaltyStatePriorityQueue>(statePenalties, penaltyFunction);
- }
- }
- }
- STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Illegal elimination order selected.");
- }
-
- template<typename SparseDtmcModelType>
- std::shared_ptr<StatePriorityQueue<typename SparseDtmcModelType::ValueType>> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::createNaivePriorityQueue(storm::storage::BitVector const& states) {
- std::vector<storm::storage::sparse::state_type> sortedStates(states.begin(), states.end());
- return std::shared_ptr<StatePriorityQueue<ValueType>>(new StaticStatePriorityQueue(sortedStates));
- }
-
- template<typename SparseDtmcModelType>
- void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performPrioritizedStateElimination(std::shared_ptr<StatePriorityQueue<ValueType>>& priorityQueue, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) {
+ void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performPrioritizedStateElimination(std::shared_ptr<StatePriorityQueue>& priorityQueue, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) {
- storm::solver::stateelimination::PrioritizedEliminator<SparseDtmcModelType> stateEliminator(transitionMatrix, backwardTransitions, priorityQueue, values);
+ storm::solver::stateelimination::PrioritizedStateEliminator<ValueType> 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<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities) {
- std::shared_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem);
+ std::shared_ptr<StatePriorityQueue> 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<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().isEliminateEntryStatesLastSet()) {
STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step.");
std::vector<storm::storage::sparse::state_type> sortedStates(entryStateQueue.begin(), entryStateQueue.end());
- std::shared_ptr<StatePriorityQueue<ValueType>> queuePriorities = std::shared_ptr<StatePriorityQueue<ValueType>>(new StaticStatePriorityQueue(sortedStates));
+ std::shared_ptr<StatePriorityQueue> queuePriorities = std::make_shared<StaticStatePriorityQueue>(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<ValueType> flexibleMatrix(transitionMatrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardTransitions);
-
+
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
if (eliminationOrderNeedsDistances(order)) {
@@ -961,7 +871,7 @@ namespace storm {
} else if (storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().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<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs);
+ std::shared_ptr<StatePriorityQueue> 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<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates);
+ std::shared_ptr<StatePriorityQueue> 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<StatePriorityQueue<ValueType>> naivePriorities = createNaivePriorityQueue(entryStates);
+ std::shared_ptr<StatePriorityQueue> 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<typename SparseDtmcModelType>
- uint_fast64_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> 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<typename SparseDtmcModelType>
- uint_fast64_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
- return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size();
- }
-
- template<typename ValueType>
- void StatePriorityQueue<ValueType>::update(storm::storage::sparse::state_type, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
- // Intentionally left empty.
- }
-
- template<typename SparseDtmcModelType>
- SparseDtmcEliminationModelChecker<SparseDtmcModelType>::StaticStatePriorityQueue::StaticStatePriorityQueue(std::vector<storm::storage::sparse::state_type> const& sortedStates) : StatePriorityQueue<ValueType>(), sortedStates(sortedStates), currentPosition(0) {
- // Intentionally left empty.
- }
-
- template<typename SparseDtmcModelType>
- bool SparseDtmcEliminationModelChecker<SparseDtmcModelType>::StaticStatePriorityQueue::hasNextState() const {
- return currentPosition < sortedStates.size();
- }
-
- template<typename SparseDtmcModelType>
- storm::storage::sparse::state_type SparseDtmcEliminationModelChecker<SparseDtmcModelType>::StaticStatePriorityQueue::popNextState() {
- ++currentPosition;
- return sortedStates[currentPosition - 1];
- }
-
- template<typename SparseDtmcModelType>
- std::size_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::StaticStatePriorityQueue::size() const {
- return sortedStates.size() - currentPosition;
- }
-
- template<typename SparseDtmcModelType>
- SparseDtmcEliminationModelChecker<SparseDtmcModelType>::DynamicPenaltyStatePriorityQueue::DynamicPenaltyStatePriorityQueue(std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> const& sortedStatePenaltyPairs, PenaltyFunctionType const& penaltyFunction) : StatePriorityQueue<ValueType>(), 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<typename SparseDtmcModelType>
- bool SparseDtmcEliminationModelChecker<SparseDtmcModelType>::DynamicPenaltyStatePriorityQueue::hasNextState() const {
- return !priorityQueue.empty();
- }
-
- template<typename SparseDtmcModelType>
- storm::storage::sparse::state_type SparseDtmcEliminationModelChecker<SparseDtmcModelType>::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<typename SparseDtmcModelType>
- void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::DynamicPenaltyStatePriorityQueue::update(storm::storage::sparse::state_type state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> 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<typename SparseDtmcModelType>
- std::size_t SparseDtmcEliminationModelChecker<SparseDtmcModelType>::DynamicPenaltyStatePriorityQueue::size() const {
- return priorityQueue.size();
- }
-
template<typename SparseDtmcModelType>
bool SparseDtmcEliminationModelChecker<SparseDtmcModelType>::checkConsistent(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions) {
for (uint_fast64_t forwardIndex = 0; forwardIndex < transitionMatrix.getRowCount(); ++forwardIndex) {
@@ -1235,13 +1031,9 @@ namespace storm {
return true;
}
- template class StatePriorityQueue<double>;
template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>>;
- template uint_fast64_t estimateComplexity(double const& value);
-
-
+
#ifdef STORM_HAVE_CARL
- template class StatePriorityQueue<storm::RationalFunction>;
template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>;
#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<typename ValueType>
- uint_fast64_t estimateComplexity(ValueType const& value);
-
- template<typename ValueType>
- 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<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities);
- virtual std::size_t size() const = 0;
- };
+ using namespace storm::solver::stateelimination;
template<typename SparseDtmcModelType>
class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker<SparseDtmcModelType> {
@@ -52,54 +44,13 @@ namespace storm {
static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector<ValueType>& stateRewardValues, bool computeForInitialStatesOnly);
private:
-
- class StaticStatePriorityQueue : public StatePriorityQueue<ValueType> {
- public:
- StaticStatePriorityQueue(std::vector<storm::storage::sparse::state_type> 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<uint_fast64_t> sortedStates;
- uint_fast64_t currentPosition;
- };
-
- struct PriorityComparator {
- bool operator()(std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& first, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& second) {
- return (first.second < second.second) || (first.second == second.second && first.first < second.first) ;
- }
- };
-
- typedef std::function<uint_fast64_t (storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities)> PenaltyFunctionType;
-
- class DynamicPenaltyStatePriorityQueue : public StatePriorityQueue<ValueType> {
- public:
- DynamicPenaltyStatePriorityQueue(std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> 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<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) override;
- virtual std::size_t size() const override;
-
- private:
- std::set<std::pair<storm::storage::sparse::state_type, uint_fast64_t>, PriorityComparator> priorityQueue;
- std::unordered_map<storm::storage::sparse::state_type, uint_fast64_t> stateToPriorityMapping;
- PenaltyFunctionType penaltyFunction;
- };
-
static std::vector<ValueType> computeLongRunValues(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& stateValues);
static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly);
static std::vector<ValueType> computeReachabilityValues(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& values, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& oneStepProbabilitiesToTarget);
- static std::shared_ptr<StatePriorityQueue<ValueType>> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& stateDistances, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& states);
-
- static std::shared_ptr<StatePriorityQueue<ValueType>> createNaivePriorityQueue(storm::storage::BitVector const& states);
-
- static void performPrioritizedStateElimination(std::shared_ptr<StatePriorityQueue<ValueType>>& priorityQueue, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly);
+ static void performPrioritizedStateElimination(std::shared_ptr<StatePriorityQueue>& priorityQueue, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly);
static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<ValueType>>& additionalStateValues, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities);
@@ -112,11 +63,7 @@ namespace storm {
static std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities, bool forward, bool reverse);
static std::vector<std::size_t> getStateDistances(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities, bool forward);
-
- static uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities);
-
- static uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities);
-
+
static bool checkConsistent(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& 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<ValueType> flexibleMatrix(this->getTransitionMatrix());
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(this->getTransitionMatrix().transpose());
- storm::solver::stateelimination::MAEliminator<storm::models::sparse::Dtmc<ValueType>> stateEliminator(flexibleMatrix, flexibleBackwardTransitions);
+ storm::solver::stateelimination::StateEliminator<ValueType> 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<typename SparseModelType>
- ConditionalEliminator<SparseModelType>::ConditionalEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector& phiStates, storm::storage::BitVector& psiStates) : StateEliminator<SparseModelType>(transitionMatrix, backwardTransitions), oneStepProbabilities(oneStepProbabilities), phiStates(phiStates), psiStates(psiStates), specificState(NONE) {
+ template<typename ValueType>
+ ConditionalEliminator<ValueType>::ConditionalEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector& phiStates, storm::storage::BitVector& psiStates) : StateEliminator<ValueType>(transitionMatrix, backwardTransitions), oneStepProbabilities(oneStepProbabilities), phiStates(phiStates), psiStates(psiStates), filterLabel(StateLabel::NONE) {
}
- template<typename SparseModelType>
- void ConditionalEliminator<SparseModelType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
+ template<typename ValueType>
+ void ConditionalEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
oneStepProbabilities[state] = storm::utility::simplify(loopProbability * oneStepProbabilities[state]);
}
- template<typename SparseModelType>
- void ConditionalEliminator<SparseModelType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
+ template<typename ValueType>
+ void ConditionalEliminator<ValueType>::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<typename SparseModelType>
- void ConditionalEliminator<SparseModelType>::updatePriority(storm::storage::sparse::state_type const& state) {
+ template<typename ValueType>
+ void ConditionalEliminator<ValueType>::updatePriority(storm::storage::sparse::state_type const& state) {
// Do nothing
}
- template<typename SparseModelType>
- bool ConditionalEliminator<SparseModelType>::filterPredecessor(storm::storage::sparse::state_type const& state) {
+ template<typename ValueType>
+ bool ConditionalEliminator<ValueType>::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<typename SparseModelType>
- bool ConditionalEliminator<SparseModelType>::isFilterPredecessor() const {
+ template<typename ValueType>
+ bool ConditionalEliminator<ValueType>::isFilterPredecessor() const {
return true;
}
+ template<typename ValueType>
+ void ConditionalEliminator<ValueType>::setFilterPhi() {
+ filterLabel = StateLabel::PHI;
+ }
+
+ template<typename ValueType>
+ void ConditionalEliminator<ValueType>::setFilterPsi() {
+ filterLabel = StateLabel::PSI;
+ }
+
+ template<typename ValueType>
+ void ConditionalEliminator<ValueType>::setFilter(StateLabel const& stateLabel) {
+ filterLabel = stateLabel;
+ }
+
+ template<typename ValueType>
+ void ConditionalEliminator<ValueType>::unsetFilter() {
+ filterLabel = StateLabel::NONE;
+ }
- template class ConditionalEliminator<storm::models::sparse::Dtmc<double>>;
+ template class ConditionalEliminator<double>;
#ifdef STORM_HAVE_CARL
- template class ConditionalEliminator<storm::models::sparse::Dtmc<storm::RationalFunction>>;
+ template class ConditionalEliminator<storm::RationalFunction>;
#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<typename SparseModelType>
- class ConditionalEliminator : public StateEliminator<SparseModelType> {
-
- typedef typename SparseModelType::ValueType ValueType;
-
- enum SpecificState { NONE, PHI, PSI};
-
+ template<typename ValueType>
+ class ConditionalEliminator : public StateEliminator<ValueType> {
public:
+ enum class StateLabel { NONE, PHI, PSI };
+
ConditionalEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& 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<ValueType>& 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<typename ValueType>
+ DynamicStatePriorityQueue<ValueType>::DynamicStatePriorityQueue(std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> const& sortedStatePenaltyPairs, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> 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<typename ValueType>
+ bool DynamicStatePriorityQueue<ValueType>::hasNext() const {
+ return !priorityQueue.empty();
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type DynamicStatePriorityQueue<ValueType>::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<typename ValueType>
+ void DynamicStatePriorityQueue<ValueType>::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<typename ValueType>
+ std::size_t DynamicStatePriorityQueue<ValueType>::size() const {
+ return priorityQueue.size();
+ }
+
+ template class DynamicStatePriorityQueue<double>;
+
+#ifdef STORM_HAVE_CARL
+ template class DynamicStatePriorityQueue<storm::RationalFunction>;
+#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 <functional>
+#include <vector>
+#include <set>
+#include <unordered_map>
+
+#include "src/solver/stateelimination/StatePriorityQueue.h"
+
+namespace storm {
+ namespace storage {
+ template<typename ValueType>
+ class FlexibleSparseMatrix;
+ }
+
+ namespace solver {
+ namespace stateelimination {
+
+ struct PriorityComparator {
+ bool operator()(std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& first, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& second) {
+ return (first.second < second.second) || (first.second == second.second && first.first < second.first) ;
+ }
+ };
+
+ template<typename ValueType>
+ class DynamicStatePriorityQueue : public StatePriorityQueue {
+ public:
+ typedef std::function<uint_fast64_t (storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities)> PenaltyFunctionType;
+
+ DynamicStatePriorityQueue(std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> const& sortedStatePenaltyPairs, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> 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<ValueType> const& transitionMatrix;
+ storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions;
+ std::vector<ValueType> const& oneStepProbabilities;
+ std::set<std::pair<storm::storage::sparse::state_type, uint_fast64_t>, PriorityComparator> priorityQueue;
+ std::unordered_map<storm::storage::sparse::state_type, uint_fast64_t> 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<typename SparseModelType>
- LongRunAverageEliminator<SparseModelType>::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& averageTimeInStates) : StateEliminator<SparseModelType>(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues), averageTimeInStates(averageTimeInStates) {
+ template<typename ValueType>
+ LongRunAverageEliminator<ValueType>::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& averageTimeInStates) : PrioritizedStateEliminator<ValueType>(transitionMatrix, backwardTransitions, priorityQueue, stateValues), averageTimeInStates(averageTimeInStates) {
}
- template<typename SparseModelType>
- void LongRunAverageEliminator<SparseModelType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
- stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]);
+ template<typename ValueType>
+ void LongRunAverageEliminator<ValueType>::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<typename SparseModelType>
- void LongRunAverageEliminator<SparseModelType>::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<typename ValueType>
+ void LongRunAverageEliminator<ValueType>::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<typename SparseModelType>
- void LongRunAverageEliminator<SparseModelType>::updatePriority(storm::storage::sparse::state_type const& state) {
- priorityQueue->update(state, StateEliminator<SparseModelType>::transitionMatrix, StateEliminator<SparseModelType>::backwardTransitions, stateValues);
- }
-
- template<typename SparseModelType>
- bool LongRunAverageEliminator<SparseModelType>::filterPredecessor(storm::storage::sparse::state_type const& state) {
- STORM_LOG_ASSERT(false, "Filter should not be applied.");
- return false;
- }
-
- template<typename SparseModelType>
- bool LongRunAverageEliminator<SparseModelType>::isFilterPredecessor() const {
- return false;
- }
-
-
- template class LongRunAverageEliminator<storm::models::sparse::Dtmc<double>>;
+ template class LongRunAverageEliminator<double>;
#ifdef STORM_HAVE_CARL
- template class LongRunAverageEliminator<storm::models::sparse::Dtmc<storm::RationalFunction>>;
+ template class LongRunAverageEliminator<storm::RationalFunction>;
#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<typename SparseModelType>
- class LongRunAverageEliminator : public StateEliminator<SparseModelType> {
-
- typedef typename SparseModelType::ValueType ValueType;
- typedef typename std::shared_ptr<storm::modelchecker::StatePriorityQueue<ValueType>> PriorityQueuePointer;
+ class StatePriorityQueue;
+ template<typename ValueType>
+ class LongRunAverageEliminator : public PrioritizedStateEliminator<ValueType> {
public:
+ typedef typename std::shared_ptr<StatePriorityQueue> PriorityQueuePointer;
+
LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& 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<ValueType>& stateValues;
std::vector<ValueType>& 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<typename SparseModelType>
- MAEliminator<SparseModelType>::MAEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions) : StateEliminator<SparseModelType>(transitionMatrix, backwardTransitions){
- }
-
- template<typename SparseModelType>
- void MAEliminator<SparseModelType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
- // Do nothing
- }
-
- template<typename SparseModelType>
- void MAEliminator<SparseModelType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
- // Do nothing
- }
-
- template<typename SparseModelType>
- void MAEliminator<SparseModelType>::updatePriority(storm::storage::sparse::state_type const& state) {
- // Do nothing
- }
-
- template<typename SparseModelType>
- bool MAEliminator<SparseModelType>::filterPredecessor(storm::storage::sparse::state_type const& state) {
- STORM_LOG_ASSERT(false, "Filter should not be applied.");
- return false;
- }
-
- template<typename SparseModelType>
- bool MAEliminator<SparseModelType>::isFilterPredecessor() const {
- return false;
- }
-
-
- template class MAEliminator<storm::models::sparse::Dtmc<double>>;
-
-#ifdef STORM_HAVE_CARL
- template class MAEliminator<storm::models::sparse::Dtmc<storm::RationalFunction>>;
-#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<typename SparseModelType>
- class MAEliminator : public StateEliminator<SparseModelType> {
-
- typedef typename SparseModelType::ValueType ValueType;
-
- public:
- MAEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& 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<typename SparseModelType>
- PrioritizedEliminator<SparseModelType>::PrioritizedEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues) : StateEliminator<SparseModelType>(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) {
- }
-
- template<typename SparseModelType>
- void PrioritizedEliminator<SparseModelType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
- stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]);
- }
-
- template<typename SparseModelType>
- void PrioritizedEliminator<SparseModelType>::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<typename SparseModelType>
- void PrioritizedEliminator<SparseModelType>::updatePriority(storm::storage::sparse::state_type const& state) {
- priorityQueue->update(state, StateEliminator<SparseModelType>::transitionMatrix, StateEliminator<SparseModelType>::backwardTransitions, stateValues);
- }
-
- template<typename SparseModelType>
- bool PrioritizedEliminator<SparseModelType>::filterPredecessor(storm::storage::sparse::state_type const& state) {
- STORM_LOG_ASSERT(false, "Filter should not be applied.");
- return false;
- }
-
- template<typename SparseModelType>
- bool PrioritizedEliminator<SparseModelType>::isFilterPredecessor() const {
- return false;
- }
-
-
- template class PrioritizedEliminator<storm::models::sparse::Dtmc<double>>;
-
-#ifdef STORM_HAVE_CARL
- template class PrioritizedEliminator<storm::models::sparse::Dtmc<storm::RationalFunction>>;
-#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<typename SparseModelType>
- class PrioritizedEliminator : public StateEliminator<SparseModelType> {
-
- typedef typename SparseModelType::ValueType ValueType;
- typedef typename std::shared_ptr<storm::modelchecker::StatePriorityQueue<ValueType>> PriorityQueuePointer;
-
- public:
- PrioritizedEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& 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<ValueType>& 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<typename ValueType>
+ PrioritizedStateEliminator<ValueType>::PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues) : StateEliminator<ValueType>(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) {
+ }
+
+ template<typename ValueType>
+ void PrioritizedStateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
+ stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]);
+ }
+
+ template<typename ValueType>
+ void PrioritizedStateEliminator<ValueType>::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<typename ValueType>
+ void PrioritizedStateEliminator<ValueType>::updatePriority(storm::storage::sparse::state_type const& state) {
+ priorityQueue->update(state);
+ }
+
+ template class PrioritizedStateEliminator<double>;
+
+#ifdef STORM_HAVE_CARL
+ template class PrioritizedStateEliminator<storm::RationalFunction>;
+#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<typename ValueType>
+ class PrioritizedStateEliminator : public StateEliminator<ValueType> {
+ public:
+ typedef typename std::shared_ptr<StatePriorityQueue> PriorityQueuePointer;
+
+ PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& 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<ValueType>& 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<typename SparseModelType>
- StateEliminator<SparseModelType>::StateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions) : transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions) {
+ using namespace storm::utility::stateelimination;
+
+ template<typename ValueType>
+ StateEliminator<ValueType>::StateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions) : transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions) {
+ // Intentionally left empty.
}
- template<typename SparseModelType>
- void StateEliminator<SparseModelType>::eliminateState(storm::storage::sparse::state_type state, bool removeForwardTransitions, storm::storage::BitVector predecessorConstraint) {
-
+ template<typename ValueType>
+ void StateEliminator<ValueType>::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<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::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<FlexibleRowType> 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<storm::models::sparse::Dtmc<double>>;
+ template<typename ValueType>
+ void StateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
+ // Intentionally left empty.
+ }
+
+ template<typename ValueType>
+ void StateEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
+ // Intentionally left empty.
+ }
+
+ template<typename ValueType>
+ void StateEliminator<ValueType>::updatePriority(storm::storage::sparse::state_type const& state) {
+ // Intentionally left empty.
+ }
+
+ template<typename ValueType>
+ bool StateEliminator<ValueType>::filterPredecessor(storm::storage::sparse::state_type const& state) {
+ STORM_LOG_ASSERT(false, "Must not filter predecessors.");
+ return false;
+ }
+
+ template<typename ValueType>
+ bool StateEliminator<ValueType>::isFilterPredecessor() const {
+ return false;
+ }
+
+ template class StateEliminator<double>;
#ifdef STORM_HAVE_CARL
- template class StateEliminator<storm::models::sparse::Dtmc<storm::RationalFunction>>;
+ template class StateEliminator<storm::RationalFunction>;
#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<typename SparseModelType>
+ template<typename ValueType>
class StateEliminator {
- typedef typename SparseModelType::ValueType ValueType;
+ public:
typedef typename storm::storage::FlexibleSparseMatrix<ValueType>::row_type FlexibleRowType;
typedef typename FlexibleRowType::iterator FlexibleRowIterator;
- public:
StateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& 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<ValueType>& transitionMatrix;
storm::storage::FlexibleSparseMatrix<ValueType>& 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 <cstddef>
+
+#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<storm::storage::sparse::state_type> 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 <vector>
+
+#include "src/solver/stateelimination/StatePriorityQueue.h"
+
+namespace storm {
+ namespace solver {
+ namespace stateelimination {
+
+ class StaticStatePriorityQueue : public StatePriorityQueue {
+ public:
+ StaticStatePriorityQueue(std::vector<storm::storage::sparse::state_type> 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<uint_fast64_t> 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 <random>
+
+#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<typename ValueType>
+ 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<typename ValueType>
+ uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> 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<typename ValueType>
+ uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities) {
+ return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size();
+ }
+
+ template<typename ValueType>
+ std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType>& 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<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
+
+ std::vector<storm::storage::sparse::state_type> 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<StaticStatePriorityQueue>(sortedStates);
+ } else {
+ if (eliminationOrderNeedsDistances(order)) {
+ STORM_LOG_THROW(static_cast<bool>(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<StaticStatePriorityQueue>(sortedStates);
+ } else if (eliminationOrderIsPenaltyBased(order)) {
+ std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> statePenalties(sortedStates.size());
+ typename DynamicStatePriorityQueue<ValueType>::PenaltyFunctionType penaltyFunction = order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression<ValueType> : computeStatePenalty<ValueType>;
+ 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<storm::storage::sparse::state_type, uint_fast64_t> const& statePenalty1, std::pair<storm::storage::sparse::state_type, uint_fast64_t> 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<StaticStatePriorityQueue>(sortedStates);
+ } else {
+ // For the dynamic penalty version, we need to give the full state-penalty pairs.
+ return std::make_unique<DynamicStatePriorityQueue<ValueType>>(statePenalties, transitionMatrix, backwardTransitions, oneStepProbabilities, penaltyFunction);
+ }
+ }
+ }
+ STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Illegal elimination order selected.");
+ }
+
+ std::shared_ptr<StatePriorityQueue> createNaivePriorityQueue(storm::storage::BitVector const& states) {
+ std::vector<storm::storage::sparse::state_type> sortedStates(states.begin(), states.end());
+ return std::make_shared<StaticStatePriorityQueue>(sortedStates);
+ }
+
+ template uint_fast64_t estimateComplexity(double const& value);
+ template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<double> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<double> const& backwardTransitions, std::vector<double>& oneStepProbabilities, storm::storage::BitVector const& states);
+ template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<double> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<double> const& backwardTransitions, std::vector<double> const& oneStepProbabilities);
+ template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<double> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<double> const& backwardTransitions, std::vector<double> const& oneStepProbabilities);
+
+
+#ifdef STORM_HAVE_CARL
+ template uint_fast64_t estimateComplexity(storm::RationalFunction const& value);
+ template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction>& oneStepProbabilities, storm::storage::BitVector const& states);
+ template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& oneStepProbabilities);
+ template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> 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 <memory>
+#include <vector>
+
+#include <boost/optional.hpp>
+
+#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<typename ValueType>
+ 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<typename ValueType>
+ uint_fast64_t estimateComplexity(ValueType const& value);
+
+#ifdef STORM_HAVE_CARL
+ template<>
+ uint_fast64_t estimateComplexity(storm::RationalFunction const& value);
+#endif
+
+ template<typename ValueType>
+ uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities);
+
+ template<typename ValueType>
+ uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities);
+
+ template<typename ValueType>
+ std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& stateDistances, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& states);
+
+ std::shared_ptr<StatePriorityQueue> createNaivePriorityQueue(storm::storage::BitVector const& states);
+
+ }
+ }
+}
\ No newline at end of file