Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm::utility::graph Namespace Reference

Classes

struct  ExplicitGameProb01Result
 
struct  SymbolicGameProb01Result
 

Functions

template<typename T >
storm::storage::BitVector getReachableOneStep (storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates)
 Computes the states reachable in one step from the states indicated by the bitvector.
 
template<typename T >
storm::storage::BitVector getReachableStates (storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &constraintStates, storm::storage::BitVector const &targetStates, bool useStepBound=false, uint_fast64_t maximalSteps=0, boost::optional< storm::storage::BitVector > const &choiceFilter=boost::none)
 Performs a forward depth-first search through the underlying graph structure to identify the states that are reachable from the given set only passing through a constrained set of states until some target have been reached.
 
template<typename T >
storm::storage::BitVector getBsccCover (storm::storage::SparseMatrix< T > const &transitionMatrix)
 Retrieves a set of states that covers als BSCCs of the system in the sense that for every BSCC exactly one state is included in the cover.
 
template<typename T >
bool hasCycle (storm::storage::SparseMatrix< T > const &transitionMatrix, boost::optional< storm::storage::BitVector > const &subsystem=boost::none)
 Returns true if the graph represented by the given matrix has a cycle.
 
template<typename T >
bool checkIfECWithChoiceExists (storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &subsystem, storm::storage::BitVector const &choices)
 Checks whether there is an End Component that.
 
template<typename T >
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 breadth-first search through the underlying graph structure to compute the distance from all states to the starting states of the search.
 
template<typename T >
storm::storage::BitVector performProbGreater0 (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound=false, uint_fast64_t maximalSteps=0)
 Performs a backward depth-first search trough the underlying graph structure of the given model to determine which states of the model have a positive probability of satisfying phi until psi.
 
template<typename T >
storm::storage::BitVector performProb1 (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::BitVector const &statesWithProbabilityGreater0)
 Computes the set of states of the given model for which all paths lead to the given set of target states and only visit states from the filter set before.
 
