storm::modelchecker::multiobjective::preprocessing Namespace Reference

Classes
class	SparseMultiObjectivePreprocessor
struct	SparseMultiObjectivePreprocessorResult
class	SparseMultiObjectiveRewardAnalysis

Enumerations
enum class	RewardFinitenessType { AllFinite , ExistsParetoFinite , Infinite }

Functions
template<typename SparseModelType >
storm::storage::BitVector	getOnlyReachableViaPhi (SparseModelType const &model, storm::storage::BitVector const &phi)
storm::logic::OperatorInformation	getOperatorInformation (storm::logic::OperatorFormula const &formula, bool considerComplementaryEvent)

Enumeration Type Documentation

RewardFinitenessType

enum class storm::modelchecker::multiobjective::preprocessing::RewardFinitenessType

strong

Enumerator
AllFinite
ExistsParetoFinite
Infinite

Definition at line 17 of file SparseMultiObjectiveRewardAnalysis.h.

Function Documentation

getOnlyReachableViaPhi()

template<typename SparseModelType >

storm::storage::BitVector storm::modelchecker::multiobjective::preprocessing::getOnlyReachableViaPhi	(	SparseModelType const &	model,
		storm::storage::BitVector const &	phi
	)

Definition at line 86 of file SparseMultiObjectivePreprocessor.cpp.

getOperatorInformation()

storm::logic::OperatorInformation storm::modelchecker::multiobjective::preprocessing::getOperatorInformation	(	storm::logic::OperatorFormula const &	formula,
		bool	considerComplementaryEvent
	)

Definition at line 257 of file SparseMultiObjectivePreprocessor.cpp.