storm::ps::SmtPermissiveSchedulerComputation< RM > Class Template Reference

#include <SmtBasedPermissiveSchedulers.h>

Inheritance diagram for storm::ps::SmtPermissiveSchedulerComputation< RM >:

Collaboration diagram for storm::ps::SmtPermissiveSchedulerComputation< RM >:

Public Member Functions
	SmtPermissiveSchedulerComputation (storm::solver::SmtSolver &smtSolver, storm::models::sparse::Mdp< double, RM > const &mdp, storm::storage::BitVector const &goalstates, storm::storage::BitVector const &sinkstates)
void	calculatePermissiveScheduler (bool lowerBound, double boundary) override
bool	foundSolution () const override
SubMDPPermissiveScheduler< RM >	getScheduler () const override
Public Member Functions inherited from storm::ps::PermissiveSchedulerComputation< RM >
	PermissiveSchedulerComputation (storm::models::sparse::Mdp< double, RM > const &mdp, storm::storage::BitVector const &goalstates, storm::storage::BitVector const &sinkstates)
virtual	~PermissiveSchedulerComputation ()=default
void	setPenalties (PermissiveSchedulerPenalties penalties)
PermissiveSchedulerPenalties const &	getPenalties () const
PermissiveSchedulerPenalties &	getPenalties ()

Additional Inherited Members
Protected Attributes inherited from storm::ps::PermissiveSchedulerComputation< RM >
storm::models::sparse::Mdp< double, RM > const &	mdp
storm::storage::BitVector const &	mGoals
storm::storage::BitVector const &	mSinks
PermissiveSchedulerPenalties	mPenalties

Detailed Description

template<typename RM>
class storm::ps::SmtPermissiveSchedulerComputation< RM >

Definition at line 9 of file SmtBasedPermissiveSchedulers.h.

Constructor & Destructor Documentation

SmtPermissiveSchedulerComputation()

template<typename RM >

storm::ps::SmtPermissiveSchedulerComputation< RM >::SmtPermissiveSchedulerComputation ( storm::solver::SmtSolver &  smtSolver, storm::models::sparse::Mdp< double, RM > const &  mdp, storm::storage::BitVector const &  goalstates, storm::storage::BitVector const &  sinkstates  )

inline

Definition at line 23 of file SmtBasedPermissiveSchedulers.h.

Member Function Documentation

calculatePermissiveScheduler()

template<typename RM >

void storm::ps::SmtPermissiveSchedulerComputation< RM >::calculatePermissiveScheduler ( bool  lowerBound, double  boundary  )

inlineoverridevirtual

Implements storm::ps::PermissiveSchedulerComputation< RM >.

Definition at line 31 of file SmtBasedPermissiveSchedulers.h.

foundSolution()

template<typename RM >

bool storm::ps::SmtPermissiveSchedulerComputation< RM >::foundSolution ( ) const

inlineoverridevirtual

Implements storm::ps::PermissiveSchedulerComputation< RM >.

Definition at line 36 of file SmtBasedPermissiveSchedulers.h.

getScheduler()

template<typename RM >

SubMDPPermissiveScheduler< RM > storm::ps::SmtPermissiveSchedulerComputation< RM >::getScheduler ( ) const

inlineoverridevirtual

Implements storm::ps::PermissiveSchedulerComputation< RM >.

Definition at line 41 of file SmtBasedPermissiveSchedulers.h.

---

The documentation for this class was generated from the following file:

• src/storm-permissive/analysis/SmtBasedPermissiveSchedulers.h