sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

added obeying a state ordering to elimination linear equation solver 

Former-commit-id: 5a62842963
tempestpy_adaptions
dehnert 9 years ago
parent
a699272dc6
commit
82d4164c39
7 changed files with 102 additions and 85 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 49
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  2. 4
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
  3. 43
      src/solver/EliminationLinearEquationSolver.cpp
  4. 14
      src/utility/graph.cpp
  5. 2
      src/utility/graph.h
  6. 64
      src/utility/stateelimination.cpp
  7. 11
      src/utility/stateelimination.h

49
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -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) {

4
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
View File

@ -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);

43
src/solver/EliminationLinearEquationSolver.cpp
View File

@ -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;

14
src/utility/graph.cpp
View File

@ -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);

2
src/utility/graph.h
View File

@ -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

64
src/utility/stateelimination.cpp
View File

@ -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);
}
}
}

11
src/utility/stateelimination.h
View File

@ -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);
}
}
}
Write Preview
Loading…
Cancel
Save