Storm
A Modern Probabilistic Model Checker
|
#include "storm/transformer/ContinuousToDiscreteTimeModelTransformer.h"
#include "storm/transformer/NonMarkovianChainTransformer.h"
#include "storm/transformer/StatePermuter.h"
#include "storm/transformer/SymbolicToSparseTransformer.h"
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/utility/builder.h"
#include "storm/utility/macros.h"
#include "storm/utility/permutation.h"
Go to the source code of this file.
Namespaces | |
namespace | storm |
LabParser.cpp. | |
namespace | storm::api |
Functions | |
template<typename ValueType > | |
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > | storm::api::eliminateNonMarkovianChains (std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &ma, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::transformer::EliminationLabelBehavior labelBehavior) |
Eliminates chains of non-Markovian states from a given Markov Automaton. | |
template<typename ValueType > | |
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > | storm::api::transformContinuousToDiscreteTimeSparseModel (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas) |
Transforms the given continuous model to a discrete time model. | |
template<typename ValueType > | |
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > | storm::api::transformContinuousToDiscreteTimeSparseModel (storm::models::sparse::Model< ValueType > &&model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas) |
Transforms the given continuous model to a discrete time model IN PLACE. | |
template<typename ValueType > | |
std::shared_ptr< storm::logic::Formula const > | storm::api::checkAndTransformContinuousToDiscreteTimeFormula (storm::logic::Formula const &formula, std::string const &timeRewardName="_time") |
template<storm::dd::DdType Type, typename ValueType > | |
std::shared_ptr< storm::models::sparse::Model< ValueType > > | storm::api::transformSymbolicToSparseModel (std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &symbolicModel, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas=std::vector< std::shared_ptr< storm::logic::Formula const > >()) |
Transforms the given symbolic model to a sparse model. | |
template<typename ValueType > | |
std::shared_ptr< storm::models::sparse::Model< ValueType > > | storm::api::transformToNondeterministicModel (storm::models::sparse::Model< ValueType > &&model) |
template<typename ValueType > | |
std::shared_ptr< storm::models::sparse::Model< ValueType > > | storm::api::permuteModelStates (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::utility::permutation::OrderKind order, std::optional< uint64_t > seed=std::nullopt) |
Permutes the order of the states of the model according to the given order. | |