Implemented simplification of system composition (this enables compatibility for more benchmarks in the dd engine).

src/storm-conv/api/storm-conv.cpp

@@ -53,6 +53,10 @@ namespace storm {
                 }
             }
 
+            if (options.simplifyComposition) {
+                janiModel.simplifyComposition();
+            }
+            
             if (options.flatten) {
                 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
                 if (storm::settings::hasModule<storm::settings::modules::CoreSettings>()) {

src/storm-conv/converter/options/JaniConversionOptions.cpp

@@ -3,11 +3,11 @@
 namespace storm {
     namespace converter {
 
-        JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), localVars(false), globalVars(false), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true), replaceUnassignedVariablesWithConstants(false) {
+        JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), localVars(false), globalVars(false), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true), replaceUnassignedVariablesWithConstants(false), simplifyComposition(false) {
             // Intentionally left empty
         }
 
-        JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), localVars(settings.isLocalVarsSet()), globalVars(settings.isGlobalVarsSet()), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true), replaceUnassignedVariablesWithConstants(settings.isReplaceUnassignedVariablesWithConstantsSet()) {
+        JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), localVars(settings.isLocalVarsSet()), globalVars(settings.isGlobalVarsSet()), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true), replaceUnassignedVariablesWithConstants(settings.isReplaceUnassignedVariablesWithConstantsSet()), simplifyComposition(settings.isSimplifyCompositionSet()) {
             if (settings.isEliminateFunctionsSet()) {
                 allowedModelFeatures.remove(storm::jani::ModelFeature::Functions);
             }

src/storm-conv/converter/options/JaniConversionOptions.h

@@ -44,6 +44,10 @@ namespace storm {
             
             /// If set, local and global variables that are (a) not assigned to some value and (b) have a known initial value are replaced by constants.
             bool replaceUnassignedVariablesWithConstants;
+            
+            /// If set, attempts to simplify the system composition
+            bool simplifyComposition;
+            
         };
     }
 }

src/storm-conv/settings/modules/JaniExportSettings.cpp

@@ -23,6 +23,7 @@ namespace storm {
             const std::string JaniExportSettings::eliminateArraysOptionName = "remove-arrays";
             const std::string JaniExportSettings::eliminateFunctionsOptionName = "remove-functions";
             const std::string JaniExportSettings::replaceUnassignedVariablesWithConstantsOptionName = "replace-unassigned-vars";
+            const std::string JaniExportSettings::simplifyCompositionOptionName = "simplify-composition";
             
             JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, locationVariablesOptionName, true, "Variables to export in the location").addArgument(storm::settings::ArgumentBuilder::createStringArgument("variables", "A comma separated list of automaton and local variable names seperated by a dot, e.g. A.x,B.y.").setDefaultValueString("").build()).build());
@@ -34,6 +35,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, eliminateArraysOptionName, false, "If set, transforms the model such that array variables/expressions are eliminated.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, eliminateFunctionsOptionName, false, "If set, transforms the model such that functions are eliminated.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, replaceUnassignedVariablesWithConstantsOptionName, false, "If set, local and global variables that are (a) not assigned to some value and (b) have a known initial value are replaced by constants.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, simplifyCompositionOptionName, false, "If set, attempts to simplify the system composition.").build());
             }
             
             bool JaniExportSettings::isAllowEdgeAssignmentsSet() const {
@@ -88,6 +90,10 @@ namespace storm {
                 return this->getOption(replaceUnassignedVariablesWithConstantsOptionName).getHasOptionBeenSet();
             }
             
+            bool JaniExportSettings::isSimplifyCompositionSet() const {
+                return this->getOption(simplifyCompositionOptionName).getHasOptionBeenSet();
+            }
+            
             void JaniExportSettings::finalize() {
                 
             }

src/storm-conv/settings/modules/JaniExportSettings.h

@@ -31,6 +31,8 @@ namespace storm {
                 bool isEliminateFunctionsSet() const;
                 
                 bool isReplaceUnassignedVariablesWithConstantsSet() const;
+                
+                bool isSimplifyCompositionSet() const;
 
                 std::vector<std::pair<std::string, std::string>> getLocationVariables() const;
 
@@ -49,6 +51,7 @@ namespace storm {
                 static const std::string eliminateArraysOptionName;
                 static const std::string eliminateFunctionsOptionName;
                 static const std::string replaceUnassignedVariablesWithConstantsOptionName;
+                static const std::string simplifyCompositionOptionName;
                 
             };
         }

src/storm/builder/DdJaniModelBuilder.cpp

@@ -91,20 +91,6 @@ namespace storm {
                     return false;
                 }
             }
-            // Check system composition
-            auto compositionInfo = storm::jani::CompositionInformationVisitor(model, model.getSystemComposition()).getInformation();
-            
-            // Every automaton has to occur exactly once.
-            if (compositionInfo.getAutomatonToMultiplicityMap().size() != model.getNumberOfAutomata()) {
-                STORM_LOG_INFO("Symbolic engine can not build Jani model since the system composition does not list each automaton exactly once.");
-                return false;
-            }
-            for (auto automatonMultiplicity : compositionInfo.getAutomatonToMultiplicityMap()) {
-                if (automatonMultiplicity.second > 1) {
-                    STORM_LOG_INFO("Symbolic engine can not build Jani model since the system composition does not list each automaton exactly once.");
-                    return false;
-                }
-            }
             
             // There probably are more cases where the model is unsupported. However, checking these is often more involved.
             // As this method is supposed to be a quick check, we just return true at this point.
