commit to switch workplace

CMakeLists.txt

@@ -77,6 +77,8 @@ message("CMAKE_INSTALL_DIR: ${CMAKE_INSTALL_DIR}")
 if (STORM_DEVELOPER)
     set(CMAKE_BUILD_TYPE "DEBUG")
     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DSTORM_DEV")
+else()
+    set(STORM_LOG_DISABLE_DEBUG ON)
 endif()
 message(STATUS "Storm - Building ${CMAKE_BUILD_TYPE} version.")
 

src/storm-gspn-cli/storm-gspn.cpp

@@ -31,6 +31,7 @@
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm/settings/modules/JaniExportSettings.h"
+#include "storm/settings/modules/ResourceSettings.h"
 
 /*!
  * Initialize the settings manager.
@@ -45,6 +46,7 @@ void initializeSettings() {
     storm::settings::addModule<storm::settings::modules::CoreSettings>();
     storm::settings::addModule<storm::settings::modules::DebugSettings>();
     storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
+    storm::settings::addModule<storm::settings::modules::ResourceSettings>();
 }
 
 

src/storm/builder/DdPrismModelBuilder.cpp

@@ -470,7 +470,7 @@ namespace storm {
         };
         
         template <storm::dd::DdType Type, typename ValueType>
-        DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), buildAllLabels(true), labelsToBuild(), terminalStates(), negatedTerminalStates() {
+        DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
             // Intentionally left empty.
         }
         
@@ -482,10 +482,6 @@ namespace storm {
         
         template <storm::dd::DdType Type, typename ValueType>
         DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
-            if (formulas.empty()) {
-                this->buildAllRewardModels = true;
-                this->buildAllLabels = true;
-            } else {
             for (auto const& formula : formulas) {
                 this->preserveFormula(*formula);
             }
@@ -493,7 +489,6 @@ namespace storm {
                 this->setTerminalStatesFromFormula(*formulas.front());
             }
         }
-        }
         
         template <storm::dd::DdType Type, typename ValueType>
         void DdPrismModelBuilder<Type, ValueType>::Options::preserveFormula(storm::logic::Formula const& formula) {
@@ -553,13 +548,13 @@ namespace storm {
         
         template <storm::dd::DdType Type, typename ValueType>
         struct DdPrismModelBuilder<Type, ValueType>::SystemResult {
-            SystemResult(storm::dd::Add<Type, ValueType> const& allTransitionsDd, DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) {
+            SystemResult(storm::dd::Add<Type, ValueType> const& allTransitionsDd, DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram const& globalModule, boost::optional<storm::dd::Add<Type, ValueType>> const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) {
                 // Intentionally left empty.
             }
             
             storm::dd::Add<Type, ValueType> allTransitionsDd;
             typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram globalModule;
-            storm::dd::Add<Type, ValueType> stateActionDd;
+            boost::optional<storm::dd::Add<Type, ValueType>> stateActionDd;
         };
         
         template <storm::dd::DdType Type, typename ValueType>
@@ -1089,11 +1084,12 @@ namespace storm {
             storm::dd::Add<Type, ValueType> result = createSystemFromModule(generationInfo, system);
 
             // Create an auxiliary DD that is used later during the construction of reward models.
-            storm::dd::Add<Type, ValueType> stateActionDd = result.sumAbstract(generationInfo.columnMetaVariables);
+            boost::optional<storm::dd::Add<Type, ValueType>> stateActionDd;
             
             // For DTMCs, we normalize each row to 1 (to account for non-determinism).
             if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
-                result = result / stateActionDd;
+                stateActionDd = result.sumAbstract(generationInfo.columnMetaVariables);
+                result = result / stateActionDd.get();
             } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
                 // For MDPs, we need to throw away the nondeterminism variables from the generation information that
                 // were never used.
@@ -1107,7 +1103,7 @@ namespace storm {
         }
         
         template <storm::dd::DdType Type, typename ValueType>
-        storm::models::symbolic::StandardRewardModel<Type, ValueType> DdPrismModelBuilder<Type, ValueType>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& stateActionDd) {
+        storm::models::symbolic::StandardRewardModel<Type, ValueType> DdPrismModelBuilder<Type, ValueType>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& transitionMatrix, boost::optional<storm::dd::Add<Type, ValueType>> stateActionDd) {
             
             // Start by creating the state reward vector.
             boost::optional<storm::dd::Add<Type, ValueType>> stateRewards;
@@ -1145,13 +1141,15 @@ namespace storm {
                     }
                     ActionDecisionDiagram const& actionDd = stateActionReward.isLabeled() ? globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()) : globalModule.independentAction;
                     states *= actionDd.guardDd * reachableStatesAdd;
-                    storm::dd::Add<Type, ValueType> stateActionRewardDd = synchronization * states * rewards;
+                    storm::dd::Add<Type, ValueType> stateActionRewardDd = synchronization * (reachableStatesAdd * states * rewards);
                     
                     // If we are building the state-action rewards for an MDP, we need to make sure that the encoding
                     // of the nondeterminism is present in the reward vector, so we ne need to multiply it with the
                     // legal state-actions.
                     if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
-                        stateActionRewardDd *= stateActionDd;
+                        // FIXME: get synchronization encoding differently.
+                        // stateActionRewardDd *= stateActionDd;
+                        stateActionRewardDd *= transitionMatrix.notZero().existsAbstract(generationInfo.columnMetaVariables).template toAdd<ValueType>();
                     } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
                         // For CTMCs, we need to multiply the entries with the exit rate of the corresponding action.
                         stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables);
@@ -1167,7 +1165,7 @@ namespace storm {
                 
                 // Scale state-action rewards for DTMCs and CTMCs.
                 if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
-                    stateActionRewards.get() /= stateActionDd;
+                    // stateActionRewards.get() /= stateActionDd;
                 }
             }
             
@@ -1215,7 +1213,7 @@ namespace storm {
                 
                 // Scale transition rewards for DTMCs.
                 if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
-                    transitionRewards.get() /= stateActionDd;
+                    transitionRewards.get() /= stateActionDd.get();
                 }
             }
                         
@@ -1240,7 +1238,7 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
             }
             
-            STORM_LOG_DEBUG("Building representation of program:" << std::endl << program << std::endl);
+            STORM_LOG_TRACE("Building representation of program:" << std::endl << program << std::endl);
             
             // Start by initializing the structure used for storing all information needed during the model generation.
             // In particular, this creates the meta variables used to encode the model.
@@ -1250,7 +1248,6 @@ namespace storm {
             storm::dd::Add<Type, ValueType> transitionMatrix = system.allTransitionsDd;
             
             ModuleDecisionDiagram const& globalModule = system.globalModule;
-            storm::dd::Add<Type, ValueType> stateActionDd = system.stateActionDd;
             
             // If we were asked to treat some states as terminal states, we cut away their transitions now.
             storm::dd::Bdd<Type> terminalStatesBdd = generationInfo.manager->getBddZero();
@@ -1314,7 +1311,9 @@ namespace storm {
             storm::dd::Bdd<Type> reachableStates = storm::utility::dd::computeReachableStates<Type>(initialStates, transitionMatrixBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables);
             storm::dd::Add<Type, ValueType> reachableStatesAdd = reachableStates.template toAdd<ValueType>();
             transitionMatrix *= reachableStatesAdd;
-            stateActionDd *= reachableStatesAdd;
+            if (system.stateActionDd) {
+                system.stateActionDd.get() *= reachableStatesAdd;
+            }
             
             // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
             storm::dd::Bdd<Type> statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables);
@@ -1384,7 +1383,7 @@ namespace storm {
             
             std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
             for (auto const& rewardModel : selectedRewardModels) {
-                rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, reachableStatesAdd, stateActionDd));
+                rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, reachableStatesAdd, transitionMatrix, system.stateActionDd));
             }
             
             // Build the labels that can be accessed as a shortcut.

src/storm/builder/DdPrismModelBuilder.h

@@ -230,7 +230,7 @@ namespace storm {
             
             static storm::dd::Add<Type, ValueType> createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module);
             
-            static storm::models::symbolic::StandardRewardModel<Type, ValueType> createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& stateActionDd);
+            static storm::models::symbolic::StandardRewardModel<Type, ValueType> createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& transitionMatrix, boost::optional<storm::dd::Add<Type, ValueType>> stateActionDd);
             
             static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo);
             

src/storm/storage/dd/Add.cpp

@@ -550,7 +550,11 @@ namespace storm {
             
             // Next, we split the matrix into one for each group. Note that this only works if the group variables are
             // at the very top.
-            std::vector<InternalAdd<LibraryType, ValueType>> groups = internalAdd.splitIntoGroups(ddGroupVariableIndices);
+            std::vector<InternalAdd<LibraryType, ValueType>> internalAddGroups = internalAdd.splitIntoGroups(ddGroupVariableIndices);
+            std::vector<Add<LibraryType, ValueType>> groups;
+            for (auto const& internalAdd : internalAddGroups) {
+                groups.push_back(Add<LibraryType, ValueType>(this->getDdManager(), internalAdd, rowAndColumnMetaVariables));
+            }
             
             // Create the actual storage for the non-zero entries.
             std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>> columnsAndValues(this->getNonZeroCount());
@@ -561,17 +565,20 @@ namespace storm {
             std::vector<InternalAdd<LibraryType, uint_fast64_t>> statesWithGroupEnabled(groups.size());
             InternalAdd<LibraryType, uint_fast64_t> stateToRowGroupCount = this->getDdManager().template getAddZero<uint_fast64_t>();
             for (uint_fast64_t i = 0; i < groups.size(); ++i) {
-                auto const& dd = groups[i];
+                auto const& group = groups[i];
+                auto groupNotZero = group.notZero();
                 
-                dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false);
+                std::vector<uint64_t> tmpRowIndications = groupNotZero.template toAdd<uint_fast64_t>().sumAbstract(columnMetaVariables).toVector(rowOdd);
+                for (uint64_t offset = 0; offset < tmpRowIndications.size(); ++offset) {
+                    rowIndications[rowGroupIndices[offset]] += tmpRowIndications[offset];
+                }
                 
-                statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnVariableCube).template toAdd<uint_fast64_t>();
-                stateToRowGroupCount += statesWithGroupEnabled[i];
+                statesWithGroupEnabled[i] = groupNotZero.existsAbstract(columnMetaVariables).template toAdd<uint_fast64_t>();
                 statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
             }
             
             // Since we modified the rowGroupIndices, we need to restore the correct values.
-            stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus<uint_fast64_t>());
+            stateToNumberOfChoices.internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus<uint_fast64_t>());
             
             // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector.
             tmp = 0;
@@ -585,15 +592,15 @@ namespace storm {
             
             // Now actually fill the entry vector.
             for (uint_fast64_t i = 0; i < groups.size(); ++i) {
-                auto const& dd = groups[i];
+                auto const& group = groups[i];
                 
-                dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true);
+                group.internalAdd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true);
                 
                 statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
             }
             
             // Since we modified the rowGroupIndices, we need to restore the correct values.
-            stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus<uint_fast64_t>());
+            stateToNumberOfChoices.internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus<uint_fast64_t>());
             
             // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values.
             for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) {
@@ -674,7 +681,11 @@ namespace storm {
             std::vector<ValueType> explicitVector(rowGroupIndices.back());
             
             // Next, we split the matrix into one for each group. Note that this only works if the group variables are at the very top.
-            std::vector<std::pair<InternalAdd<LibraryType, ValueType>, InternalAdd<LibraryType, ValueType>>> groups = internalAdd.splitIntoGroups(vector, ddGroupVariableIndices);
+            std::vector<std::pair<InternalAdd<LibraryType, ValueType>, InternalAdd<LibraryType, ValueType>>> internalAddGroups = internalAdd.splitIntoGroups(vector, ddGroupVariableIndices);
+            std::vector<std::pair<Add<LibraryType, ValueType>, Add<LibraryType, ValueType>>> groups;
+            for (auto const& internalAdd : internalAddGroups) {
+                groups.push_back(std::make_pair(Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.first, rowAndColumnMetaVariables), Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.second, rowMetaVariables)));
+            }
 
             // Create the actual storage for the non-zero entries.
             std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>> columnsAndValues(this->getNonZeroCount());
@@ -685,12 +696,18 @@ namespace storm {
             std::vector<InternalAdd<LibraryType, uint_fast64_t>> statesWithGroupEnabled(groups.size());
             InternalAdd<LibraryType, uint_fast64_t> stateToRowGroupCount = this->getDdManager().template getAddZero<uint_fast64_t>();
             for (uint_fast64_t i = 0; i < groups.size(); ++i) {
-                std::pair<InternalAdd<LibraryType, ValueType>, InternalAdd<LibraryType, ValueType>> const& ddPair = groups[i];
+                std::pair<Add<LibraryType, ValueType>, Add<LibraryType, ValueType>> const& ddPair = groups[i];
+                Bdd<LibraryType> matrixDdNotZero = ddPair.first.notZero();
+                Bdd<LibraryType> vectorDdNotZero = ddPair.second.notZero();
+
+                std::vector<uint64_t> tmpRowIndications = matrixDdNotZero.template toAdd<uint_fast64_t>().sumAbstract(columnMetaVariables).toVector(rowOdd);
+                for (uint64_t offset = 0; offset < tmpRowIndications.size(); ++offset) {
+                    rowIndications[rowGroupIndices[offset]] += tmpRowIndications[offset];
+                }
 
-                ddPair.first.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false);
-                ddPair.second.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVector, std::plus<ValueType>());
+                ddPair.second.internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVector, std::plus<ValueType>());
                 
-                statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnVariableCube) || ddPair.second.notZero()).template toAdd<uint_fast64_t>();
+                statesWithGroupEnabled[i] = (matrixDdNotZero.existsAbstract(columnMetaVariables) || vectorDdNotZero).template toAdd<uint_fast64_t>();
                 stateToRowGroupCount += statesWithGroupEnabled[i];
                 statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
             }
@@ -712,8 +729,7 @@ namespace storm {
             for (uint_fast64_t i = 0; i < groups.size(); ++i) {
                 auto const& dd = groups[i].first;
                 
-                dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true);
-                
+                dd.internalAdd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true);
                 statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
             }
             

src/storm/storage/dd/DdManager.cpp

@@ -111,8 +111,17 @@ namespace storm {
 		
         template<DdType LibraryType>
         Bdd<LibraryType> DdManager<LibraryType>::getCube(storm::expressions::Variable const& variable) const {
+            return getCube({variable});
+        }
+        
+        template<DdType LibraryType>
+        Bdd<LibraryType> DdManager<LibraryType>::getCube(std::set<storm::expressions::Variable> const& variables) const {
+            Bdd<LibraryType> result = this->getBddOne();
+            for (auto const& variable : variables) {
                 storm::dd::DdMetaVariable<LibraryType> const& metaVariable = this->getMetaVariable(variable);
-            return metaVariable.getCube();
+                result &= metaVariable.getCube();
+            }
+            return result;
         }
         
         template<DdType LibraryType>

src/storm/storage/dd/DdManager.h

@@ -126,6 +126,14 @@ namespace storm {
              */
             Bdd<LibraryType> getCube(storm::expressions::Variable const& variable) const;
 
