diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 662881ed0..1f3067253 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -363,7 +363,7 @@ namespace storm {
// 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);
- std::vector<std::size_t> distancesFromInitialStates;
+ std::vector<uint_fast64_t> distancesFromInitialStates;
storm::storage::BitVector relevantStates;
if (checkTask.isOnlyInitialStatesRelevantSet()) {
// Determine the set of initial states of the sub-model.
@@ -961,53 +961,6 @@ namespace storm {
return maximalDepth;
}
- template<typename SparseDtmcModelType>
- std::vector<uint_fast64_t> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::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) {
- std::vector<uint_fast64_t> statePriorities(transitionMatrix.getRowCount());
- std::vector<storm::storage::sparse::state_type> states(transitionMatrix.getRowCount());
- for (std::size_t index = 0; index < states.size(); ++index) {
- states[index] = index;
- }
-
- std::vector<std::size_t> distances = getStateDistances(transitionMatrix, transitionMatrixTransposed, initialStates, oneStepProbabilities,
- storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder() == storm::settings::modules::EliminationSettings::EliminationOrder::Forward ||
- storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder() == storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed);
-
- // In case of the forward or backward ordering, we can sort the states according to the distances.
- if (forward ^ reverse) {
- std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] < distances[state2]; } );
- } else {
- // Otherwise, we sort them according to descending distances.
- std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] > distances[state2]; } );
- }
-
- // Now convert the ordering of the states to priorities.
- for (uint_fast64_t index = 0; index < states.size(); ++index) {
- statePriorities[states[index]] = index;
- }
-
- return statePriorities;
- }
-
- template<typename SparseDtmcModelType>
- std::vector<std::size_t> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::getStateDistances(storm::storage::SparseMatrix<typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::ValueType> const& transitionMatrix, storm::storage::SparseMatrix<typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::ValueType> const& oneStepProbabilities, bool forward) {
- if (forward) {
- return storm::utility::graph::getDistances(transitionMatrix, initialStates);
- } else {
- // Since the target states were eliminated from the matrix already, we construct a replacement by
- // treating all states that have some non-zero probability to go to a target state in one step as target
- // states.
- storm::storage::BitVector pseudoTargetStates(transitionMatrix.getRowCount());
- for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) {
- if (oneStepProbabilities[index] != storm::utility::zero<ValueType>()) {
- pseudoTargetStates.set(index);
- }
- }
-
- return storm::utility::graph::getDistances(transitionMatrixTransposed, pseudoTargetStates);
- }
- }
-
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) {
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
index 73f419425..8459d4bf3 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
@@ -59,10 +59,6 @@ namespace storm {
static uint_fast64_t performHybridStateElimination(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, 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);
static uint_fast64_t treatScc(storm::storage::FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities = boost::none);
-
- 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 bool checkConsistent(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions);
diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp
index 72e675569..01c91531d 100644
--- a/src/solver/EliminationLinearEquationSolver.cpp
+++ b/src/solver/EliminationLinearEquationSolver.cpp
@@ -2,6 +2,9 @@
#include <numeric>
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/EliminationSettings.h"
+
#include "src/solver/stateelimination/StatePriorityQueue.h"
#include "src/solver/stateelimination/PrioritizedStateEliminator.h"
@@ -13,6 +16,7 @@ namespace storm {
namespace solver {
using namespace stateelimination;
+ using namespace storm::utility::stateelimination;
template<typename ValueType>
EliminationLinearEquationSolver<ValueType>::EliminationLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) : A(A) {
@@ -23,29 +27,30 @@ namespace storm {
void EliminationLinearEquationSolver<ValueType>::solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult) const {
STORM_LOG_WARN_COND(multiplyResult == nullptr, "Providing scratch memory will not improve the performance of this solver.");
-// std::cout << "input:" << std::endl;
-// std::cout << "A:" << std::endl;
-// std::cout << A << std::endl;
-// std::cout << "b:" << std::endl;
-// for (auto const& e : b) {
-// std::cout << e << std::endl;
-// }
-
- // Create a naive priority queue.
- // TODO: improve.
- std::vector<storm::storage::sparse::state_type> allRows(x.size());
- std::iota(allRows.begin(), allRows.end(), 0);
- std::shared_ptr<StatePriorityQueue> priorityQueue = storm::utility::stateelimination::createStatePriorityQueue(allRows);
-
+ // We need to revert the transformation into an equation system matrix, because the elimination procedure
+ // and the distance computation is based on the probability matrix instead.
+ storm::storage::SparseMatrix<ValueType> transitionMatrix(A);
+ transitionMatrix.convertToEquationSystem();
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = A.transpose();
+
// Initialize the solution to the right-hand side of the equation system.
x = b;
// Translate the matrix and its transpose into the flexible format.
- // We need to revert the matrix from the equation system format to the probability matrix format. That is,
- // from (I-P), we construct P. Note that for the backwards transitions, this does not need to be done, as all
- // entries are set to one anyway.
- storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(A, false, true);
- storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(A.transpose(), true, true);
+ storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(transitionMatrix, false);
+ storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardTransitions, true);
+
+ storm::settings::modules::EliminationSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder();
+ boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
+ if (eliminationOrderNeedsDistances(order)) {
+ // Compute the distance from the first state.
+ // FIXME: This is not exactly the initial states.
+ storm::storage::BitVector initialStates = storm::storage::BitVector(A.getRowCount());
+ initialStates.set(0);
+ distanceBasedPriorities = getDistanceBasedPriorities(transitionMatrix, backwardTransitions, initialStates, b, eliminationOrderNeedsForwardDistances(order), eliminationOrderNeedsReversedDistances(order));
+ }
+
+ std::shared_ptr<StatePriorityQueue> priorityQueue = createStatePriorityQueue<ValueType>(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, b, storm::storage::BitVector(x.size(), true));
// std::cout << "intermediate:" << std::endl;
// std::cout << "flexibleMatrix:" << std::endl;
diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp
index 05541ae01..5705c10b9 100644
--- a/src/utility/graph.cpp
+++ b/src/utility/graph.cpp
@@ -83,10 +83,10 @@ namespace storm {
}
template<typename T>
- std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem) {
- std::vector<std::size_t> distances(transitionMatrix.getRowGroupCount());
+ std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem) {
+ std::vector<uint_fast64_t> distances(transitionMatrix.getRowGroupCount());
- std::vector<std::pair<storm::storage::sparse::state_type, std::size_t>> stateQueue;
+ std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> stateQueue;
stateQueue.reserve(transitionMatrix.getRowGroupCount());
storm::storage::BitVector statesInQueue(transitionMatrix.getRowGroupCount());
@@ -993,7 +993,7 @@ namespace storm {
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);
- template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
+ template std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
@@ -1065,7 +1065,7 @@ namespace storm {
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);
- template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
+ template std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
@@ -1119,7 +1119,7 @@ namespace storm {
// Instantiations for storm::RationalNumber.
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);
- template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
+ template std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
@@ -1174,7 +1174,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);
- template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
+ template std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
diff --git a/src/utility/graph.h b/src/utility/graph.h
index 611d983bb..26f73902d 100644
--- a/src/utility/graph.h
+++ b/src/utility/graph.h
@@ -71,7 +71,7 @@ namespace storm {
* @return The distances of each state to the initial states of the sarch.
*/
template<typename T>
- std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem = boost::none);
+ std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem = boost::none);
/*!
* Performs a backward depth-first search trough the underlying graph structure
diff --git a/src/utility/stateelimination.cpp b/src/utility/stateelimination.cpp
index c2882dcde..7076c3f15 100644
--- a/src/utility/stateelimination.cpp
+++ b/src/utility/stateelimination.cpp
@@ -11,6 +11,7 @@
#include "src/settings/SettingsManager.h"
+#include "src/utility/graph.h"
#include "src/utility/macros.h"
#include "src/utility/constants.h"
#include "src/exceptions/InvalidStateException.h"
@@ -95,7 +96,7 @@ namespace storm {
}
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) {
+ 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> const& oneStepProbabilities, storm::storage::BitVector const& states) {
STORM_LOG_TRACE("Creating state priority queue for states " << states);
@@ -147,20 +148,73 @@ namespace storm {
return std::make_shared<StaticStatePriorityQueue>(states);
}
+ template<typename ValueType>
+ 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) {
+ std::vector<uint_fast64_t> statePriorities(transitionMatrix.getRowCount());
+ std::vector<storm::storage::sparse::state_type> states(transitionMatrix.getRowCount());
+ for (std::size_t index = 0; index < states.size(); ++index) {
+ states[index] = index;
+ }
+
+ std::vector<uint_fast64_t> distances = getStateDistances(transitionMatrix, transitionMatrixTransposed, initialStates, oneStepProbabilities,
+ storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder() == storm::settings::modules::EliminationSettings::EliminationOrder::Forward ||
+ storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder() == storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed);
+
+ // In case of the forward or backward ordering, we can sort the states according to the distances.
+ if (forward ^ reverse) {
+ std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] < distances[state2]; } );
+ } else {
+ // Otherwise, we sort them according to descending distances.
+ std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] > distances[state2]; } );
+ }
+
+ // Now convert the ordering of the states to priorities.
+ for (uint_fast64_t index = 0; index < states.size(); ++index) {
+ statePriorities[states[index]] = index;
+ }
+
+ return statePriorities;
+ }
+
+ template<typename ValueType>
+ std::vector<uint_fast64_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) {
+ if (forward) {
+ return storm::utility::graph::getDistances(transitionMatrix, initialStates);
+ } else {
+ // Since the target states were eliminated from the matrix already, we construct a replacement by
+ // treating all states that have some non-zero probability to go to a target state in one step as target
+ // states.
+ storm::storage::BitVector pseudoTargetStates(transitionMatrix.getRowCount());
+ for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) {
+ if (oneStepProbabilities[index] != storm::utility::zero<ValueType>()) {
+ pseudoTargetStates.set(index);
+ }
+ }
+
+ return storm::utility::graph::getDistances(transitionMatrixTransposed, pseudoTargetStates);
+ }
+ }
+
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 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> const& 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);
-
+ template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<double> const& oneStepProbabilities, bool forward, bool reverse);
+ template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<double> const& oneStepProbabilities, bool forward);
+
template uint_fast64_t estimateComplexity(storm::RationalNumber const& value);
- template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber>& oneStepProbabilities, storm::storage::BitVector const& states);
+ template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& oneStepProbabilities, storm::storage::BitVector const& states);
template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& oneStepProbabilities);
template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& oneStepProbabilities);
+ template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalNumber> const& oneStepProbabilities, bool forward, bool reverse);
+ template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalNumber> const& oneStepProbabilities, bool forward);
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 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> const& 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);
+ template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalFunction> const& oneStepProbabilities, bool forward, bool reverse);
+ template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalFunction> const& oneStepProbabilities, bool forward);
}
}
}
\ No newline at end of file
diff --git a/src/utility/stateelimination.h b/src/utility/stateelimination.h
index 13c8904eb..b3d940ab2 100644
--- a/src/utility/stateelimination.h
+++ b/src/utility/stateelimination.h
@@ -23,6 +23,9 @@ namespace storm {
template<typename ValueType>
class FlexibleSparseMatrix;
+
+ template<typename ValueType>
+ class SparseMatrix;
}
namespace utility {
@@ -51,11 +54,17 @@ namespace storm {
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> 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> const& oneStepProbabilities, storm::storage::BitVector const& states);
std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(storm::storage::BitVector const& states);
std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(std::vector<storm::storage::sparse::state_type> const& states);
+ template<typename ValueType>
+ 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);
+
+ template<typename ValueType>
+ std::vector<uint_fast64_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);
+
}
}
}
\ No newline at end of file