transformation.h File Reference

#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"

Include dependency graph for transformation.h:

This graph shows which files directly or indirectly include this file:

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.