Storm
A Modern Probabilistic Model Checker
|
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) |
|
strong |
Enumerator | |
---|---|
AllFinite | |
ExistsParetoFinite | |
Infinite |
Definition at line 17 of file SparseMultiObjectiveRewardAnalysis.h.
storm::storage::BitVector storm::modelchecker::multiobjective::preprocessing::getOnlyReachableViaPhi | ( | SparseModelType const & | model, |
storm::storage::BitVector const & | phi | ||
) |
Definition at line 86 of file SparseMultiObjectivePreprocessor.cpp.
storm::logic::OperatorInformation storm::modelchecker::multiobjective::preprocessing::getOperatorInformation | ( | storm::logic::OperatorFormula const & | formula, |
bool | considerComplementaryEvent | ||
) |
Definition at line 257 of file SparseMultiObjectivePreprocessor.cpp.