DdJaniModelBuilder.cpp File Reference

#include "storm/builder/DdJaniModelBuilder.h"
#include <sstream>
#include <boost/algorithm/string/join.hpp>
#include "storm/logic/Formulas.h"
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/storage/jani/Automaton.h"
#include "storm/storage/jani/AutomatonComposition.h"
#include "storm/storage/jani/Edge.h"
#include "storm/storage/jani/EdgeDestination.h"
#include "storm/storage/jani/Location.h"
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/ParallelComposition.h"
#include "storm/storage/jani/Variable.h"
#include "storm/storage/jani/eliminator/ArrayEliminator.h"
#include "storm/storage/jani/types/AllJaniTypes.h"
#include "storm/storage/jani/visitor/CompositionInformationVisitor.h"
#include "storm/adapters/AddExpressionAdapter.h"
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/models/symbolic/Ctmc.h"
#include "storm/models/symbolic/Dtmc.h"
#include "storm/models/symbolic/MarkovAutomaton.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/BuildSettings.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/WrongFormatException.h"
#include "storm/utility/dd.h"
#include "storm/utility/jani.h"
#include "storm/utility/macros.h"
#include "storm/utility/math.h"
#include "storm/adapters/RationalFunctionAdapter.h"

Include dependency graph for DdJaniModelBuilder.cpp:

Go to the source code of this file.

Classes
class	storm::builder::ParameterCreator< Type, ValueType >
class	storm::builder::ParameterCreator< Type, storm::RationalFunction >
struct	storm::builder::CompositionVariables< Type, ValueType >
class	storm::builder::CompositionVariableCreator< Type, ValueType >
struct	storm::builder::ComposerResult< Type, ValueType >
class	storm::builder::SystemComposer< Type, ValueType >
struct	storm::builder::EdgeDestinationDd< Type, ValueType >
class	storm::builder::CombinedEdgesSystemComposer< Type, ValueType >
struct	storm::builder::CombinedEdgesSystemComposer< Type, ValueType >::EdgeDd
struct	storm::builder::CombinedEdgesSystemComposer< Type, ValueType >::ActionDd
struct	storm::builder::CombinedEdgesSystemComposer< Type, ValueType >::ActionIdentification
struct	storm::builder::CombinedEdgesSystemComposer< Type, ValueType >::ActionIdentificationHash
struct	storm::builder::CombinedEdgesSystemComposer< Type, ValueType >::AutomatonDd
struct	storm::builder::CombinedEdgesSystemComposer< Type, ValueType >::ActionInstantiation
struct	storm::builder::CombinedEdgesSystemComposer< Type, ValueType >::ActionInstantiationHash
struct	storm::builder::ModelComponents< Type, ValueType >

Namespaces
namespace	storm
	LabParser.cpp.
namespace	storm::builder

Functions
template<storm::dd::DdType Type, typename ValueType >
EdgeDestinationDd< Type, ValueType >	storm::builder::buildEdgeDestinationDd (storm::jani::Automaton const &automaton, storm::jani::EdgeDestination const &destination, storm::dd::Bdd< Type > const &guard, CompositionVariables< Type, ValueType > const &variables)
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Add< Type, ValueType >	storm::builder::encodeAction (boost::optional< uint64_t > const &actionIndex, boost::optional< bool > const &markovian, CompositionVariables< Type, ValueType > const &variables)
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Add< Type, ValueType >	storm::builder::encodeIndex (uint64_t index, uint64_t localNondeterminismVariableOffset, uint64_t numberOfLocalNondeterminismVariables, CompositionVariables< Type, ValueType > const &variables)
template<storm::dd::DdType Type, typename ValueType >
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > >	storm::builder::createModel (storm::jani::ModelType const &modelType, CompositionVariables< Type, ValueType > const &variables, ModelComponents< Type, ValueType > const &modelComponents)
template<storm::dd::DdType Type, typename ValueType >
void	storm::builder::postprocessVariables (storm::jani::ModelType const &modelType, ComposerResult< Type, ValueType > &system, CompositionVariables< Type, ValueType > &variables)
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::builder::postprocessSystem (storm::jani::Model const &model, ComposerResult< Type, ValueType > &system, CompositionVariables< Type, ValueType > const &variables, typename DdJaniModelBuilder< Type, ValueType >::Options const &options, std::map< std::string, storm::expressions::Expression > const &labelsToExpressionMap)
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::builder::computeInitialStates (storm::jani::Model const &model, CompositionVariables< Type, ValueType > const &variables)
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::builder::fixDeadlocks (storm::jani::ModelType const &modelType, storm::dd::Add< Type, ValueType > &transitionMatrix, storm::dd::Bdd< Type > const &transitionMatrixBdd, storm::dd::Bdd< Type > const &reachableStates, CompositionVariables< Type, ValueType > const &variables)
template<storm::dd::DdType Type, typename ValueType >
std::vector< storm::expressions::Variable >	storm::builder::selectRewardVariables (storm::jani::Model const &model, typename DdJaniModelBuilder< Type, ValueType >::Options const &options)
template<storm::dd::DdType Type, typename ValueType >
std::unordered_map< std::string, storm::models::symbolic::StandardRewardModel< Type, ValueType > >	storm::builder::buildRewardModels (storm::dd::Add< Type, ValueType > const &reachableStates, storm::dd::Add< Type, ValueType > const &transitionMatrix, storm::jani::ModelType const &modelType, CompositionVariables< Type, ValueType > const &variables, ComposerResult< Type, ValueType > const &system, std::vector< storm::expressions::Variable > const &rewardVariables)
template<storm::dd::DdType Type, typename ValueType >
std::map< std::string, storm::expressions::Expression >	storm::builder::buildLabelExpressions (storm::jani::Model const &model, CompositionVariables< Type, ValueType > const &variables, typename DdJaniModelBuilder< Type, ValueType >::Options const &options)
template<storm::dd::DdType Type, typename ValueType >
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > >	storm::builder::buildInternal (storm::jani::Model const &model, typename DdJaniModelBuilder< Type, ValueType >::Options const &options, std::shared_ptr< storm::dd::DdManager< Type > > const &manager)