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::BitVector >	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.
template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVector >	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.
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::BitVector >	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)
template<typename T , typename RM >
std::pair< storm::storage::BitVector, storm::storage::BitVector >	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.
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::BitVector >	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)
template<typename T , typename RM >
std::pair< storm::storage::BitVector, storm::storage::BitVector >	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.
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::BitVector >	performProb01 (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::BitVector >	performProb01 (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::BitVector >	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)
template std::pair< storm::storage::BitVector, storm::storage::BitVector >	performProb01Max (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::BitVector >	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)
template std::pair< storm::storage::BitVector, storm::storage::BitVector >	performProb01Min (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::CUDD >	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 >())
template storm::dd::Bdd< storm::dd::DdType::CUDD >	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)
template storm::dd::Bdd< storm::dd::DdType::CUDD >	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)
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::CUDD >	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)
template storm::dd::Bdd< storm::dd::DdType::CUDD >	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)
template storm::dd::Bdd< storm::dd::DdType::CUDD >	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)
template storm::dd::Bdd< storm::dd::DdType::CUDD >	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)
template storm::dd::Bdd< storm::dd::DdType::CUDD >	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)
template storm::dd::Bdd< storm::dd::DdType::CUDD >	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)
template storm::dd::Bdd< storm::dd::DdType::CUDD >	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)
template storm::dd::Bdd< storm::dd::DdType::CUDD >	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)
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::CUDD >	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)
template SymbolicGameProb01Result< storm::dd::DdType::CUDD >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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 >())
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
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::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
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::Sylvan >	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)
template SymbolicGameProb01Result< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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 >())
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
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::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
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::Sylvan >	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)
template SymbolicGameProb01Result< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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 >())
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
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::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	performProb0A (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::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	performProb0E (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::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	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)
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

transitionMatrix	the transition matrix
backwardTransitions	The reversed transition relation of the graph structure to search
subsystem	the subsystem which we consider
choices	the 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

prob0EStates	The states that have a scheduler achieving probablity 0.
transitionMatrix	The transition matrix of the system.
scheduler	The 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

prob1EStates	The states that have a scheduler achieving probablity 1.
transitionMatrix	The transition matrix of the system.
backwardTransitions	The reversed transition relation.
phiStates	The set of states satisfying phi.
psiStates	The set of states satisfying psi.
scheduler	The resulting scheduler for the prob1EStates. The scheduler is not set at the remaining states.
rowFilter	If 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

transitionMatrix	The transition matrix of the system.
backwardTransitions	The reversed transition relation.
phiStates	The set of states satisfying phi.
psiStates	The set of states satisfying psi.
rowFilter	If given, the returned scheduler will only pick choices such that rowFilter is true for the corresponding matrixrow.
scheduler	The 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

rewInfStates	The states that have a scheduler achieving reward infinity.
transitionMatrix	The transition matrix of the system.
backwardTransitions	The reversed transition relation.
scheduler	The 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

states	The set of states for which to compute the scheduler that stays in this very set.
transitionMatrix	The transition matrix.
scheduler	The resulting scheduler. The scheduler is only set at the given states.
rowFilter	If 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

states	The set of states for which to compute the scheduler that chooses an action with a successor in this very set.
transitionMatrix	The transition matrix.
scheduler	The 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

transitionMatrix

The 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

transitionMatrix	The transition relation of the graph structure to search.
initialStates	The set of states from which to start the search.
subsystem	The 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

transitionMatrix	The transition relation of the graph structure to search.
initialStates	The set of states from which to start the search.
constraintStates	The set of states that must not be left.
targetStates	The target states that may not be passed.
useStepBound	A flag that indicates whether or not to use the given number of maximal steps for the search.
maximalSteps	The maximal number of steps to reach the psi states.
choiceFilter	If 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

matrix

A 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
subsystem	if 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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The BDD containing all phi states of the model.
psiStates	The BDD containing all psi states of the model.
producePlayer1Strategy	A flag indicating whether the strategy of player 1 shall be produced.
producePlayer2Strategy	A 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

transitionMatrix	The transition matrix of the model as a BDD.
player1Groups	The grouping of player 1 states (in terms of player 2 states).
player1BackwardTransitions	The backward transitions (player 1 to player 2).
player2BackwardTransitions	The backward transitions (player 2 to player 1).
phiStates	The phi states of the model.
psiStates	The psi states of the model.
player1Direction	The optimization direction of player 1.
player2Direction	The optimization direction of player 2.
strategyPair	If 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

model	The model whose graph structure to search.
phiStates	The set of all states satisfying phi.
psiStates	The 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]

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::RationalFunction > const &	model,
		storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	phiStates,
		storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	psiStates
	)

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

