storm::ps Namespace Reference

Classes
class	MilpPermissiveSchedulerComputation
class	PermissiveScheduler
class	PermissiveSchedulerComputation
class	PermissiveSchedulerPenalties
class	SmtPermissiveSchedulerComputation
class	SubMDPPermissiveScheduler

Functions
template<typename RM >
boost::optional< SubMDPPermissiveScheduler< RM > >	computePermissiveSchedulerViaMILP (storm::models::sparse::Mdp< double, RM > const &mdp, storm::logic::ProbabilityOperatorFormula const &safeProp)
template<typename RM >
boost::optional< SubMDPPermissiveScheduler< RM > >	computePermissiveSchedulerViaSMT (storm::models::sparse::Mdp< double, RM > const &mdp, storm::logic::ProbabilityOperatorFormula const &safeProp)
template boost::optional< SubMDPPermissiveScheduler<> >	computePermissiveSchedulerViaMILP (storm::models::sparse::Mdp< double > const &mdp, storm::logic::ProbabilityOperatorFormula const &safeProp)
template boost::optional< SubMDPPermissiveScheduler<> >	computePermissiveSchedulerViaSMT (storm::models::sparse::Mdp< double > const &mdp, storm::logic::ProbabilityOperatorFormula const &safeProp)

Function Documentation

computePermissiveSchedulerViaMILP() [1/2]

template boost::optional< SubMDPPermissiveScheduler<> > storm::ps::computePermissiveSchedulerViaMILP	(	storm::models::sparse::Mdp< double > const &	mdp,
		storm::logic::ProbabilityOperatorFormula const &	safeProp
	)

computePermissiveSchedulerViaMILP() [2/2]

template<typename RM >

boost::optional< SubMDPPermissiveScheduler< RM > > storm::ps::computePermissiveSchedulerViaMILP	(	storm::models::sparse::Mdp< double, RM > const &	mdp,
		storm::logic::ProbabilityOperatorFormula const &	safeProp
	)

Definition at line 18 of file PermissiveSchedulers.cpp.

computePermissiveSchedulerViaSMT() [1/2]

template boost::optional< SubMDPPermissiveScheduler<> > storm::ps::computePermissiveSchedulerViaSMT	(	storm::models::sparse::Mdp< double > const &	mdp,
		storm::logic::ProbabilityOperatorFormula const &	safeProp
	)

computePermissiveSchedulerViaSMT() [2/2]

template<typename RM >

boost::optional< SubMDPPermissiveScheduler< RM > > storm::ps::computePermissiveSchedulerViaSMT	(	storm::models::sparse::Mdp< double, RM > const &	mdp,
		storm::logic::ProbabilityOperatorFormula const &	safeProp
	)

Definition at line 43 of file PermissiveSchedulers.cpp.