diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 35d2e1d92..5fcf85253 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -32,6 +32,7 @@ file(GLOB_RECURSE STORM_PERMISSIVESCHEDULER_FILES ${PROJECT_SOURCE_DIR}/src/perm file(GLOB STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp) file(GLOB_RECURSE STORM_MODELS_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/models/sparse/*.h ${PROJECT_SOURCE_DIR}/src/models/sparse/*.cpp) file(GLOB_RECURSE STORM_MODELS_SYMBOLIC_FILES ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.h ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.cpp) +file(GLOB_RECURSE STORM_MODELTRANSFORMER_FILES ${PROJECT_SOURCE_DIR}/src/modeltransformer/*.h ${PROJECT_SOURCE_DIR}/src/modeltransformer/*.cpp) file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) file(GLOB STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp) @@ -88,6 +89,7 @@ source_group(permissiveschedulers FILES ${STORM_PERMISSIVESCHEDULER_FILES}) source_group(models FILES ${STORM_MODELS_FILES}) source_group(models\\sparse FILES ${STORM_MODELS_SPARSE_FILES}) source_group(models\\symbolic FILES ${STORM_MODELS_SYMBOLIC_FILES}) +source_group(modeltransformer FILES ${STORM_MODELTRANSFORMER_FILES}) source_group(parser FILES ${STORM_PARSER_FILES}) source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) source_group(settings FILES ${STORM_SETTINGS_FILES}) diff --git a/src/modeltransformers/StateDuplicator.h b/src/modeltransformers/StateDuplicator.h new file mode 100644 index 000000000..f96e0f9c6 --- /dev/null +++ b/src/modeltransformers/StateDuplicator.h @@ -0,0 +1,204 @@ +#ifndef STORM_MDPTRIVIALSTATEELIMINATOR_H +#define STORM_MDPTRIVIALSTATEELIMINATOR_H + +#include "../utility/macros.h" + +#include +#include +#include + +#include "src/adapters/CarlAdapter.h" +#include "src/logic/Formulas.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/region/RegionCheckResult.h" +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "src/models/sparse/StandardRewardModel.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/RegionSettings.h" +#include "src/solver/OptimizationDirection.h" +#include "src/storage/sparse/StateType.h" +#include "src/storage/FlexibleSparseMatrix.h" +#include "src/utility/constants.h" +#include "src/utility/graph.h" +#include "src/utility/macros.h" +#include "src/utility/vector.h" + +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/InvalidPropertyException.h" +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidSettingsException.h" +#include "src/exceptions/NotImplementedException.h" +#include "src/exceptions/UnexpectedException.h" +#include "src/exceptions/NotSupportedException.h" +#include "src/logic/FragmentSpecification.h" + +namespace storm { + namespace transformer { + + /* + * Duplicates the state space of the given model and redirects the incoming transitions of gateStates of the first copy to the gateStates of the second copy. + * Only states reachable from the initial states are kept. + */ +