model	The (symbolic) model for which to compute the set of states.
phiStates	The BDD containing all phi states of the model.
psiStates	The 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

model	The (symbolic) model for which to compute the set of states. This is used for retrieving the manager and information about the meta variables.
phiStates	The BDD containing all phi states of the model.
psiStates	The 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

backwardTransitions	The backward transitions of the model whose graph structure to search.
phiStates	The set of all states satisfying phi.
psiStates	The 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

model	The model whose graph structure to search.
phiStates	The set of all states satisfying phi.
psiStates	The 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]

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::RationalFunction > const &	model,
		storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	phiStates,
		storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	psiStates
	)

performProb01Max() [8/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::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
	)

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

model	The model whose graph structure to search.
phiStates	The set of all states satisfying phi.
psiStates	The 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]

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::RationalFunction > const &	model,
		storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	phiStates,
		storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	psiStates
	)

performProb01Min() [8/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::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
	)

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]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb0A	(	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
	)

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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The phi states of the model.
psiStates	The 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

model	The model whose graph structure to search.
backwardTransitions	The reversed transition relation of the model.
phiStates	The set of all states satisfying phi.
psiStates	The 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]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::graph::performProb0E	(	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
	)

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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The BDD containing all phi states of the model.
psiStates	The 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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The BDD containing all phi states of the model.
psiStates	The 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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The BDD containing all phi states of the model.
psiStates	The BDD containing all psi states of the model.
statesWithProbabilityGreater0	The 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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The BDD containing all phi states of the model.
psiStates	The BDD containing all psi states of the model.
producePlayer1Strategy	A flag indicating whether the strategy of player 1 shall be produced.
producePlayer2Strategy	A flag indicating whether the strategy of player 2 shall be produced.
player1Candidates	If 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

backwardTransitions	The reversed transition relation of the graph structure to search.
phiStates	A bit vector of all states satisfying phi.
psiStates	A 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

backwardTransitions	The reversed transition relation of the graph structure to search.
phiStates	A bit vector of all states satisfying phi.
psiStates	A bit vector of all states satisfying psi.
statesWithProbabilityGreater0	A 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

transitionMatrix	The transition matrix of the model as a BDD.
player1Groups	The grouping of player 1 states (in terms of player 2 states).
player1BackwardTransitions	The backward transitions (player 1 to player 2).
player2BackwardTransitions	The backward transitions (player 2 to player 1).
phiStates	The phi states of the model.
psiStates	The psi states of the model.
player1Direction	The optimization direction of player 1.
player2Direction	The optimization direction of player 2.
strategyPair	If not null, player 1 and t2 strategies are synthesized and the corresponding choices are written to this strategy.
player1Candidates	If 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

model	The model whose graph structure to search.
backwardTransitions	The reversed transition relation of the model.
phiStates	The set of all states satisfying phi.
psiStates	The 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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The BDD containing all phi states of the model.
psiStates	The BDD containing all psi states of the model.
statesWithProbabilityGreater0A	The 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

model	The model whose graph structure to search.
backwardTransitions	The reversed transition relation of the model.
phiStates	The set of all states satisfying phi.
psiStates	The 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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The BDD containing all phi states of the model.
psiStates	The BDD containing all psi states of the model.
statesWithProbabilityGreater0E	The 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

model	The model whose graph structure to search.
backwardTransitions	The reversed transition relation of the model.
phiStates	The set of all states satisfying phi.
psiStates	The set of all states satisfying psi.
choiceConstraint	If 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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The BDD containing all phi states of the model.
psiStates	The BDD containing all psi states of the model.
stepBound	If 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

backwardTransitions	The reversed transition relation of the graph structure to search.
phiStates	A bit vector of all states satisfying phi.
psiStates	A bit vector of all states satisfying psi.
useStepBound	A flag that indicates whether or not to use the given number of maximal steps for the search.
maximalSteps	The 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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The BDD containing all phi states of the model.
psiStates	The 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

model	The model whose graph structure to search.
backwardTransitions	The reversed transition relation of the model.
phiStates	The set of all states satisfying phi.
psiStates	The set of all states satisfying psi.
useStepBound	A flag that indicates whether or not to use the given number of maximal steps for the search.
maximalSteps	The maximal number of steps to reach the psi states.
choiceConstraint	If 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

model	The (symbolic) model for which to compute the set of states.
transitionMatrix	The transition matrix of the model as a BDD.
phiStates	The BDD containing all phi states of the model.
psiStates	The 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

backwardTransitions	The reversed transition relation of the model.
phiStates	The set of all states satisfying phi.
psiStates	The set of all states satisfying psi.
useStepBound	A flag that indicates whether or not to use the given number of maximal steps for the search.
maximalSteps	The 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.