template<typename T >
storm::storage::BitVector performProb1 (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 Computes the set of states of the given model for which all paths lead to the given set of target states and only visit states from the filter set before.
 
template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01 (storm::models::sparse::DeterministicModel< T > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.
 
template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01 (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > performProbGreater0 (storm::models::symbolic::Model< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, boost::optional< uint_fast64_t > const &stepBound=boost::optional< uint_fast64_t >())
 Computes the set of states that has a positive probability of reaching psi states after only passing through phi states before.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > performProb1 (storm::models::symbolic::Model< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, storm::dd::Bdd< Type > const &statesWithProbabilityGreater0)
 Computes the set of states that have a probability of one of reaching psi states after only passing through phi states before.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > performProb1 (storm::models::symbolic::Model< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 Computes the set of states that have a probability of one of reaching psi states after only passing through phi states before.
 
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > performProb01 (storm::models::symbolic::DeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.
 
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > performProb01 (storm::models::symbolic::Model< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.
 
template<typename T , typename SchedulerValueType >
void computeSchedulerStayingInStates (storm::storage::BitVector const &states, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter=boost::none)
 Computes a scheduler for the given states that chooses an action that stays completely in the very same set.
 
template<typename T , typename SchedulerValueType >
void computeSchedulerWithOneSuccessorInStates (storm::storage::BitVector const &states, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler)
 
template<typename T , typename SchedulerValueType >
void computeSchedulerProbGreater0E (storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter=boost::none)
 Computes a scheduler for the ProbGreater0E-States such that in the induced system the given psiStates are reachable via phiStates.
 
template<typename T , typename SchedulerValueType >
void computeSchedulerProb0E (storm::storage::BitVector const &prob0EStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler)
 Computes a scheduler for the given states that have a scheduler that has a probability 0.
 
template<typename T , typename SchedulerValueType >
void computeSchedulerRewInf (storm::storage::BitVector const &rewInfStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::Scheduler< SchedulerValueType > &scheduler)
 Computes a scheduler for the given states that have a scheduler that has a reward infinity.
 
template<typename T , typename SchedulerValueType >
void computeSchedulerProb1E (storm::storage::BitVector const &prob1EStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter=boost::none)
 Computes a scheduler for the given prob1EStates such that in the induced system the given psiStates are reached with probability 1.
 
template<typename T >
storm::storage::BitVector performProbGreater0E (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound=false, uint_fast64_t maximalSteps=0)
 Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.
 
template<typename T >
storm::storage::BitVector performProb0A (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template<typename T >
storm::storage::BitVector performProb1E (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, boost::optional< storm::storage::BitVector > const &choiceConstraint=boost::none)
 Computes the sets of states that have probability 1 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.
 
template<typename T , typename RM >
storm::storage::BitVector performProb1E (storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 Computes the sets of states that have probability 1 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.
 
template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01Max (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template<typename T , typename RM >
std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01Max (storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a non-deterministic model in which all non-deterministic choices are resolved such that the probability is maximized.
 
template<typename T >
storm::storage::BitVector performProbGreater0A (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound=false, uint_fast64_t maximalSteps=0, boost::optional< storm::storage::BitVector > const &choiceConstraint=boost::none)
 Computes the sets of states that have probability greater 0 of satisfying phi until psi under any possible resolution of non-determinism in a non-deterministic model.
 
template<typename T , typename RM >
storm::storage::BitVector performProb0E (storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 Computes the sets of states that have probability 0 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.
 
template<typename T >
storm::storage::BitVector performProb0E (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template<typename T , typename RM >
storm::storage::BitVector performProb1A (storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 Computes the sets of states that have probability 1 of satisfying phi until psi under all possible resolutions of non-determinism in a non-deterministic model.
 
template<typename T >
storm::storage::BitVector performProb1A (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01Min (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template<typename T , typename RM >
std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01Min (storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a non-deterministic model in which all non-deterministic choices are resolved such that the probability is minimized.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > computeSchedulerProbGreater0E (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 Computes a scheduler realizing a probability greater zero of satisfying phi until psi for all such states.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > performProbGreater0E (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 Computes the set of states for which there exists a scheduler that achieves a probability greater than zero of satisfying phi until psi.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > performProb0A (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 Computes the set of states for which there does not exist a scheduler that achieves a probability greater than zero of satisfying phi until psi.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > performProbGreater0A (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 Computes the set of states for which all schedulers achieve a probability greater than zero of satisfying phi until psi.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > performProb0E (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 Computes the set of states for which there exists a scheduler that achieves probability zero of satisfying phi until psi.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > performProb1A (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &psiStates, storm::dd::Bdd< Type > const &statesWithProbabilityGreater0A)
 Computes the set of states for which all schedulers achieve probability one of satisfying phi until psi.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > performProb1E (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, storm::dd::Bdd< Type > const &statesWithProbabilityGreater0E)
 Computes the set of states for which there exists a scheduler that achieves probability one of satisfying phi until psi.
 
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > computeSchedulerProb1E (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, storm::dd::Bdd< Type > const &statesWithProbability1E)
 Computes a scheduler satisfying phi until psi with probability 1.
 
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > performProb01Max (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > performProb01Max (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > performProb01Min (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > performProb01Min (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
 
template<typename ValueType >
ExplicitGameProb01Result performProb0 (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint64_t > const &player1Groups, storm::storage::SparseMatrix< ValueType > const &player1BackwardTransitions, std::vector< uint64_t > const &player2BackwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::storage::ExplicitGameStrategyPair *strategyPair=nullptr)
 Computes the set of states that have probability 0 given the strategies of the two players.
 
template<storm::dd::DdType Type, typename ValueType >
SymbolicGameProb01Result< Type > performProb0 (storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, storm::OptimizationDirection const &player1Strategy, storm::OptimizationDirection const &player2Strategy, bool producePlayer1Strategy=false, bool producePlayer2Strategy=false)
 Computes the set of states that have probability 0 given the strategies of the two players.
 
template<typename ValueType >
ExplicitGameProb01Result performProb1 (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint64_t > const &player1Groups, storm::storage::SparseMatrix< ValueType > const &player1BackwardTransitions, std::vector< uint64_t > const &player2BackwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::storage::ExplicitGameStrategyPair *strategyPair=nullptr, boost::optional< storm::storage::BitVector > const &player1Candidates=boost::none)
 Computes the set of states that have probability 1 given the strategies of the two players.
 
template<storm::dd::DdType Type, typename ValueType >
SymbolicGameProb01Result< Type > performProb1 (storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, storm::OptimizationDirection const &player1Strategy, storm::OptimizationDirection const &player2Strategy, bool producePlayer1Strategy=false, bool producePlayer2Strategy=false, boost::optional< storm::dd::Bdd< Type > > const &player1Candidates=boost::none)
 Computes the set of states that have probability 1 given the strategies of the two players.
 
template<typename T >
void topologicalSortHelper (storm::storage::SparseMatrix< T > const &matrix, uint64_t state, std::vector< uint_fast64_t > &topologicalSort, std::vector< uint_fast64_t > &recursionStack, std::vector< typename storm::storage::SparseMatrix< T >::const_iterator > &iteratorRecursionStack, storm::storage::BitVector &visitedStates)
 
template<typename T >
std::vector< uint_fast64_t > getBFSSort (storm::storage::SparseMatrix< T > const &matrix, std::vector< uint_fast64_t > const &firstStates)
 
template<typename T >
std::vector< uint_fast64_t > getTopologicalSort (storm::storage::SparseMatrix< T > const &matrix, std::vector< uint64_t > const &firstStates={})
 Performs a topological sort of the states of the system according to the given transitions.
 
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, boost::optional< storm::storage::BitVector > const &choiceFilter)
 
template storm::storage::BitVector getBsccCover (storm::storage::SparseMatrix< double > const &transitionMatrix)
 
template bool hasCycle (storm::storage::SparseMatrix< double > const &transitionMatrix, boost::optional< storm::storage::BitVector > const &subsystem)
 
template bool checkIfECWithChoiceExists (storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &subsystem, storm::storage::BitVector const &choices)
 
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)
 
template storm::storage::BitVector performProb1 (storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::BitVector const &statesWithProbabilityGreater0)
 
template storm::storage::BitVector performProb1 (storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01 (storm::models::sparse::DeterministicModel< double > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01 (storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template void computeSchedulerProbGreater0E (storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< double > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter)
 
template void computeSchedulerProb0E (storm::storage::BitVector const &prob0EStates, storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::Scheduler< double > &scheduler)
 
template void computeSchedulerRewInf (storm::storage::BitVector const &rewInfStates, storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::Scheduler< double > &scheduler)
 
template void computeSchedulerProb1E (storm::storage::BitVector const &prob1EStates, storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< double > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter=boost::none)
 
template storm::storage::BitVector performProbGreater0E (storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound=false, uint_fast64_t maximalSteps=0)
 
template storm::storage::BitVector performProb0A (storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template storm::storage::BitVector performProb1E (storm::storage::SparseMatrix< double > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, boost::optional< storm::storage::BitVector > const &choiceConstraint=boost::none)
 
template storm::storage::BitVector performProb1E (storm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > const &model, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01Max (storm::storage::SparseMatrix< double > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01Max (storm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template storm::storage::BitVector performProbGreater0A (storm::storage::SparseMatrix< double > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound=false, uint_fast64_t maximalSteps=0, boost::optional< storm::storage::BitVector > const &choiceConstraint=boost::none)
 
template storm::storage::BitVector performProb0E (storm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > const &model, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template storm::storage::BitVector performProb0E (storm::storage::SparseMatrix< double > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template storm::storage::BitVector performProb1A (storm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > const &model, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template storm::storage::BitVector performProb1A (storm::storage::SparseMatrix< double > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01Min (storm::storage::SparseMatrix< double > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template std::pair< storm::storage::BitVector, storm::storage::BitVectorperformProb01Min (storm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
 
template ExplicitGameProb01Result performProb0 (storm::storage::SparseMatrix< double > const &transitionMatrix, std::vector< uint64_t > const &player1RowGrouping, storm::storage::SparseMatrix< double > const &player1BackwardTransitions, std::vector< uint64_t > const &player2BackwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::storage::ExplicitGameStrategyPair *strategyPair)
 
template ExplicitGameProb01Result performProb1 (storm::storage::SparseMatrix< double > const &transitionMatrix, std::vector< uint64_t > const &player1RowGrouping, storm::storage::SparseMatrix< double > const &player1BackwardTransitions, std::vector< uint64_t > const &player2BackwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::storage::ExplicitGameStrategyPair *strategyPair, boost::optional< storm::storage::BitVector > const &player1Candidates)
 
template std::vector< uint_fast64_t > getTopologicalSort (storm::storage::SparseMatrix< double > const &matrix, std::vector< uint64_t > const &firstStates)
 
template storm::dd::Bdd< storm::dd::DdType::CUDDperformProbGreater0 (storm::models::symbolic::Model< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates, boost::optional< uint_fast64_t > const &stepBound=boost::optional< uint_fast64_t >())
 
template storm::dd::Bdd< storm::dd::DdType::CUDDperformProb1 (storm::models::symbolic::Model< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &statesWithProbabilityGreater0)
 
template storm::dd::Bdd< storm::dd::DdType::CUDDperformProb1 (storm::models::symbolic::Model< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > performProb01 (storm::models::symbolic::DeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > performProb01 (storm::models::symbolic::Model< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::CUDDcomputeSchedulerProbGreater0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::CUDDperformProbGreater0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::CUDDperformProb0A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::CUDDperformProbGreater0A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::CUDDperformProb0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::CUDDperformProb1A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &statesWithProbabilityGreater0A)
 
template storm::dd::Bdd< storm::dd::DdType::CUDDperformProb1E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &statesWithProbabilityGreater0E)
 
template storm::dd::Bdd< storm::dd::DdType::CUDDcomputeSchedulerProb1E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &statesWithProbability1E)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > performProb01Max (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > performProb01Max (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > performProb01Min (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > performProb01Min (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates)
 
template SymbolicGameProb01Result< storm::dd::DdType::CUDDperformProb0 (storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates, storm::OptimizationDirection const &player1Strategy, storm::OptimizationDirection const &player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy)
 
template SymbolicGameProb01Result< storm::dd::DdType::CUDDperformProb1 (storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::CUDD, double > const &model, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::CUDD > const &phiStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &psiStates, storm::OptimizationDirection const &player1Strategy, storm::OptimizationDirection const &player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional< storm::dd::Bdd< storm::dd::DdType::CUDD > > const &player1Candidates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProbGreater0 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, boost::optional< uint_fast64_t > const &stepBound=boost::optional< uint_fast64_t >())
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbabilityGreater0)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01 (storm::models::symbolic::DeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvancomputeSchedulerProbGreater0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProbGreater0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb0A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProbGreater0A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbabilityGreater0A)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbabilityGreater0E)
 
template storm::dd::Bdd< storm::dd::DdType::SylvancomputeSchedulerProb1E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbability1E)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Max (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Max (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Min (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Min (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template SymbolicGameProb01Result< storm::dd::DdType::SylvanperformProb0 (storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::Sylvan > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::OptimizationDirection const &player1Strategy, storm::OptimizationDirection const &player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy)
 
template SymbolicGameProb01Result< storm::dd::DdType::SylvanperformProb1 (storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::Sylvan > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::OptimizationDirection const &player1Strategy, storm::OptimizationDirection const &player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional< storm::dd::Bdd< storm::dd::DdType::Sylvan > > const &player1Candidates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProbGreater0 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, boost::optional< uint_fast64_t > const &stepBound=boost::optional< uint_fast64_t >())
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbabilityGreater0)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01 (storm::models::symbolic::DeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvancomputeSchedulerProbGreater0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProbGreater0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb0A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProbGreater0A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbabilityGreater0A)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbabilityGreater0E)
 
template storm::dd::Bdd< storm::dd::DdType::SylvancomputeSchedulerProb1E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbability1E)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Max (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Max (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Min (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Min (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template SymbolicGameProb01Result< storm::dd::DdType::SylvanperformProb0 (storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::OptimizationDirection const &player1Strategy, storm::OptimizationDirection const &player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy)
 
template SymbolicGameProb01Result< storm::dd::DdType::SylvanperformProb1 (storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::Sylvan, storm::RationalNumber > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::OptimizationDirection const &player1Strategy, storm::OptimizationDirection const &player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional< storm::dd::Bdd< storm::dd::DdType::Sylvan > > const &player1Candidates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProbGreater0 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, boost::optional< uint_fast64_t > const &stepBound=boost::optional< uint_fast64_t >())
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbabilityGreater0)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01 (storm::models::symbolic::DeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01 (storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvancomputeSchedulerProbGreater0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProbGreater0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb0A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProbGreater0A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb0E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1A (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbabilityGreater0A)
 
template storm::dd::Bdd< storm::dd::DdType::SylvanperformProb1E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbabilityGreater0E)
 
template storm::dd::Bdd< storm::dd::DdType::SylvancomputeSchedulerProb1E (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &statesWithProbability1E)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Max (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Max (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Min (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > performProb01Min (storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &model, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitionMatrix, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &phiStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &psiStates)
 
template<typename T >
void computeSchedulerWithOneSuccessorInStates (storm::storage::BitVector const &states, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< T > &scheduler)
 Computes a scheduler for the given states that chooses an action that has at least one successor in the given set of states.
 

Function Documentation

◆ checkIfECWithChoiceExists() [1/2]

template bool storm::utility::graph::checkIfECWithChoiceExists ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  subsystem,
storm::storage::BitVector const &  choices 
)

◆ checkIfECWithChoiceExists() [2/2]

template<typename T >
bool storm::utility::graph::checkIfECWithChoiceExists ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  subsystem,
storm::storage::BitVector const &  choices 
)

Checks whether there is an End Component that.

  1. contains at least one of the specified choices and
  2. only contains states given by the specified subsystem.
Parameters
transitionMatrixthe transition matrix
backwardTransitionsThe reversed transition relation of the graph structure to search
subsystemthe subsystem which we consider
choicesthe choices which are to be checked

Definition at line 182 of file graph.cpp.

◆ computeSchedulerProb0E() [1/2]

template<typename T , typename SchedulerValueType >
void storm::utility::graph::computeSchedulerProb0E ( storm::storage::BitVector const &  prob0EStates,
storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::Scheduler< SchedulerValueType > &  scheduler 
)

Computes a scheduler for the given states that have a scheduler that has a probability 0.

Parameters
prob0EStatesThe states that have a scheduler achieving probablity 0.
transitionMatrixThe transition matrix of the system.
schedulerThe resulting scheduler for the prob0EStates States. The scheduler is not set at probGreater0A states.

Definition at line 593 of file graph.cpp.

◆ computeSchedulerProb0E() [2/2]

template void storm::utility::graph::computeSchedulerProb0E ( storm::storage::BitVector const &  prob0EStates,
storm::storage::SparseMatrix< double > const &  transitionMatrix,
storm::storage::Scheduler< double > &  scheduler 
)

◆ computeSchedulerProb1E() [1/7]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::computeSchedulerProb1E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  statesWithProbability1E 
)

◆ computeSchedulerProb1E() [2/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::computeSchedulerProb1E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbability1E 
)

◆ computeSchedulerProb1E() [3/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::computeSchedulerProb1E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbability1E 
)

◆ computeSchedulerProb1E() [4/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::computeSchedulerProb1E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbability1E 
)

◆ computeSchedulerProb1E() [5/7]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::computeSchedulerProb1E ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates,
storm::dd::Bdd< Type > const &  statesWithProbability1E 
)

Computes a scheduler satisfying phi until psi with probability 1.

Definition at line 1240 of file graph.cpp.

◆ computeSchedulerProb1E() [6/7]

template<typename T , typename SchedulerValueType >
void storm::utility::graph::computeSchedulerProb1E ( storm::storage::BitVector const &  prob1EStates,
storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
storm::storage::Scheduler< SchedulerValueType > &  scheduler,
boost::optional< storm::storage::BitVector > const &  rowFilter = boost::none 
)

Computes a scheduler for the given prob1EStates such that in the induced system the given psiStates are reached with probability 1.

Parameters
prob1EStatesThe states that have a scheduler achieving probablity 1.
transitionMatrixThe transition matrix of the system.
backwardTransitionsThe reversed transition relation.
phiStatesThe set of states satisfying phi.
psiStatesThe set of states satisfying psi.
schedulerThe resulting scheduler for the prob1EStates. The scheduler is not set at the remaining states.
rowFilterIf given, only scheduler choices within this filter are taken. This filter is ignored for the psiStates.

Definition at line 624 of file graph.cpp.

◆ computeSchedulerProb1E() [7/7]

template void storm::utility::graph::computeSchedulerProb1E ( storm::storage::BitVector const &  prob1EStates,
storm::storage::SparseMatrix< double > const &  transitionMatrix,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
storm::storage::Scheduler< double > &  scheduler,
boost::optional< storm::storage::BitVector > const &  rowFilter = boost::none 
)

◆ computeSchedulerProbGreater0E() [1/7]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::computeSchedulerProbGreater0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ computeSchedulerProbGreater0E() [2/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::computeSchedulerProbGreater0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ computeSchedulerProbGreater0E() [3/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::computeSchedulerProbGreater0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ computeSchedulerProbGreater0E() [4/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::computeSchedulerProbGreater0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ computeSchedulerProbGreater0E() [5/7]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::computeSchedulerProbGreater0E ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Computes a scheduler realizing a probability greater zero of satisfying phi until psi for all such states.

Definition at line 1102 of file graph.cpp.

◆ computeSchedulerProbGreater0E() [6/7]

template void storm::utility::graph::computeSchedulerProbGreater0E ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
storm::storage::Scheduler< double > &  scheduler,
boost::optional< storm::storage::BitVector > const &  rowFilter 
)

◆ computeSchedulerProbGreater0E() [7/7]

template<typename T , typename SchedulerValueType >
void storm::utility::graph::computeSchedulerProbGreater0E ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
storm::storage::Scheduler< SchedulerValueType > &  scheduler,
boost::optional< storm::storage::BitVector > const &  rowFilter = boost::none 
)

Computes a scheduler for the ProbGreater0E-States such that in the induced system the given psiStates are reachable via phiStates.

Parameters
transitionMatrixThe transition matrix of the system.
backwardTransitionsThe reversed transition relation.
phiStatesThe set of states satisfying phi.
psiStatesThe set of states satisfying psi.
rowFilterIf given, the returned scheduler will only pick choices such that rowFilter is true for the corresponding matrixrow.
schedulerThe resulting scheduler for the ProbGreater0E-States. The scheduler is not set at prob0A states.
Note
No choice is defined for ProbGreater0E-States if all the probGreater0-choices violate the row filter. This also holds for states that only reach psi via such states.

Definition at line 542 of file graph.cpp.

◆ computeSchedulerRewInf() [1/2]

template<typename T , typename SchedulerValueType >
void storm::utility::graph::computeSchedulerRewInf ( storm::storage::BitVector const &  rewInfStates,
storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::Scheduler< SchedulerValueType > &  scheduler 
)

Computes a scheduler for the given states that have a scheduler that has a reward infinity.

Parameters
rewInfStatesThe states that have a scheduler achieving reward infinity.
transitionMatrixThe transition matrix of the system.
backwardTransitionsThe reversed transition relation.
schedulerThe resulting scheduler for the rewInf States. The scheduler is not set at other states.

Definition at line 599 of file graph.cpp.

◆ computeSchedulerRewInf() [2/2]

template void storm::utility::graph::computeSchedulerRewInf ( storm::storage::BitVector const &  rewInfStates,
storm::storage::SparseMatrix< double > const &  transitionMatrix,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::Scheduler< double > &  scheduler 
)

◆ computeSchedulerStayingInStates()

template<typename T , typename SchedulerValueType >
void storm::utility::graph::computeSchedulerStayingInStates ( storm::storage::BitVector const &  states,
storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::Scheduler< SchedulerValueType > &  scheduler,
boost::optional< storm::storage::BitVector > const &  rowFilter = boost::none 
)

Computes a scheduler for the given states that chooses an action that stays completely in the very same set.

Note that this assumes that there is a legal choice for each of the states.

Parameters
statesThe set of states for which to compute the scheduler that stays in this very set.
transitionMatrixThe transition matrix.
schedulerThe resulting scheduler. The scheduler is only set at the given states.
rowFilterIf given, the returned scheduler will only pick choices such that rowFilter is true for the corresponding matrixrow.

Definition at line 490 of file graph.cpp.

◆ computeSchedulerWithOneSuccessorInStates() [1/2]

template<typename T , typename SchedulerValueType >
void storm::utility::graph::computeSchedulerWithOneSuccessorInStates ( storm::storage::BitVector const &  states,
storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::Scheduler< SchedulerValueType > &  scheduler 
)

Definition at line 515 of file graph.cpp.

◆ computeSchedulerWithOneSuccessorInStates() [2/2]

template<typename T >
void storm::utility::graph::computeSchedulerWithOneSuccessorInStates ( storm::storage::BitVector const &  states,
storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::Scheduler< T > &  scheduler 
)

Computes a scheduler for the given states that chooses an action that has at least one successor in the given set of states.

Note that this assumes that there is a legal choice for each of the states.

Parameters
statesThe set of states for which to compute the scheduler that chooses an action with a successor in this very set.
transitionMatrixThe transition matrix.
schedulerThe resulting scheduler. The scheduler is only set at the given states.

◆ getBFSSort()

template<typename T >
std::vector< uint_fast64_t > storm::utility::graph::getBFSSort ( storm::storage::SparseMatrix< T > const &  matrix,
std::vector< uint_fast64_t > const &  firstStates 
)

Definition at line 1827 of file graph.cpp.

◆ getBsccCover() [1/2]

template storm::storage::BitVector storm::utility::graph::getBsccCover ( storm::storage::SparseMatrix< double > const &  transitionMatrix)

◆ getBsccCover() [2/2]

template<typename T >
storm::storage::BitVector storm::utility::graph::getBsccCover ( storm::storage::SparseMatrix< T > const &  transitionMatrix)

Retrieves a set of states that covers als BSCCs of the system in the sense that for every BSCC exactly one state is included in the cover.

Parameters
transitionMatrixThe transition relation of the graph structure.

Definition at line 129 of file graph.cpp.

◆ getDistances() [1/2]

template std::vector< uint_fast64_t > storm::utility::graph::getDistances ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
storm::storage::BitVector const &  initialStates,
boost::optional< storm::storage::BitVector > const &  subsystem 
)

◆ getDistances() [2/2]

template<typename T >
std::vector< uint_fast64_t > storm::utility::graph::getDistances ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::BitVector const &  initialStates,
boost::optional< storm::storage::BitVector > const &  subsystem = boost::none 
)

Performs a breadth-first search through the underlying graph structure to compute the distance from all states to the starting states of the search.

Parameters
transitionMatrixThe transition relation of the graph structure to search.
initialStatesThe set of states from which to start the search.
subsystemThe subsystem to consider.
Returns
The distances of each state to the initial states of the sarch.

Definition at line 288 of file graph.cpp.

◆ getReachableOneStep()

template<typename T >
storm::storage::BitVector storm::utility::graph::getReachableOneStep ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::BitVector const &  initialStates 
)

Computes the states reachable in one step from the states indicated by the bitvector.

Assumes that no zero entries exist in the transition matrix.

Definition at line 36 of file graph.cpp.

◆ getReachableStates() [1/2]

template storm::storage::BitVector storm::utility::graph::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,
boost::optional< storm::storage::BitVector > const &  choiceFilter 
)

◆ getReachableStates() [2/2]

template<typename T >
storm::storage::BitVector storm::utility::graph::getReachableStates ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
storm::storage::BitVector const &  initialStates,
storm::storage::BitVector const &  constraintStates,
storm::storage::BitVector const &  targetStates,
bool  useStepBound = false,
uint_fast64_t  maximalSteps = 0,
boost::optional< storm::storage::BitVector > const &  choiceFilter = boost::none 
)

Performs a forward depth-first search through the underlying graph structure to identify the states that are reachable from the given set only passing through a constrained set of states until some target have been reached.

If an initial state or a (constrained-reachable) target state is not in the constrained set, it will be added to the reachable states but not explored.

Parameters
transitionMatrixThe transition relation of the graph structure to search.
initialStatesThe set of states from which to start the search.
constraintStatesThe set of states that must not be left.
targetStatesThe target states that may not be passed.
useStepBoundA flag that indicates whether or not to use the given number of maximal steps for the search.
maximalStepsThe maximal number of steps to reach the psi states.
choiceFilterIf given, only choices for which the bitvector is true are considered.

Definition at line 48 of file graph.cpp.

◆ getTopologicalSort() [1/2]

template std::vector< uint_fast64_t > storm::utility::graph::getTopologicalSort ( storm::storage::SparseMatrix< double > const &  matrix,
std::vector< uint64_t > const &  firstStates 
)

◆ getTopologicalSort() [2/2]

template<typename T >
std::vector< uint_fast64_t > storm::utility::graph::getTopologicalSort ( storm::storage::SparseMatrix< T > const &  matrix,
std::vector< uint64_t > const &  firstStates = {} 
)

Performs a topological sort of the states of the system according to the given transitions.

Parameters
matrixA square matrix representing the transition relation of the system.
Returns
A vector of indices that is a topological sort of the states.

Definition at line 1861 of file graph.cpp.

◆ hasCycle() [1/2]

template bool storm::utility::graph::hasCycle ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
boost::optional< storm::storage::BitVector > const &  subsystem 
)

◆ hasCycle() [2/2]

template<typename T >
bool storm::utility::graph::hasCycle ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
boost::optional< storm::storage::BitVector > const &  subsystem = boost::none 
)

Returns true if the graph represented by the given matrix has a cycle.

Parameters
transitionMatrix
subsystemif given, only states in the subsystem are considered for the check.

Definition at line 143 of file graph.cpp.

◆ performProb0() [1/6]

template SymbolicGameProb01Result< storm::dd::DdType::CUDD > storm::utility::graph::performProb0 ( storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates,
storm::OptimizationDirection const &  player1Strategy,
storm::OptimizationDirection const &  player2Strategy,
bool  producePlayer1Strategy,
bool  producePlayer2Strategy 
)

◆ performProb0() [2/6]

template SymbolicGameProb01Result< storm::dd::DdType::Sylvan > storm::utility::graph::performProb0 ( storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::Sylvan > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::OptimizationDirection const &  player1Strategy,
storm::OptimizationDirection const &  player2Strategy,
bool  producePlayer1Strategy,
bool  producePlayer2Strategy 
)

◆ performProb0() [3/6]

template SymbolicGameProb01Result< storm::dd::DdType::Sylvan > storm::utility::graph::performProb0 ( storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::OptimizationDirection const &  player1Strategy,
storm::OptimizationDirection const &  player2Strategy,
bool  producePlayer1Strategy,
bool  producePlayer2Strategy 
)

◆ performProb0() [4/6]

template<storm::dd::DdType Type, typename ValueType >
SymbolicGameProb01Result< Type > storm::utility::graph::performProb0 ( storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates,
storm::OptimizationDirection const &  player1Strategy,
storm::OptimizationDirection const &  player2Strategy,
bool  producePlayer1Strategy = false,
bool  producePlayer2Strategy = false 
)

Computes the set of states that have probability 0 given the strategies of the two players.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
producePlayer1StrategyA flag indicating whether the strategy of player 1 shall be produced.
producePlayer2StrategyA flag indicating whether the strategy of player 2 shall be produced.

Definition at line 1447 of file graph.cpp.

◆ performProb0() [5/6]

template ExplicitGameProb01Result storm::utility::graph::performProb0 ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
std::vector< uint64_t > const &  player1RowGrouping,
storm::storage::SparseMatrix< double > const &  player1BackwardTransitions,
std::vector< uint64_t > const &  player2BackwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
storm::OptimizationDirection const &  player1Direction,
storm::OptimizationDirection const &  player2Direction,
storm::storage::ExplicitGameStrategyPair strategyPair 
)

◆ performProb0() [6/6]

template<typename ValueType >
ExplicitGameProb01Result storm::utility::graph::performProb0 ( storm::storage::SparseMatrix< ValueType > const &  transitionMatrix,
std::vector< uint64_t > const &  player1Groups,
storm::storage::SparseMatrix< ValueType > const &  player1BackwardTransitions,
std::vector< uint64_t > const &  player2BackwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
storm::OptimizationDirection const &  player1Direction,
storm::OptimizationDirection const &  player2Direction,
storm::storage::ExplicitGameStrategyPair strategyPair = nullptr 
)

Computes the set of states that have probability 0 given the strategies of the two players.

Parameters
transitionMatrixThe transition matrix of the model as a BDD.
player1GroupsThe grouping of player 1 states (in terms of player 2 states).
player1BackwardTransitionsThe backward transitions (player 1 to player 2).
player2BackwardTransitionsThe backward transitions (player 2 to player 1).
phiStatesThe phi states of the model.
psiStatesThe psi states of the model.
player1DirectionThe optimization direction of player 1.
player2DirectionThe optimization direction of player 2.
strategyPairIf not null, player 1 and t2 strategies are synthesized and the corresponding choices are written to this strategy.

Definition at line 1308 of file graph.cpp.

◆ performProb01() [1/14]

template std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01 ( storm::models::sparse::DeterministicModel< double > const &  model,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb01() [2/14]

template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01 ( storm::models::sparse::DeterministicModel< T > const &  model,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.

Parameters
modelThe model whose graph structure to search.
phiStatesThe set of all states satisfying phi.
psiStatesThe set of all states satisfying psi.
Returns
A pair of bit vectors such that the first bit vector stores the indices of all states with probability 0 and the second stores all indices of states with probability 1.

Definition at line 400 of file graph.cpp.

◆ performProb01() [3/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > storm::utility::graph::performProb01 ( storm::models::symbolic::DeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProb01() [4/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01 ( storm::models::symbolic::DeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01() [5/14]

◆ performProb01() [6/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01 ( storm::models::symbolic::DeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01() [7/14]

template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > storm::utility::graph::performProb01 ( storm::models::symbolic::DeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.

Parameters
modelThe (symbolic) model for which to compute the set of states.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
Returns
A pair of BDDs that represent all states with probability 0 and 1, respectively.

Definition at line 466 of file graph.cpp.

◆ performProb01() [8/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > storm::utility::graph::performProb01 ( storm::models::symbolic::Model< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProb01() [9/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01() [10/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01() [11/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01() [12/14]

template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > storm::utility::graph::performProb01 ( storm::models::symbolic::Model< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.

Parameters
modelThe (symbolic) model for which to compute the set of states. This is used for retrieving the manager and information about the meta variables.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
Returns
A pair of BDDs that represent all states with probability 0 and 1, respectively.

Definition at line 478 of file graph.cpp.

◆ performProb01() [13/14]

template std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01 ( storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb01() [14/14]

template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01 ( storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.

Parameters
backwardTransitionsThe backward transitions of the model whose graph structure to search.
phiStatesThe set of all states satisfying phi.
psiStatesThe set of all states satisfying psi.
Returns
A pair of bit vectors such that the first bit vector stores the indices of all states with probability 0 and the second stores all indices of states with probability 1.

Definition at line 412 of file graph.cpp.

◆ performProb01Max() [1/14]

template std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01Max ( storm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > const &  model,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb01Max() [2/14]

template<typename T , typename RM >
std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01Max ( storm::models::sparse::NondeterministicModel< T, RM > const &  model,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a non-deterministic model in which all non-deterministic choices are resolved such that the probability is maximized.

Parameters
modelThe model whose graph structure to search.
phiStatesThe set of all states satisfying phi.
psiStatesThe set of all states satisfying psi.
Returns
A pair of bit vectors that represent all states with probability 0 and 1, respectively.

Definition at line 849 of file graph.cpp.

◆ performProb01Max() [3/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > storm::utility::graph::performProb01Max ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProb01Max() [4/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > storm::utility::graph::performProb01Max ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProb01Max() [5/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01Max ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01Max() [6/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01Max ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01Max() [7/14]

◆ performProb01Max() [8/14]

◆ performProb01Max() [9/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01Max ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01Max() [10/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01Max ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01Max() [11/14]

template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > storm::utility::graph::performProb01Max ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Definition at line 1276 of file graph.cpp.

◆ performProb01Max() [12/14]

template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > storm::utility::graph::performProb01Max ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Definition at line 1282 of file graph.cpp.

◆ performProb01Max() [13/14]

template std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01Max ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb01Max() [14/14]

template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01Max ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Definition at line 835 of file graph.cpp.

◆ performProb01Min() [1/14]

template std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01Min ( storm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > const &  model,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb01Min() [2/14]

template<typename T , typename RM >
std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01Min ( storm::models::sparse::NondeterministicModel< T, RM > const &  model,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a non-deterministic model in which all non-deterministic choices are resolved such that the probability is minimized.

Parameters
modelThe model whose graph structure to search.
phiStatesThe set of all states satisfying phi.
psiStatesThe set of all states satisfying psi.
Returns
A pair of bit vectors that represent all states with probability 0 and 1, respectively.

Definition at line 1094 of file graph.cpp.

◆ performProb01Min() [3/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > storm::utility::graph::performProb01Min ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProb01Min() [4/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::CUDD > > storm::utility::graph::performProb01Min ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProb01Min() [5/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01Min ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01Min() [6/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01Min ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01Min() [7/14]

◆ performProb01Min() [8/14]

◆ performProb01Min() [9/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01Min ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01Min() [10/14]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, storm::dd::Bdd< storm::dd::DdType::Sylvan > > storm::utility::graph::performProb01Min ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb01Min() [11/14]

template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > storm::utility::graph::performProb01Min ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Definition at line 1292 of file graph.cpp.

◆ performProb01Min() [12/14]

template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > > storm::utility::graph::performProb01Min ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Definition at line 1298 of file graph.cpp.

◆ performProb01Min() [13/14]

template std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01Min ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb01Min() [14/14]

template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::utility::graph::performProb01Min ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Definition at line 1079 of file graph.cpp.

◆ performProb0A() [1/7]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::performProb0A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProb0A() [2/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb0A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb0A() [3/7]

◆ performProb0A() [4/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb0A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb0A() [5/7]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::performProb0A ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Computes the set of states for which there does not exist a scheduler that achieves a probability greater than zero of satisfying phi until psi.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe phi states of the model.
psiStatesThe psi states of the model.
Returns
A BDD representing all such states.

Definition at line 1144 of file graph.cpp.

◆ performProb0A() [6/7]

template storm::storage::BitVector storm::utility::graph::performProb0A ( storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb0A() [7/7]

template<typename T >
storm::storage::BitVector storm::utility::graph::performProb0A ( storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Definition at line 749 of file graph.cpp.

◆ performProb0E() [1/9]

template storm::storage::BitVector storm::utility::graph::performProb0E ( storm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > const &  model,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb0E() [2/9]

template<typename T , typename RM >
storm::storage::BitVector storm::utility::graph::performProb0E ( storm::models::sparse::NondeterministicModel< T, RM > const &  model,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Computes the sets of states that have probability 0 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.

Stated differently, this means that these states have probability 0 of satisfying phi until psi if the scheduler tries to minimize this probability.

Parameters
modelThe model whose graph structure to search.
backwardTransitionsThe reversed transition relation of the model.
phiStatesThe set of all states satisfying phi.
psiStatesThe set of all states satisfying psi.
Returns
A bit vector that represents all states with probability 0.

Definition at line 976 of file graph.cpp.

◆ performProb0E() [3/9]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::performProb0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProb0E() [4/9]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb0E() [5/9]

◆ performProb0E() [6/9]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb0E() [7/9]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::performProb0E ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Computes the set of states for which there exists a scheduler that achieves probability zero of satisfying phi until psi.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
Returns
A BDD representing all such states.

Definition at line 1172 of file graph.cpp.

◆ performProb0E() [8/9]

template storm::storage::BitVector storm::utility::graph::performProb0E ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb0E() [9/9]

template<typename T >
storm::storage::BitVector storm::utility::graph::performProb0E ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Definition at line 986 of file graph.cpp.

◆ performProb1() [1/20]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::performProb1 ( storm::models::symbolic::Model< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProb1() [2/20]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::performProb1 ( storm::models::symbolic::Model< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  statesWithProbabilityGreater0 
)

◆ performProb1() [3/20]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb1() [4/20]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbabilityGreater0 
)

◆ performProb1() [5/20]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb1() [6/20]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbabilityGreater0 
)

◆ performProb1() [7/20]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProb1() [8/20]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbabilityGreater0 
)

◆ performProb1() [9/20]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::performProb1 ( storm::models::symbolic::Model< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Computes the set of states that have a probability of one of reaching psi states after only passing through phi states before.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
Returns
All states with probability 1.

Definition at line 459 of file graph.cpp.

◆ performProb1() [10/20]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::performProb1 ( storm::models::symbolic::Model< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates,
storm::dd::Bdd< Type > const &  statesWithProbabilityGreater0 
)

Computes the set of states that have a probability of one of reaching psi states after only passing through phi states before.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
statesWithProbabilityGreater0The set of states with a positive probability of satisfying phi until psi as a BDD.
Returns
All states with probability 1.

Definition at line 449 of file graph.cpp.

◆ performProb1() [11/20]

template SymbolicGameProb01Result< storm::dd::DdType::CUDD > storm::utility::graph::performProb1 ( storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates,
storm::OptimizationDirection const &  player1Strategy,
storm::OptimizationDirection const &  player2Strategy,
bool  producePlayer1Strategy,
bool  producePlayer2Strategy,
boost::optional< storm::dd::Bdd< storm::dd::DdType::CUDD > > const &  player1Candidates 
)

◆ performProb1() [12/20]

template SymbolicGameProb01Result< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1 ( storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::Sylvan > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::OptimizationDirection const &  player1Strategy,
storm::OptimizationDirection const &  player2Strategy,
bool  producePlayer1Strategy,
bool  producePlayer2Strategy,
boost::optional< storm::dd::Bdd< storm::dd::DdType::Sylvan > > const &  player1Candidates 
)

◆ performProb1() [13/20]

template SymbolicGameProb01Result< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1 ( storm::models::symbolic::StochasticTwoPlayerGame< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::OptimizationDirection const &  player1Strategy,
storm::OptimizationDirection const &  player2Strategy,
bool  producePlayer1Strategy,
bool  producePlayer2Strategy,
boost::optional< storm::dd::Bdd< storm::dd::DdType::Sylvan > > const &  player1Candidates 
)

◆ performProb1() [14/20]

template<storm::dd::DdType Type, typename ValueType >
SymbolicGameProb01Result< Type > storm::utility::graph::performProb1 ( storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates,
storm::OptimizationDirection const &  player1Strategy,
storm::OptimizationDirection const &  player2Strategy,
bool  producePlayer1Strategy = false,
bool  producePlayer2Strategy = false,
boost::optional< storm::dd::Bdd< Type > > const &  player1Candidates = boost::none 
)

Computes the set of states that have probability 1 given the strategies of the two players.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
producePlayer1StrategyA flag indicating whether the strategy of player 1 shall be produced.
producePlayer2StrategyA flag indicating whether the strategy of player 2 shall be produced.
player1CandidatesIf given, this set constrains the candidates of player 1 states that are considered.

Definition at line 1639 of file graph.cpp.

◆ performProb1() [15/20]

template storm::storage::BitVector storm::utility::graph::performProb1 ( storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb1() [16/20]

template storm::storage::BitVector storm::utility::graph::performProb1 ( storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
storm::storage::BitVector const &  statesWithProbabilityGreater0 
)

◆ performProb1() [17/20]

template ExplicitGameProb01Result storm::utility::graph::performProb1 ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
std::vector< uint64_t > const &  player1RowGrouping,
storm::storage::SparseMatrix< double > const &  player1BackwardTransitions,
std::vector< uint64_t > const &  player2BackwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
storm::OptimizationDirection const &  player1Direction,
storm::OptimizationDirection const &  player2Direction,
storm::storage::ExplicitGameStrategyPair strategyPair,
boost::optional< storm::storage::BitVector > const &  player1Candidates 
)

◆ performProb1() [18/20]

template<typename T >
storm::storage::BitVector storm::utility::graph::performProb1 ( storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Computes the set of states of the given model for which all paths lead to the given set of target states and only visit states from the filter set before.

In order to do this, it uses the given set of states that characterizes the states that possess at least one path to a target state. The results are written to the given bit vector.

Parameters
backwardTransitionsThe reversed transition relation of the graph structure to search.
phiStatesA bit vector of all states satisfying phi.
psiStatesA bit vector of all states satisfying psi.
Returns
A bit vector with all indices of states that have a probability greater than 1.

Definition at line 391 of file graph.cpp.

◆ performProb1() [19/20]

template<typename T >
storm::storage::BitVector storm::utility::graph::performProb1 ( storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
storm::storage::BitVector const &  statesWithProbabilityGreater0 
)

Computes the set of states of the given model for which all paths lead to the given set of target states and only visit states from the filter set before.

In order to do this, it uses the given set of states that characterizes the states that possess at least one path to a target state. The results are written to the given bit vector.

Parameters
backwardTransitionsThe reversed transition relation of the graph structure to search.
phiStatesA bit vector of all states satisfying phi.
psiStatesA bit vector of all states satisfying psi.
statesWithProbabilityGreater0A reference to a bit vector of states that possess a positive probability mass of satisfying phi until psi.
Returns
A bit vector with all indices of states that have a probability greater than 1.

Definition at line 383 of file graph.cpp.

◆ performProb1() [20/20]

template<typename ValueType >
ExplicitGameProb01Result storm::utility::graph::performProb1 ( storm::storage::SparseMatrix< ValueType > const &  transitionMatrix,
std::vector< uint64_t > const &  player1Groups,
storm::storage::SparseMatrix< ValueType > const &  player1BackwardTransitions,
std::vector< uint64_t > const &  player2BackwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
storm::OptimizationDirection const &  player1Direction,
storm::OptimizationDirection const &  player2Direction,
storm::storage::ExplicitGameStrategyPair strategyPair = nullptr,
boost::optional< storm::storage::BitVector > const &  player1Candidates = boost::none 
)

Computes the set of states that have probability 1 given the strategies of the two players.

Parameters
transitionMatrixThe transition matrix of the model as a BDD.
player1GroupsThe grouping of player 1 states (in terms of player 2 states).
player1BackwardTransitionsThe backward transitions (player 1 to player 2).
player2BackwardTransitionsThe backward transitions (player 2 to player 1).
phiStatesThe phi states of the model.
psiStatesThe psi states of the model.
player1DirectionThe optimization direction of player 1.
player2DirectionThe optimization direction of player 2.
strategyPairIf not null, player 1 and t2 strategies are synthesized and the corresponding choices are written to this strategy.
player1CandidatesIf given, this set constrains the candidates of player 1 states that are considered.

Definition at line 1516 of file graph.cpp.

◆ performProb1A() [1/9]

template storm::storage::BitVector storm::utility::graph::performProb1A ( storm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > const &  model,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb1A() [2/9]

template<typename T , typename RM >
storm::storage::BitVector storm::utility::graph::performProb1A ( storm::models::sparse::NondeterministicModel< T, RM > const &  model,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Computes the sets of states that have probability 1 of satisfying phi until psi under all possible resolutions of non-determinism in a non-deterministic model.

Stated differently, this means that these states have probability 1 of satisfying phi until psi even if the scheduler tries to minimize this probability.

Parameters
modelThe model whose graph structure to search.
backwardTransitionsThe reversed transition relation of the model.
phiStatesThe set of all states satisfying phi.
psiStatesThe set of all states satisfying psi.
Returns
A bit vector that represents all states with probability 0.

Definition at line 997 of file graph.cpp.

◆ performProb1A() [3/9]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::performProb1A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  statesWithProbabilityGreater0A 
)

◆ performProb1A() [4/9]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbabilityGreater0A 
)

◆ performProb1A() [5/9]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbabilityGreater0A 
)

◆ performProb1A() [6/9]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbabilityGreater0A 
)

◆ performProb1A() [7/9]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::performProb1A ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  psiStates,
storm::dd::Bdd< Type > const &  statesWithProbabilityGreater0A 
)

Computes the set of states for which all schedulers achieve probability one of satisfying phi until psi.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
statesWithProbabilityGreater0AThe states of the model that have a probability greater zero under all schedulers.
Returns
A BDD representing all such states.

Definition at line 1178 of file graph.cpp.

◆ performProb1A() [8/9]

template storm::storage::BitVector storm::utility::graph::performProb1A ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb1A() [9/9]

template<typename T >
storm::storage::BitVector storm::utility::graph::performProb1A ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Definition at line 1004 of file graph.cpp.

◆ performProb1E() [1/9]

template storm::storage::BitVector storm::utility::graph::performProb1E ( storm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > const &  model,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

◆ performProb1E() [2/9]

template<typename T , typename RM >
storm::storage::BitVector storm::utility::graph::performProb1E ( storm::models::sparse::NondeterministicModel< T, RM > const &  model,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates 
)

Computes the sets of states that have probability 1 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.

Stated differently, this means that these states have probability 1 of satisfying phi until psi if the scheduler tries to maximize this probability.

Parameters
modelThe model whose graph structure to search.
backwardTransitionsThe reversed transition relation of the model.
phiStatesThe set of all states satisfying phi.
psiStatesThe set of all states satisfying psi.
Returns
A bit vector that represents all states with probability 1.

Definition at line 828 of file graph.cpp.

◆ performProb1E() [3/9]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::performProb1E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  statesWithProbabilityGreater0E 
)

◆ performProb1E() [4/9]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbabilityGreater0E 
)

◆ performProb1E() [5/9]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbabilityGreater0E 
)

◆ performProb1E() [6/9]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb1E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  statesWithProbabilityGreater0E 
)

◆ performProb1E() [7/9]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::performProb1E ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates,
storm::dd::Bdd< Type > const &  statesWithProbabilityGreater0E 
)

Computes the set of states for which there exists a scheduler that achieves probability one of satisfying phi until psi.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
statesWithProbabilityGreater0EThe states of the model that have a scheduler that achieves a value greater than zero.
Returns
A BDD representing all such states.

Definition at line 1199 of file graph.cpp.

◆ performProb1E() [8/9]

template storm::storage::BitVector storm::utility::graph::performProb1E ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
boost::optional< storm::storage::BitVector > const &  choiceConstraint = boost::none 
)

◆ performProb1E() [9/9]

template<typename T >
storm::storage::BitVector storm::utility::graph::performProb1E ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
boost::optional< storm::storage::BitVector > const &  choiceConstraint = boost::none 
)

Computes the sets of states that have probability 1 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.

Stated differently, this means that these states have probability 1 of satisfying phi until psi if the scheduler tries to maximize this probability.

Parameters
modelThe model whose graph structure to search.
backwardTransitionsThe reversed transition relation of the model.
phiStatesThe set of all states satisfying phi.
psiStatesThe set of all states satisfying psi.
choiceConstraintIf given, only the selected choices are considered.
Returns
A bit vector that represents all states with probability 1.

Definition at line 757 of file graph.cpp.

◆ performProbGreater0() [1/7]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::performProbGreater0 ( storm::models::symbolic::Model< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates,
boost::optional< uint_fast64_t > const &  stepBound = boost::optional< uint_fast64_t >() 
)

◆ performProbGreater0() [2/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProbGreater0 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
boost::optional< uint_fast64_t > const &  stepBound = boost::optional< uint_fast64_t >() 
)

◆ performProbGreater0() [3/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProbGreater0 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
boost::optional< uint_fast64_t > const &  stepBound = boost::optional< uint_fast64_t >() 
)

◆ performProbGreater0() [4/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProbGreater0 ( storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates,
boost::optional< uint_fast64_t > const &  stepBound = boost::optional< uint_fast64_t >() 
)

◆ performProbGreater0() [5/7]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::performProbGreater0 ( storm::models::symbolic::Model< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates,
boost::optional< uint_fast64_t > const &  stepBound = boost::optional< uint_fast64_t >() 
)

Computes the set of states that has a positive probability of reaching psi states after only passing through phi states before.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
stepBoundIf given, this number indicates the maximal amount of steps allowed.
Returns
All states with positive probability.

Definition at line 423 of file graph.cpp.

◆ performProbGreater0() [6/7]

template storm::storage::BitVector storm::utility::graph::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 
)

◆ performProbGreater0() [7/7]

template<typename T >
storm::storage::BitVector storm::utility::graph::performProbGreater0 ( storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
bool  useStepBound = false,
uint_fast64_t  maximalSteps = 0 
)

Performs a backward depth-first search trough the underlying graph structure of the given model to determine which states of the model have a positive probability of satisfying phi until psi.

The resulting states are written to the given bit vector.

Parameters
backwardTransitionsThe reversed transition relation of the graph structure to search.
phiStatesA bit vector of all states satisfying phi.
psiStatesA bit vector of all states satisfying psi.
useStepBoundA flag that indicates whether or not to use the given number of maximal steps for the search.
maximalStepsThe maximal number of steps to reach the psi states.
Returns
A bit vector with all indices of states that have a probability greater than 0.

Definition at line 322 of file graph.cpp.

◆ performProbGreater0A() [1/7]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::performProbGreater0A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProbGreater0A() [2/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProbGreater0A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProbGreater0A() [3/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProbGreater0A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProbGreater0A() [4/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProbGreater0A ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProbGreater0A() [5/7]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::performProbGreater0A ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Computes the set of states for which all schedulers achieve a probability greater than zero of satisfying phi until psi.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
Returns
A BDD representing all such states.

Definition at line 1150 of file graph.cpp.

◆ performProbGreater0A() [6/7]

template storm::storage::BitVector storm::utility::graph::performProbGreater0A ( storm::storage::SparseMatrix< double > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
bool  useStepBound = false,
uint_fast64_t  maximalSteps = 0,
boost::optional< storm::storage::BitVector > const &  choiceConstraint = boost::none 
)

◆ performProbGreater0A() [7/7]

template<typename T >
storm::storage::BitVector storm::utility::graph::performProbGreater0A ( storm::storage::SparseMatrix< T > const &  transitionMatrix,
std::vector< uint_fast64_t > const &  nondeterministicChoiceIndices,
storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
bool  useStepBound = false,
uint_fast64_t  maximalSteps = 0,
boost::optional< storm::storage::BitVector > const &  choiceConstraint = boost::none 
)

Computes the sets of states that have probability greater 0 of satisfying phi until psi under any possible resolution of non-determinism in a non-deterministic model.

Stated differently, this means that these states have a probability greater 0 of satisfying phi until psi if the scheduler tries to maximize this probability.

Parameters
modelThe model whose graph structure to search.
backwardTransitionsThe reversed transition relation of the model.
phiStatesThe set of all states satisfying phi.
psiStatesThe set of all states satisfying psi.
useStepBoundA flag that indicates whether or not to use the given number of maximal steps for the search.
maximalStepsThe maximal number of steps to reach the psi states.
choiceConstraintIf set, we assume that only the specified choices exist in the model
Returns
A bit vector that represents all states with probability 0.

Definition at line 857 of file graph.cpp.

◆ performProbGreater0E() [1/7]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::graph::performProbGreater0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::CUDD, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::CUDD > const &  psiStates 
)

◆ performProbGreater0E() [2/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProbGreater0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, double > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProbGreater0E() [3/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProbGreater0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProbGreater0E() [4/7]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProbGreater0E ( storm::models::symbolic::NondeterministicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > const &  model,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  transitionMatrix,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  phiStates,
storm::dd::Bdd< storm::dd::DdType::Sylvan > const &  psiStates 
)

◆ performProbGreater0E() [5/7]

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type > storm::utility::graph::performProbGreater0E ( storm::models::symbolic::NondeterministicModel< Type, ValueType > const &  model,
storm::dd::Bdd< Type > const &  transitionMatrix,
storm::dd::Bdd< Type > const &  phiStates,
storm::dd::Bdd< Type > const &  psiStates 
)

Computes the set of states for which there exists a scheduler that achieves a probability greater than zero of satisfying phi until psi.

Parameters
modelThe (symbolic) model for which to compute the set of states.
transitionMatrixThe transition matrix of the model as a BDD.
phiStatesThe BDD containing all phi states of the model.
psiStatesThe BDD containing all psi states of the model.
Returns
A BDD representing all such states.

Definition at line 1123 of file graph.cpp.

◆ performProbGreater0E() [6/7]

template storm::storage::BitVector storm::utility::graph::performProbGreater0E ( storm::storage::SparseMatrix< double > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
bool  useStepBound = false,
uint_fast64_t  maximalSteps = 0 
)

◆ performProbGreater0E() [7/7]

template<typename T >
storm::storage::BitVector storm::utility::graph::performProbGreater0E ( storm::storage::SparseMatrix< T > const &  backwardTransitions,
storm::storage::BitVector const &  phiStates,
storm::storage::BitVector const &  psiStates,
bool  useStepBound = false,
uint_fast64_t  maximalSteps = 0 
)

Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.

Stated differently, this means that these states have a probability greater 0 of satisfying phi until psi if the scheduler tries to minimize this probability.

Parameters
backwardTransitionsThe reversed transition relation of the model.
phiStatesThe set of all states satisfying phi.
psiStatesThe set of all states satisfying psi.
useStepBoundA flag that indicates whether or not to use the given number of maximal steps for the search.
maximalStepsThe maximal number of steps to reach the psi states.
Returns
A bit vector that represents all states with probability 0.

Definition at line 689 of file graph.cpp.

◆ topologicalSortHelper()

template<typename T >
void storm::utility::graph::topologicalSortHelper ( storm::storage::SparseMatrix< T > const &  matrix,
uint64_t  state,
std::vector< uint_fast64_t > &  topologicalSort,
std::vector< uint_fast64_t > &  recursionStack,
std::vector< typename storm::storage::SparseMatrix< T >::const_iterator > &  iteratorRecursionStack,
storm::storage::BitVector visitedStates 
)

Definition at line 1778 of file graph.cpp.