Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::utility::stateelimination Namespace Reference

Functions

bool eliminationOrderNeedsDistances (storm::settings::modules::EliminationSettings::EliminationOrder const &order)
 
bool eliminationOrderNeedsForwardDistances (storm::settings::modules::EliminationSettings::EliminationOrder const &order)
 
bool eliminationOrderNeedsReversedDistances (storm::settings::modules::EliminationSettings::EliminationOrder const &order)
 
bool eliminationOrderIsPenaltyBased (storm::settings::modules::EliminationSettings::EliminationOrder const &order)
 
bool eliminationOrderIsStatic (storm::settings::modules::EliminationSettings::EliminationOrder const &order)
 
template<typename ValueType >
uint_fast64_t estimateComplexity (ValueType const &)
 
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< StatePriorityQueuecreateStatePriorityQueue (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< StatePriorityQueuecreateStatePriorityQueue (storm::storage::BitVector const &states)
 
std::shared_ptr< StatePriorityQueuecreateStatePriorityQueue (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)
 
template uint_fast64_t estimateComplexity (double const &value)
 
template std::shared_ptr< StatePriorityQueuecreateStatePriorityQueue (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)
 

Function Documentation

◆ computeStatePenalty() [1/2]

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 
)

◆ computeStatePenalty() [2/2]

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 
)

Definition at line 71 of file stateelimination.cpp.

◆ computeStatePenaltyRegularExpression() [1/2]

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 
)

◆ computeStatePenaltyRegularExpression() [2/2]

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 &   
)

Definition at line 97 of file stateelimination.cpp.

◆ createStatePriorityQueue() [1/4]

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 
)

◆ createStatePriorityQueue() [2/4]

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 
)

Definition at line 104 of file stateelimination.cpp.

◆ createStatePriorityQueue() [3/4]

std::shared_ptr< StatePriorityQueue > storm::utility::stateelimination::createStatePriorityQueue ( std::vector< storm::storage::sparse::state_type > const &  states)

Definition at line 166 of file stateelimination.cpp.

◆ createStatePriorityQueue() [4/4]

std::shared_ptr< StatePriorityQueue > storm::utility::stateelimination::createStatePriorityQueue ( storm::storage::BitVector const &  states)

Definition at line 161 of file stateelimination.cpp.

◆ eliminationOrderIsPenaltyBased()

bool storm::utility::stateelimination::eliminationOrderIsPenaltyBased ( storm::settings::modules::EliminationSettings::EliminationOrder const &  order)

Definition at line 41 of file stateelimination.cpp.

◆ eliminationOrderIsStatic()

bool storm::utility::stateelimination::eliminationOrderIsStatic ( storm::settings::modules::EliminationSettings::EliminationOrder const &  order)

Definition at line 47 of file stateelimination.cpp.

◆ eliminationOrderNeedsDistances()

bool storm::utility::stateelimination::eliminationOrderNeedsDistances ( storm::settings::modules::EliminationSettings::EliminationOrder const &  order)

Definition at line 24 of file stateelimination.cpp.

◆ eliminationOrderNeedsForwardDistances()

bool storm::utility::stateelimination::eliminationOrderNeedsForwardDistances ( storm::settings::modules::EliminationSettings::EliminationOrder const &  order)

Definition at line 31 of file stateelimination.cpp.

◆ eliminationOrderNeedsReversedDistances()

bool storm::utility::stateelimination::eliminationOrderNeedsReversedDistances ( storm::settings::modules::EliminationSettings::EliminationOrder const &  order)

Definition at line 36 of file stateelimination.cpp.

◆ estimateComplexity() [1/2]

template uint_fast64_t storm::utility::stateelimination::estimateComplexity ( double const &  value)

◆ estimateComplexity() [2/2]

template<typename ValueType >
uint_fast64_t storm::utility::stateelimination::estimateComplexity ( ValueType const &  )

Definition at line 52 of file stateelimination.cpp.

◆ getDistanceBasedPriorities() [1/2]

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 
)

◆ getDistanceBasedPriorities() [2/2]

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 
)

Definition at line 171 of file stateelimination.cpp.

◆ getStateDistances() [1/2]

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 
)

◆ getStateDistances() [2/2]

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 
)

Definition at line 211 of file stateelimination.cpp.