storm::solver::stateelimination Namespace Reference

Classes
class	ConditionalStateEliminator
struct	PriorityComparator
class	DynamicStatePriorityQueue
class	EliminatorBase
class	EquationSystemEliminator
class	MultiValueStateEliminator
class	NondeterministicModelStateEliminator
class	PrioritizedStateEliminator
class	StateEliminator
class	StatePriorityQueue
class	StaticStatePriorityQueue

Enumerations
enum class	EliminationMethod { State , Scc , Hybrid }
	An enum that contains all available elimination methods. More...
enum class	EliminationOrder {   Forward , ForwardReversed , Backward , BackwardReversed ,   Random , StaticPenalty , DynamicPenalty , RegularExpression }
	An enum that contains all available state elimination orders. More...
enum class	ScalingMode { Divide , DivideOneMinus }

Functions
bool	eliminationOrderNeedsDistances (EliminationOrder const &order)
bool	eliminationOrderNeedsForwardDistances (EliminationOrder const &order)
bool	eliminationOrderNeedsReversedDistances (EliminationOrder const &order)
bool	eliminationOrderIsPenaltyBased (EliminationOrder const &order)
bool	eliminationOrderIsStatic (EliminationOrder const &order)
template<typename ValueType>
uint_fast64_t	estimateComplexity (ValueType const &)
template<>
uint_fast64_t	estimateComplexity (storm::RationalFunction const &value)
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 &)
template<typename ValueType>
std::shared_ptr< StatePriorityQueue >	createStatePriorityQueue (EliminationOrder const &order, 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 >	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 (EliminationOrder const &order, 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)
template uint_fast64_t	estimateComplexity (double const &value)
template std::shared_ptr< StatePriorityQueue >	createStatePriorityQueue (EliminationOrder const &order, 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 (EliminationOrder const &order, 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 (EliminationOrder const &order, 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 (EliminationOrder const &order, 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 std::shared_ptr< StatePriorityQueue >	createStatePriorityQueue (EliminationOrder const &order, 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 (EliminationOrder const &order, 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)
template<>
uint_fast64_t	estimateComplexity (storm::RationalFunction const &value)

Enumeration Type Documentation

EliminationMethod

enum class storm::solver::stateelimination::EliminationMethod

strong

An enum that contains all available elimination methods.

Enumerator
State
Scc
Hybrid

Definition at line 10 of file EliminationMethod.h.

EliminationOrder

enum class storm::solver::stateelimination::EliminationOrder

strong

An enum that contains all available state elimination orders.

Enumerator
Forward
ForwardReversed
Backward
BackwardReversed
Random
StaticPenalty
DynamicPenalty
RegularExpression

Definition at line 10 of file EliminationOrder.h.

ScalingMode

enum class storm::solver::stateelimination::ScalingMode

strong

Enumerator
Divide
DivideOneMinus

Definition at line 11 of file EliminatorBase.h.

Function Documentation

computeStatePenalty() [1/4]

template uint_fast64_t storm::solver::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 )

computeStatePenalty() [2/4]

template uint_fast64_t storm::solver::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 )

computeStatePenalty() [3/4]

template uint_fast64_t storm::solver::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 )

computeStatePenalty() [4/4]

template<typename ValueType>

uint_fast64_t storm::solver::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 )

Definition at line 60 of file StateEliminationUtility.cpp.

computeStatePenaltyRegularExpression() [1/4]

template uint_fast64_t storm::solver::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 )

computeStatePenaltyRegularExpression() [2/4]

template uint_fast64_t storm::solver::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 )

computeStatePenaltyRegularExpression() [3/4]

template uint_fast64_t storm::solver::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 )

computeStatePenaltyRegularExpression() [4/4]

template<typename ValueType>

uint_fast64_t storm::solver::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 &	)

Definition at line 86 of file StateEliminationUtility.cpp.

createStatePriorityQueue() [1/6]

template std::shared_ptr< StatePriorityQueue > storm::solver::stateelimination::createStatePriorityQueue	(	EliminationOrder const &	order,
		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 )

createStatePriorityQueue() [2/6]

template std::shared_ptr< StatePriorityQueue > storm::solver::stateelimination::createStatePriorityQueue	(	EliminationOrder const &	order,
		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 )

createStatePriorityQueue() [3/6]