@@ -2155,6 +2141,7 @@ namespace storm {
             features.remove(storm::jani::ModelFeature::StateExitRewards);
 
             storm::jani::Model preparedModel = model;
+            preparedModel.simplifyComposition();
             if (features.hasArrays()) {
                 STORM_LOG_ERROR("The jani model still considers arrays. These should have been eliminated before calling the dd builder. The arrays are eliminated now, but occurrences in properties will not be handled properly.");
                 preparedModel.eliminateArrays();

src/storm/storage/jani/Automaton.cpp

@@ -38,6 +38,7 @@ namespace storm {
             }
             result.variables.substituteExpressionVariables(oldToNewVarMap);
             result.substitute(oldToNewVarMap);
+            return result;
         }
         
         std::string const& Automaton::getName() const {

src/storm/storage/jani/Model.cpp

@@ -955,6 +955,69 @@ namespace storm {
             return *composition;
         }
         
+        class CompositionSimplificationVisitor : public CompositionVisitor {
+        public:
+            CompositionSimplificationVisitor(std::unordered_map<std::string, std::vector<std::string>> const& automatonToCopiesMap) : automatonToCopiesMap(automatonToCopiesMap) {}
+            
+            std::shared_ptr<Composition> simplify(Composition const& oldComposition) {
+                return boost::any_cast<std::shared_ptr<Composition>>(oldComposition.accept(*this, boost::any()));
+            }
+            
+            virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override {
+                std::string name = composition.getAutomatonName();
+                if (automatonToCopiesMap.count(name) != 0) {
+                    auto& copies = automatonToCopiesMap[name];
+                    STORM_LOG_ASSERT(!copies.empty(), "Not enough copies of automaton " << name << ".");
+                    name = copies.back();
+                    copies.pop_back();
+                }
+                return std::shared_ptr<Composition>(new AutomatonComposition(name, composition.getInputEnabledActions()));
+            }
+            
+            virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override {
+                std::vector<std::shared_ptr<Composition>> subcomposition;
+                for (auto const& p : composition.getSubcompositions()) {
+                    subcomposition.push_back(boost::any_cast<std::shared_ptr<Composition>>(p->accept(*this, data)));
+                }
+                return std::shared_ptr<Composition>(new ParallelComposition(subcomposition, composition.getSynchronizationVectors()));
+            }
+            
+        private:
+            std::unordered_map<std::string, std::vector<std::string>> automatonToCopiesMap;
+        };
+        
+        void Model::simplifyComposition() {
+            CompositionInformationVisitor visitor(*this, this->getSystemComposition());
+            CompositionInformation info = visitor.getInformation();
+            if (info.containsNestedParallelComposition()) {
+                STORM_LOG_WARN("Unable to simplify non-standard compliant system composition.");
+            }
+            
+            // Check whether we need to copy certain automata
+            std::unordered_map<std::string, std::vector<std::string>> automatonToCopiesMap;
+            for (auto const& automatonMultiplicity : info.getAutomatonToMultiplicityMap()) {
+                if (automatonMultiplicity.second > 1) {
+                    std::vector<std::string> copies = {automatonMultiplicity.first};
+                    // We need to copy this automaton n-1 times.
+                    for (uint64_t copyIndex = 1; copyIndex < automatonMultiplicity.second; ++copyIndex) {
+                        std::string copyPrefix = "Copy__" + std::to_string(copyIndex) + "_Of";
+                        std::string copyAutName = copyPrefix + automatonMultiplicity.first;
+                        this->addAutomaton(this->getAutomaton(automatonMultiplicity.first).clone(getManager(), copyAutName, copyPrefix));
+                        copies.push_back(copyAutName);
+                    }
+                    // For esthetic reasons we reverse the list of copies so that the ones with the lowest index will be pop_back'ed first
+                    std::reverse(copies.begin(), copies.end());
+                    // We insert the copies in reversed order as they will be popped in reversed order, as well.
+                    automatonToCopiesMap[automatonMultiplicity.first] = std::move(copies);
+                }
+            }
+            
+            // Traverse the system composition and exchange automata by their copy
+            auto newComposition = CompositionSimplificationVisitor(automatonToCopiesMap).simplify(getSystemComposition());
+            this->setSystemComposition(newComposition);
+            
+        }
+        
         void Model::setSystemComposition(std::shared_ptr<Composition> const& composition) {
             this->composition = composition;
         }

src/storm/storage/jani/Model.h

@@ -412,6 +412,13 @@ namespace storm {
              */
             Composition const& getSystemComposition() const;
             
+            /*!
+             * Attempts to simplify the composition.
+             * Right now, this only means that automata that occur  multiple times in the composition will be
+             * duplicated su that each automata occurs at most once.
+             */
+            void simplifyComposition();
+            
             /*!
              * Retrieves the set of action names.
              */