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