Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
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

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.