making sure to add meta variables to transition matrix DD to make sure one can abstract from them later

src/storm/builder/DdPrismModelBuilder.cpp

@@ -1057,10 +1057,21 @@ namespace storm {
         }
         
         template <storm::dd::DdType Type, typename ValueType>
-        storm::dd::Add<Type, ValueType> DdPrismModelBuilder<Type, ValueType>::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module) {
+        storm::dd::Add<Type, ValueType> DdPrismModelBuilder<Type, ValueType>::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram& module) {
+            storm::dd::Add<Type, ValueType> result;
+            
+            // Make sure all actions contain all necessary meta variables.
+            module.independentAction.ensureContainsVariables(generationInfo.rowMetaVariables, generationInfo.columnMetaVariables);
+            for (auto& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
+                synchronizingAction.second.ensureContainsVariables(generationInfo.rowMetaVariables, generationInfo.columnMetaVariables);
+            }
+            
+
+
+            
             // If the model is an MDP, we need to encode the nondeterminism using additional variables.
             if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
-                storm::dd::Add<Type, ValueType> result = generationInfo.manager->template getAddZero<ValueType>();
+                result = generationInfo.manager->template getAddZero<ValueType>();
                 
                 // First, determine the highest number of nondeterminism variables that is used in any action and make
                 // all actions use the same amout of nondeterminism variables.
@@ -1080,6 +1091,7 @@ namespace storm {
                 for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) {
                     nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd<ValueType>();
                 }
+
                 result = identityEncoding * module.independentAction.transitionsDd * nondeterminismEncoding;
                 
                 // Add variables to synchronized action DDs.
@@ -1112,8 +1124,6 @@ namespace storm {
                 for (auto const& synchronizingAction : synchronizingActionToDdMap) {
                     result += synchronizingAction.second;
                 }
-                
-                return result;
             } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
                 // Simply add all actions, but make sure to include the missing global variable identities.
                 
@@ -1126,8 +1136,7 @@ namespace storm {
                     identityEncoding *= generationInfo.variableToIdentityMap.at(variable);
                 }
 
-                storm::dd::Add<Type, ValueType> result = identityEncoding * module.independentAction.transitionsDd;
-                
+                result = identityEncoding * module.independentAction.transitionsDd;
                 for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
                     // Compute missing global variable identities in synchronizing actions.
                     missingIdentities = std::set<storm::expressions::Variable>();
@@ -1140,10 +1149,10 @@ namespace storm {
                     
                     result += identityEncoding * synchronizingAction.second.transitionsDd;
                 }
-                return result;
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
             }
+            return result;
         }
         
         template <storm::dd::DdType Type, typename ValueType>

src/storm/builder/DdPrismModelBuilder.h

@@ -130,6 +130,12 @@ namespace storm {
                     // Intentionally left empty.
                 }
                 
+                void ensureContainsVariables(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) {
+                    guardDd.addMetaVariables(rowMetaVariables);
+                    transitionsDd.addMetaVariables(rowMetaVariables);
+                    transitionsDd.addMetaVariables(columnMetaVariables);
+                }
+                
                 ActionDecisionDiagram(ActionDecisionDiagram const& other) = default;
                 ActionDecisionDiagram& operator=(ActionDecisionDiagram const& other) = default;
                 
@@ -228,7 +234,7 @@ namespace storm {
 
             static storm::dd::Add<Type, ValueType> getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, uint_fast64_t actionIndex = 0);
             
-            static storm::dd::Add<Type, ValueType> createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module);
+            static storm::dd::Add<Type, ValueType> createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram& module);
             
             static std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> createRewardModelDecisionDiagrams(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, SystemResult& system, GenerationInformation& generationInfo, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& transitionMatrix);
 

src/storm/storage/dd/Dd.cpp

@@ -78,7 +78,7 @@ namespace storm {
         template<DdType LibraryType>
         std::set<storm::expressions::Variable> Dd<LibraryType>::subtractMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second) {
             bool includesAllMetaVariables = std::includes(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end());
-            STORM_LOG_WARN_COND(includesAllMetaVariables, "Subtracting from meta variables that are not contained in the DD.");
+            STORM_LOG_THROW(includesAllMetaVariables, storm::exceptions::InvalidArgumentException, "Cannot subtract meta variables that are not contained in the DD.");
             std::set<storm::expressions::Variable> metaVariables;
             std::set_difference(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
             return metaVariables;

src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

@@ -896,7 +896,7 @@ namespace storm {
                     
                     quotientRewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel<ValueType>(std::move(quotientStateRewards), std::move(quotientStateActionRewards), boost::none));
                 }
-                start = std::chrono::high_resolution_clock::now();
+                end = std::chrono::high_resolution_clock::now();
                 STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> result;