stateelimination.cpp File Reference

#include "storm/utility/stateelimination.h"
#include <random>
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/settings/SettingsManager.h"
#include "storm/solver/stateelimination/DynamicStatePriorityQueue.h"
#include "storm/solver/stateelimination/StatePriorityQueue.h"
#include "storm/solver/stateelimination/StaticStatePriorityQueue.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/FlexibleSparseMatrix.h"
#include "storm/utility/constants.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"

Include dependency graph for stateelimination.cpp:

Go to the source code of this file.

Namespaces
namespace	storm
namespace	storm::utility
namespace	storm::utility::stateelimination

Functions
bool	storm::utility::stateelimination::eliminationOrderNeedsDistances (storm::settings::modules::EliminationSettings::EliminationOrder const &order)
bool	storm::utility::stateelimination::eliminationOrderNeedsForwardDistances (storm::settings::modules::EliminationSettings::EliminationOrder const &order)
bool	storm::utility::stateelimination::eliminationOrderNeedsReversedDistances (storm::settings::modules::EliminationSettings::EliminationOrder const &order)
bool	storm::utility::stateelimination::eliminationOrderIsPenaltyBased (storm::settings::modules::EliminationSettings::EliminationOrder const &order)
bool	storm::utility::stateelimination::eliminationOrderIsStatic (storm::settings::modules::EliminationSettings::EliminationOrder const &order)
template<typename ValueType >
uint_fast64_t	storm::utility::stateelimination::estimateComplexity (ValueType const &)
template<>
uint_fast64_t	storm::utility::stateelimination::estimateComplexity (storm::RationalFunction const &value)
template<typename ValueType >
uint_fast64_t	storm::utility::stateelimination::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	storm::utility::stateelimination::computeStatePenaltyRegularExpression (storm::storage::sparse::state_type const &state, storm::storage::FlexibleSparseMatrix< ValueType > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< ValueType > const &backwardTransitions, std::vector< ValueType > const &)
template<typename ValueType >
std::shared_ptr< StatePriorityQueue >	storm::utility::stateelimination::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)
std::shared_ptr< StatePriorityQueue >	storm::utility::stateelimination::createStatePriorityQueue (storm::storage::BitVector const &states)
std::shared_ptr< StatePriorityQueue >	storm::utility::stateelimination::createStatePriorityQueue (std::vector< storm::storage::sparse::state_type > const &states)
template<typename ValueType >
std::vector< uint_fast64_t >	storm::utility::stateelimination::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 >	storm::utility::stateelimination::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)
template uint_fast64_t	storm::utility::stateelimination::estimateComplexity (double const &value)
template std::shared_ptr< StatePriorityQueue >	storm::utility::stateelimination::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	storm::utility::stateelimination::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	storm::utility::stateelimination::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 >	storm::utility::stateelimination::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 >	storm::utility::stateelimination::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	storm::utility::stateelimination::estimateComplexity (storm::RationalNumber const &value)
template std::shared_ptr< StatePriorityQueue >	storm::utility::stateelimination::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	storm::utility::stateelimination::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	storm::utility::stateelimination::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 >	storm::utility::stateelimination::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 >	storm::utility::stateelimination::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 std::shared_ptr< StatePriorityQueue >	storm::utility::stateelimination::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	storm::utility::stateelimination::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	storm::utility::stateelimination::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 >	storm::utility::stateelimination::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 >	storm::utility::stateelimination::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)