Loading...
Searching...
No Matches
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.
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) |