template std::shared_ptr< StatePriorityQueue > storm::solver::stateelimination::createStatePriorityQueue	(	EliminationOrder const &	order,
		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 )

createStatePriorityQueue() [4/6]

template<typename ValueType>

std::shared_ptr< StatePriorityQueue > storm::solver::stateelimination::createStatePriorityQueue	(	EliminationOrder const &	order,
		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 )

Definition at line 93 of file StateEliminationUtility.cpp.

createStatePriorityQueue() [5/6]

std::shared_ptr< StatePriorityQueue > storm::solver::stateelimination::createStatePriorityQueue

(

std::vector< storm::storage::sparse::state_type > const &

states

)

Definition at line 151 of file StateEliminationUtility.cpp.

createStatePriorityQueue() [6/6]

std::shared_ptr< StatePriorityQueue > storm::solver::stateelimination::createStatePriorityQueue

(

storm::storage::BitVector const &

states

)

Definition at line 146 of file StateEliminationUtility.cpp.

eliminationOrderIsPenaltyBased()

bool storm::solver::stateelimination::eliminationOrderIsPenaltyBased

(

EliminationOrder const &

order

)

Definition at line 34 of file StateEliminationUtility.cpp.

eliminationOrderIsStatic()

bool storm::solver::stateelimination::eliminationOrderIsStatic

(

EliminationOrder const &

order

)

Definition at line 38 of file StateEliminationUtility.cpp.

eliminationOrderNeedsDistances()

bool storm::solver::stateelimination::eliminationOrderNeedsDistances

(

EliminationOrder const &

order

)

Definition at line 21 of file StateEliminationUtility.cpp.

eliminationOrderNeedsForwardDistances()

bool storm::solver::stateelimination::eliminationOrderNeedsForwardDistances

(

EliminationOrder const &

order

)

Definition at line 26 of file StateEliminationUtility.cpp.

eliminationOrderNeedsReversedDistances()

bool storm::solver::stateelimination::eliminationOrderNeedsReversedDistances

(

EliminationOrder const &

order

)

Definition at line 30 of file StateEliminationUtility.cpp.

estimateComplexity() [1/5]

template uint_fast64_t storm::solver::stateelimination::estimateComplexity

(

double const &

value

)

estimateComplexity() [2/5]

template<>

uint_fast64_t storm::solver::stateelimination::estimateComplexity

(

storm::RationalFunction const &

value

)

Definition at line 48 of file StateEliminationUtility.cpp.

estimateComplexity() [3/5]

template<>

uint_fast64_t storm::solver::stateelimination::estimateComplexity

(

storm::RationalFunction const &

value

)

Definition at line 48 of file StateEliminationUtility.cpp.

estimateComplexity() [4/5]

template uint_fast64_t storm::solver::stateelimination::estimateComplexity

(

storm::RationalNumber const &

value

)

estimateComplexity() [5/5]

template<typename ValueType>

uint_fast64_t storm::solver::stateelimination::estimateComplexity

(

ValueType const &

)

Definition at line 43 of file StateEliminationUtility.cpp.

getDistanceBasedPriorities() [1/4]

template std::vector< uint_fast64_t > storm::solver::stateelimination::getDistanceBasedPriorities	(	EliminationOrder const &	order,
		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 )

getDistanceBasedPriorities() [2/4]

template std::vector< uint_fast64_t > storm::solver::stateelimination::getDistanceBasedPriorities	(	EliminationOrder const &	order,
		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 )

getDistanceBasedPriorities() [3/4]

template std::vector< uint_fast64_t > storm::solver::stateelimination::getDistanceBasedPriorities	(	EliminationOrder const &	order,
		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 )

getDistanceBasedPriorities() [4/4]

template<typename ValueType>

std::vector< uint_fast64_t > storm::solver::stateelimination::getDistanceBasedPriorities	(	EliminationOrder const &	order,
		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 )

Definition at line 156 of file StateEliminationUtility.cpp.

getStateDistances() [1/4]

template std::vector< uint_fast64_t > storm::solver::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 )

getStateDistances() [2/4]

template std::vector< uint_fast64_t > storm::solver::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 )

getStateDistances() [3/4]

template std::vector< uint_fast64_t > storm::solver::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 )

getStateDistances() [4/4]

template<typename ValueType>

std::vector< uint_fast64_t > storm::solver::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 )

Definition at line 192 of file StateEliminationUtility.cpp.