+            /*!
+             * Retrieves a BDD that is the cube of the variables representing the given meta variables.
+             *
+             * @param variables The expression variables associated with the meta variables.
+             * @return The cube of the meta variables.
+             */
+            Bdd<LibraryType> getCube(std::set<storm::expressions::Variable> const& variables) const;
+
             /*!
              * Adds an integer meta variable with the given range.
              *

src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -14,6 +14,11 @@
 
 namespace storm {
     namespace dd {
+        template<typename ValueType>
+        InternalAdd<DdType::Sylvan, ValueType>::InternalAdd() : ddManager(nullptr), sylvanMtbdd() {
+            // Intentionally left empty.
+        }
+        
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType>::InternalAdd(InternalDdManager<DdType::Sylvan> const* ddManager, sylvan::Mtbdd const& sylvanMtbdd) : ddManager(ddManager), sylvanMtbdd(sylvanMtbdd) {
             // Intentionally left empty.

src/storm/storage/dd/sylvan/InternalSylvanAdd.h

@@ -55,7 +55,7 @@ namespace storm {
             InternalAdd(InternalDdManager<DdType::Sylvan> const* ddManager, sylvan::Mtbdd const& sylvanMtbdd);
             
             // Instantiate all copy/move constructors/assignments with the default implementation.
-            InternalAdd() = default;
+            InternalAdd();
             InternalAdd(InternalAdd<DdType::Sylvan, ValueType> const& other) = default;
             InternalAdd& operator=(InternalAdd<DdType::Sylvan, ValueType> const& other) = default;
             InternalAdd(InternalAdd<DdType::Sylvan, ValueType>&& other) = default;

src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp

@@ -18,6 +18,10 @@
 
 namespace storm {
     namespace dd {
+        InternalBdd<DdType::Sylvan>::InternalBdd() : ddManager(nullptr), sylvanBdd() {
+            // Intentionally left empty.
+        }
+
         InternalBdd<DdType::Sylvan>::InternalBdd(InternalDdManager<DdType::Sylvan> const* ddManager, sylvan::Bdd const& sylvanBdd) : ddManager(ddManager), sylvanBdd(sylvanBdd) {
             // Intentionally left empty.
         }

src/storm/storage/dd/sylvan/InternalSylvanBdd.h

@@ -35,7 +35,7 @@ namespace storm {
             InternalBdd(InternalDdManager<DdType::Sylvan> const* ddManager, sylvan::Bdd const& sylvanBdd);
             
             // Instantiate all copy/move constructors/assignments with the default implementation.
-            InternalBdd() = default;
+            InternalBdd();
             InternalBdd(InternalBdd<DdType::Sylvan> const& other) = default;
             InternalBdd& operator=(InternalBdd<DdType::Sylvan> const& other) = default;
             InternalBdd(InternalBdd<DdType::Sylvan>&& other) = default;

src/test/storage/JaniModelTest.cpp

@@ -7,7 +7,7 @@
 #include "storm/storage/jani/Model.h"
 
 #ifdef STORM_HAVE_MSAT
-TEST(JaniModelTest, FlattenModules) {
+TEST(JaniModelTest, FlattenComposition) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -19,7 +19,7 @@ TEST(JaniModelTest, FlattenModules) {
     EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges());
 }
 
-TEST(JaniModelTest, FlattenModules_Wlan_Mathsat) {
+TEST(JaniModelTest, FlattenComposition_Wlan_Mathsat) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -31,7 +31,7 @@ TEST(JaniModelTest, FlattenModules_Wlan_Mathsat) {
     EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges());
 }
 
-TEST(JaniModelTest, FlattenModules_Csma_Mathsat) {
+TEST(JaniModelTest, FlattenComposition_Csma_Mathsat) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -43,7 +43,7 @@ TEST(JaniModelTest, FlattenModules_Csma_Mathsat) {
     EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges());
 }
 
-TEST(JaniModelTest, FlattenModules_Firewire_Mathsat) {
+TEST(JaniModelTest, FlattenComposition_Firewire_Mathsat) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -55,7 +55,7 @@ TEST(JaniModelTest, FlattenModules_Firewire_Mathsat) {
     EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges());
 }
 
-TEST(JaniModelTest, FlattenModules_Coin_Mathsat) {
+TEST(JaniModelTest, FlattenComposition_Coin_Mathsat) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -67,7 +67,7 @@ TEST(JaniModelTest, FlattenModules_Coin_Mathsat) {
     EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges());
 }
 
-TEST(JaniModelTest, FlattenModules_Dice_Mathsat) {
+TEST(JaniModelTest, FlattenComposition_Dice_Mathsat) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -81,7 +81,7 @@ TEST(JaniModelTest, FlattenModules_Dice_Mathsat) {
 #endif
 
 #ifdef STORM_HAVE_Z3
-TEST(JaniModelTest, FlattenModules_Leader_Z3) {
+TEST(JaniModelTest, FlattenComposition_Leader_Z3) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -93,7 +93,7 @@ TEST(JaniModelTest, FlattenModules_Leader_Z3) {
     EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges());
 }
 
-TEST(JaniModelTest, FlattenModules_Wlan_Z3) {
+TEST(JaniModelTest, FlattenComposition_Wlan_Z3) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -105,7 +105,7 @@ TEST(JaniModelTest, FlattenModules_Wlan_Z3) {
     EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges());
 }
 
-TEST(JaniModelTest, FlattenModules_Csma_Z3) {
+TEST(JaniModelTest, FlattenComposition_Csma_Z3) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -117,7 +117,7 @@ TEST(JaniModelTest, FlattenModules_Csma_Z3) {
     EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges());
 }
 
-TEST(JaniModelTest, FlattenModules_Firewire_Z3) {
+TEST(JaniModelTest, FlattenComposition_Firewire_Z3) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -129,7 +129,7 @@ TEST(JaniModelTest, FlattenModules_Firewire_Z3) {
     EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges());
 }
 
-TEST(JaniModelTest, FlattenModules_Coin_Z3) {
+TEST(JaniModelTest, FlattenComposition_Coin_Z3) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm"));
     storm::jani::Model janiModel = program.toJani();
@@ -141,7 +141,7 @@ TEST(JaniModelTest, FlattenModules_Coin_Z3) {
     EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges());
 }
 
-TEST(JaniModelTest, FlattenModules_Dice_Z3) {
+TEST(JaniModelTest, FlattenComposition_Dice_Z3) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"));
     storm::jani::Model janiModel = program.toJani();