more work on input-enabling automata

Former-commit-id: 309b5b2b29 [formerly fb97755529]
Former-commit-id: 7f9a32356f

src/builder/DdJaniModelBuilder.cpp

@@ -9,7 +9,7 @@
 #include "src/storage/jani/Model.h"
 #include "src/storage/jani/AutomatonComposition.h"
 #include "src/storage/jani/ParallelComposition.h"
-#include "src/storage/jani/CompositionActionInformationVisitor.h"
+#include "src/storage/jani/CompositionInformationVisitor.h"
 
 #include "src/storage/dd/Add.h"
 #include "src/storage/dd/Bdd.h"
@@ -177,7 +177,7 @@ namespace storm {
         template <storm::dd::DdType Type, typename ValueType>
         class CompositionVariableCreator : public storm::jani::CompositionVisitor {
         public:
-            CompositionVariableCreator(storm::jani::Model const& model, storm::jani::ActionInformation const& actionInformation) : model(model), automata(), actionInformation(actionInformation) {
+            CompositionVariableCreator(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation) : model(model), automata(), actionInformation(actionInformation) {
                 // Intentionally left empty.
             }
             
@@ -356,7 +356,7 @@ namespace storm {
             
             storm::jani::Model const& model;
             std::set<std::string> automata;
-            storm::jani::ActionInformation actionInformation;
+            storm::jani::CompositionInformation actionInformation;
         };
         
         template <storm::dd::DdType Type, typename ValueType>
@@ -612,18 +612,18 @@ namespace storm {
 
             };
             
-            CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::ActionInformation const& actionInformation, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : SystemComposer<Type, ValueType>(model, variables, transientVariables), actionInformation(actionInformation) {
+            CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : SystemComposer<Type, ValueType>(model, variables, transientVariables), actionInformation(actionInformation) {
                 // Intentionally left empty.
             }
         
-            storm::jani::ActionInformation const& actionInformation;
+            storm::jani::CompositionInformation const& actionInformation;
 
             ComposerResult<Type, ValueType> compose() override {
                 std::map<uint64_t, uint64_t> actionIndexToLocalNondeterminismVariableOffset;
                 for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) {
                     actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0;
                 }
-                actionIndexToLocalNondeterminismVariableOffset[actionInformation.getSilentActionIndex()] = 0;
+                actionIndexToLocalNondeterminismVariableOffset[storm::jani::Model::getSilentActionIndex()] = 0;
 
                 AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset));
                 return buildSystemFromAutomaton(globalAutomaton);
@@ -1659,8 +1659,8 @@ namespace storm {
             }
             
             // Determine the actions that will appear in the parallel composition.
-            storm::jani::CompositionActionInformationVisitor actionInformationVisitor(model);
-            storm::jani::ActionInformation actionInformation = actionInformationVisitor.getActionInformation(model.getSystemComposition());
+            storm::jani::CompositionInformationVisitor visitor(model, model.getSystemComposition());
+            storm::jani::CompositionInformation actionInformation = visitor.getInformation();
             
             // Create all necessary variables.
             CompositionVariableCreator<Type, ValueType> variableCreator(model, actionInformation);

src/storage/jani/CompositionActionInformationVisitor.cpp

@@ -1,123 +0,0 @@
-#include "src/storage/jani/CompositionActionInformationVisitor.h"
-
-#include "src/storage/jani/Model.h"
-#include "src/storage/jani/Compositions.h"
-
-namespace storm {
-    namespace jani {
-        
-        ActionInformation::ActionInformation(std::set<uint64_t> const& nonsilentActionIndices, std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap, uint64_t silentActionIndex) : silentActionIndex(silentActionIndex), nonsilentActionIndices(nonsilentActionIndices), indexToNameMap(indexToNameMap), nameToIndexMap(nameToIndexMap) {
-            // Intentionally left empty.
-        }
-        
-        std::string const& ActionInformation::getActionName(uint64_t index) const {
-            return indexToNameMap.at(index);
-        }
-        
-        uint64_t ActionInformation::getActionIndex(std::string const& name) const {
-            return nameToIndexMap.at(name);
-        }
-        
-        std::set<uint64_t> const& ActionInformation::getNonSilentActionIndices() const {
-            return nonsilentActionIndices;
-        }
-        
-        uint64_t ActionInformation::getSilentActionIndex() const {
-            return silentActionIndex;
-        }
-     
-        CompositionActionInformationVisitor::CompositionActionInformationVisitor(storm::jani::Model const& model) : model(model), nextFreeActionIndex(0), nameToIndexMap(), indexToNameMap() {
-            // Intentionally left empty.
-        }
-        
-        ActionInformation CompositionActionInformationVisitor::getActionInformation(storm::jani::Composition const& composition) {
-            indexToNameMap.clear();
-            nameToIndexMap.clear();
-
-            // Determine the next free index we can give out to a new action.
-            for (auto const& action : model.getActions()) {
-                uint64_t actionIndex = model.getActionIndex(action.getName());
-                
-                nameToIndexMap[action.getName()] = model.getActionIndex(action.getName());
-                indexToNameMap[actionIndex] = action.getName();
-
-                nextFreeActionIndex = std::max(nextFreeActionIndex, model.getActionIndex(action.getName()));
-            }
-            ++nextFreeActionIndex;
-            
-            std::set<uint64_t> nonSilentActionIndices = boost::any_cast<std::set<uint64_t>>(composition.accept(*this, boost::none));
-            
-            return ActionInformation(nonSilentActionIndices, indexToNameMap, nameToIndexMap);
-        }
-        
-        boost::any CompositionActionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) {
-            std::set<uint64_t> result = model.getAutomaton(composition.getAutomatonName()).getActionIndices();
-            result.erase(model.getSilentActionIndex());
-            return result;
-        }
-        
-        boost::any CompositionActionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) {
-            std::vector<std::set<uint64_t>> subresults;
-            for (auto const& subcomposition : composition.getSubcompositions()) {
-                subresults.push_back(boost::any_cast<std::set<uint64_t>>(subcomposition->accept(*this, boost::none)));
-            }
-
-            std::set<uint64_t> effectiveSynchronizationVectors;
-            for (uint64_t index = 0; index < composition.getNumberOfSynchronizationVectors(); ++index) {
-                effectiveSynchronizationVectors.insert(index);
-            }
-            
-            // Determine all actions that do not take part in synchronization vectors.
-            std::set<uint64_t> result;
-            for (uint64_t subresultIndex = 0; subresultIndex < subresults.size(); ++subresultIndex) {
-                std::set<uint64_t> actionsInSynch;
-                std::set<uint64_t> localEffectiveSynchVectors;
-                for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) {
-                    auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex);
-                    
-                    if (synchVector.isNoActionInput(synchVector.getInput(subresultIndex))) {
-                        effectiveSynchronizationVectors.insert(synchVectorIndex);
-                    } else {
-                        uint64_t synchVectorActionIndex = nameToIndexMap.at(synchVector.getInput(subresultIndex));
-                        actionsInSynch.insert(synchVectorActionIndex);
-                        
-                        // If the action of they synchronization vector at this position is one that is actually contained
-                        // in the corresponding subcomposition, the synchronization vector is effective.
-                        if (subresults[subresultIndex].find(synchVectorActionIndex) != subresults[subresultIndex].end()) {
-                            effectiveSynchronizationVectors.insert(synchVectorIndex);
-                        }
-                    }
-                }
-                
-                std::set_difference(subresults[subresultIndex].begin(), subresults[subresultIndex].end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(result, result.begin()));
-                
-                // Intersect the previously effective synchronization vectors with the ones that were derived to be
-                // effective for the current subcomposition.
-                std::set<uint64_t> newEffectiveSynchVectors;
-                std::set_intersection(effectiveSynchronizationVectors.begin(), effectiveSynchronizationVectors.end(), newEffectiveSynchVectors.begin(), newEffectiveSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin()));
-                effectiveSynchronizationVectors = std::move(newEffectiveSynchVectors);
-            }
-            
-            // Now add all outputs of synchronization vectors.
-            for (auto const& synchVector : composition.getSynchronizationVectors()) {
-                if (synchVector.getOutput() != storm::jani::Model::getSilentActionName()) {
-                    result.insert(addOrGetActionIndex(synchVector.getOutput()));
-                }
-            }
-            
-            return result;
-        }
-
-        uint64_t CompositionActionInformationVisitor::addOrGetActionIndex(std::string const& name) {
-            auto it = nameToIndexMap.find(name);
-            if (it != nameToIndexMap.end()) {
-                return it->second;
-            } else {
-                nameToIndexMap[name] = nextFreeActionIndex;
-                indexToNameMap[nextFreeActionIndex] = name;
-                return nextFreeActionIndex++;
-            }
-        }
-        
-    }
-}

src/storage/jani/CompositionActionInformationVisitor.h

@@ -1,49 +0,0 @@
-#pragma once
-
-#include <set>
-#include <map>
-
-#include "src/storage/jani/CompositionVisitor.h"
-
-namespace storm {
-    namespace jani {
-        
-        class Model;
-        
-        class ActionInformation {
-        public:
-            ActionInformation(std::set<uint64_t> const& nonsilentActionIndices, std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap, uint64_t silentActionIndex = 0);
-            
-            std::string const& getActionName(uint64_t index) const;
-            uint64_t getActionIndex(std::string const& name) const;
-            std::set<uint64_t> const& getNonSilentActionIndices() const;
-            uint64_t getSilentActionIndex() const;
-            
-        private:
-            uint64_t silentActionIndex;
-            std::set<uint64_t> nonsilentActionIndices;
-            std::map<uint64_t, std::string> indexToNameMap;
-            std::map<std::string, uint64_t> nameToIndexMap;
-        };
-        
-        class CompositionActionInformationVisitor : public CompositionVisitor {
-        public:
-            CompositionActionInformationVisitor(storm::jani::Model const& model);
-            
-            ActionInformation getActionInformation(storm::jani::Composition const& composition);
-            
-            virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override;
-            virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override;
-            
-        private:
-            uint64_t addOrGetActionIndex(std::string const& name);
-            
-            storm::jani::Model const& model;
-            uint64_t nextFreeActionIndex;
-            std::map<std::string, uint64_t> nameToIndexMap;
-            std::map<uint64_t, std::string> indexToNameMap;
-        };
-
-        
-    }
-}

src/storage/jani/CompositionInformationVisitor.cpp

@@ -3,14 +3,13 @@
 #include "src/storage/jani/Model.h"
 #include "src/storage/jani/Compositions.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/WrongFormatException.h"
+
 namespace storm {
     namespace jani {
         
-        CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), nonStandardParallelComposition(false) {
-            // Intentionally left empty.
-        }
-        
-        CompositionInformation::CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool nonStandardParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), nonStandardParallelComposition(nonStandardParallelComposition) {
+        CompositionInformation::CompositionInformation() : nonStandardParallelComposition(false) {
             // Intentionally left empty.
         }
         
@@ -18,36 +17,84 @@ namespace storm {
             automatonNameToMultiplicity[automatonName] += count;
         }
 
-        void CompositionInformation::addNonsilentAction(std::string const& actionName) {
-            nonsilentActions.insert(actionName);
+        std::map<std::string, uint64_t> const& CompositionInformation::getAutomatonToMultiplicityMap() const {
+            return automatonNameToMultiplicity;
         }
 
-        std::set<std::string> const& CompositionInformation::getNonsilentActions() const {
-            return nonsilentActions;
+        void CompositionInformation::addMultiplicityMap(std::map<std::string, uint64_t> const& multiplicityMap) {
+            automatonNameToMultiplicity = joinMultiplicityMaps(automatonNameToMultiplicity, multiplicityMap);
         }
         
-        void CompositionInformation::setContainsNonStandardParallelComposition() {
-            nonStandardParallelComposition = true;
+        std::map<std::string, uint64_t> CompositionInformation::joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second) {
+            std::map<std::string, uint64_t> result = first;
+            for (auto const& element : second) {
+                result[element.first] += element.second;
+            }
+            return result;
+        }
+        
+        void CompositionInformation::setContainsNonStandardParallelComposition(bool value) {
+            nonStandardParallelComposition = value;
         }
         
         bool CompositionInformation::containsNonStandardParallelComposition() const {
             return nonStandardParallelComposition;
         }
         
-        std::map<std::string, uint64_t> CompositionInformation::joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second) {
-            std::map<std::string, uint64_t> result = first;
-            for (auto const& element : second) {
-                result[element.first] += element.second;
+        std::string const& CompositionInformation::getActionName(uint64_t index) const {
+            return indexToNameMap.at(index);
         }
-            return result;
+        
+        uint64_t CompositionInformation::getActionIndex(std::string const& name) const {
+            return nameToIndexMap.at(name);
         }
         
-        std::map<std::string, uint64_t> const& CompositionInformation::getAutomatonToMultiplicityMap() const {
-            return automatonNameToMultiplicity;
+        void CompositionInformation::addNonSilentActionIndex(uint64_t index) {
+            nonSilentActionIndices.insert(index);
         }
         
-        CompositionInformation CompositionInformationVisitor::getInformation(Composition const& composition, Model const& model) {
-            return boost::any_cast<CompositionInformation>(composition.accept(*this, model));
+        void CompositionInformation::addNonSilentActionIndices(std::set<uint64_t> const& indices) {
+            nonSilentActionIndices.insert(indices.begin(), indices.end());
+        }
+        
+        bool CompositionInformation::hasNonSilentActionIndex(uint64_t index) {
+            return nonSilentActionIndices.find(index) != nonSilentActionIndices.end();
+        }
+        
+        void CompositionInformation::addInputEnabledActionIndex(uint64_t index) {
+            inputEnabledActionIndices.insert(index);
+        }
+        
+        std::set<uint64_t> const& CompositionInformation::getNonSilentActionIndices() const {
+            return nonSilentActionIndices;
+        }
+
+        std::set<uint64_t> const& CompositionInformation::getInputEnabledActionIndices() const {
+            return inputEnabledActionIndices;
+        }
+        
+        void CompositionInformation::setMappings(std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap) {
+            this->indexToNameMap = indexToNameMap;
+            this->nameToIndexMap = nameToIndexMap;
+        }
+        
+        CompositionInformationVisitor::CompositionInformationVisitor(Model const& model, Composition const& composition) : model(model), composition(composition), nextFreeActionIndex(0) {
+            // Determine the next free index we can give out to a new action.
+            for (auto const& action : model.getActions()) {
+                uint64_t actionIndex = model.getActionIndex(action.getName());
+                
+                nameToIndexMap[action.getName()] = model.getActionIndex(action.getName());
+                indexToNameMap[actionIndex] = action.getName();
+                
+                nextFreeActionIndex = std::max(nextFreeActionIndex, model.getActionIndex(action.getName()));
+            }
+            ++nextFreeActionIndex;
+        }
+        
+        CompositionInformation CompositionInformationVisitor::getInformation() {
+            CompositionInformation result = boost::any_cast<CompositionInformation>(composition.accept(*this, model));
+            result.setMappings(indexToNameMap, nameToIndexMap);
+            return result;
         }
                 
         boost::any CompositionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) {
@@ -58,27 +105,35 @@ namespace storm {
             result.increaseAutomatonMultiplicity(composition.getAutomatonName());
             for (auto const& actionIndex : automaton.getActionIndices()) {
                 if (actionIndex != model.getSilentActionIndex()) {
-                    result.addNonsilentAction(model.getAction(actionIndex).getName());
+                    result.addNonSilentActionIndex(actionIndex);
                 }
             }
+            for (auto const& action : composition.getInputEnabledActions()) {
+                auto it = nameToIndexMap.find(action);
+                STORM_LOG_THROW(it != nameToIndexMap.end(), storm::exceptions::WrongFormatException, "Illegal action name '" << action << "' in when input-enabling automaton '" << composition.getAutomatonName() << "'.");
+                uint64_t actionIndex = it->second;
+                STORM_LOG_THROW(result.hasNonSilentActionIndex(actionIndex), storm::exceptions::WrongFormatException, "Cannot make automaton '" << composition.getAutomatonName() << "' input enabled for action " << action << ", because it has no such action.");
+                result.addInputEnabledActionIndex(actionIndex);
+            }
             return result;
         }
         
         boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) {
+            CompositionInformation result;
+
             std::vector<CompositionInformation> subinformation;
             
-            std::set<std::string> nonsilentSubActions;
+            std::set<uint64_t> nonsilentSubActionIndices;
             for (auto const& subcomposition : composition.getSubcompositions()) {
                 subinformation.push_back(boost::any_cast<CompositionInformation>(subcomposition->accept(*this, data)));
-                nonsilentSubActions.insert(subinformation.back().getNonsilentActions().begin(), subinformation.back().getNonsilentActions().end());
+                nonsilentSubActionIndices.insert(subinformation.back().getNonSilentActionIndices().begin(), subinformation.back().getNonSilentActionIndices().end());
             }
             
-            std::map<std::string, uint64_t> joinedAutomatonToMultiplicityMap;
             bool containsNonStandardParallelComposition = false;
             
             for (auto const& subinfo : subinformation) {
                 containsNonStandardParallelComposition |= subinfo.containsNonStandardParallelComposition();
-                joinedAutomatonToMultiplicityMap = CompositionInformation::joinMultiplicityMaps(joinedAutomatonToMultiplicityMap, subinfo.getAutomatonToMultiplicityMap());
+                result.addMultiplicityMap(subinfo.getAutomatonToMultiplicityMap());
             }
             
             // Keep track of the synchronization vectors that are effective, meaning that the subcompositions all have
@@ -89,7 +144,7 @@ namespace storm {
             }
             
             // Now compute non-silent actions.
-            std::set<std::string> nonsilentActions;
+            std::set<uint64_t> nonSilentActionIndices;
             for (uint_fast64_t infoIndex = 0; infoIndex < subinformation.size(); ++infoIndex) {
                 auto const& subinfo = subinformation[infoIndex];
                 
@@ -98,10 +153,11 @@ namespace storm {
                 for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) {
                     auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex);
                     if (synchVector.getInput(infoIndex) != SynchronizationVector::getNoActionInput()) {
-                        for (auto const& nonsilentAction : subinfo.getNonsilentActions()) {
-                            if (synchVector.getInput(infoIndex) == nonsilentAction) {
+                        for (auto const& nonsilentActionIndex : subinfo.getNonSilentActionIndices()) {
+                            std::string const& nonSilentAction = indexToNameMap.at(nonsilentActionIndex);
+                            if (synchVector.getInput(infoIndex) == nonSilentAction) {
                                 enabledSynchVectors.insert(synchVectorIndex);
-                                actionsInSynch.insert(nonsilentAction);
+                                actionsInSynch.insert(nonSilentAction);
                             }
                         }
                     } else {
@@ -109,7 +165,7 @@ namespace storm {
                     }
                 }
                 
-                std::set_difference(subinfo.getNonsilentActions().begin(), subinfo.getNonsilentActions().end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(nonsilentActions, nonsilentActions.begin()));
+                std::set_difference(subinfo.getNonSilentActionIndices().begin(), subinfo.getNonSilentActionIndices().end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(nonSilentActionIndices, nonSilentActionIndices.begin()));
 
                 std::set<uint64_t> newEffectiveSynchVectors;
                 std::set_intersection(effectiveSynchVectors.begin(), effectiveSynchVectors.end(), enabledSynchVectors.begin(), enabledSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin()));
@@ -128,19 +184,20 @@ namespace storm {
             // Construct the set of expected synchronization vectors.
             std::set<storm::jani::SynchronizationVector, storm::jani::SynchronizationVectorLexicographicalLess> expectedSynchVectorSetUnderApprox;
             std::set<storm::jani::SynchronizationVector, storm::jani::SynchronizationVectorLexicographicalLess> expectedSynchVectorSetOverApprox;
-            for (auto action : nonsilentSubActions) {
+            for (auto actionIndex : nonsilentSubActionIndices) {
+                std::string const& actionName = indexToNameMap.at(actionIndex);
                 std::vector<std::string> input;
                 uint64_t numberOfParticipatingAutomata = 0;
                 for (auto const& subcomposition : subinformation) {
-                    if (subcomposition.getNonsilentActions().find(action) != subcomposition.getNonsilentActions().end()) {
-                        input.push_back(action);
+                    if (subcomposition.getNonSilentActionIndices().find(actionIndex) != subcomposition.getNonSilentActionIndices().end()) {
+                        input.push_back(actionName);
                         ++numberOfParticipatingAutomata;
                     } else {
                         input.push_back(SynchronizationVector::getNoActionInput());
                     }
                 }
                 
-                storm::jani::SynchronizationVector newSynchVector(input, action);
+                storm::jani::SynchronizationVector newSynchVector(input, actionName);
                 expectedSynchVectorSetOverApprox.insert(newSynchVector);
                 if (numberOfParticipatingAutomata > 1) {
                     expectedSynchVectorSetUnderApprox.insert(newSynchVector);
@@ -151,7 +208,21 @@ namespace storm {
 
             containsNonStandardParallelComposition |= !std::includes(synchVectorSet.begin(), synchVectorSet.end(), expectedSynchVectorSetUnderApprox.begin(), expectedSynchVectorSetUnderApprox.end(), SynchronizationVectorLexicographicalLess());
 
-            return CompositionInformation(joinedAutomatonToMultiplicityMap, nonsilentActions, containsNonStandardParallelComposition);
+            result.setContainsNonStandardParallelComposition(containsNonStandardParallelComposition);
+            
+            result.addNonSilentActionIndices(nonSilentActionIndices);
+            return result;
+        }
+        
+        uint64_t CompositionInformationVisitor::addOrGetActionIndex(std::string const& name) {
+            auto it = nameToIndexMap.find(name);
+            if (it != nameToIndexMap.end()) {
+                return it->second;
+            } else {
+                nameToIndexMap[name] = nextFreeActionIndex;
+                indexToNameMap[nextFreeActionIndex] = name;
+                return nextFreeActionIndex++;
+            }
         }
         
     }

src/storage/jani/CompositionInformationVisitor.h

@@ -16,38 +16,65 @@ namespace storm {
         class CompositionInformation {
         public:
             CompositionInformation();
-            CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool nonStandardParallelComposition);
 
             void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1);
+            std::map<std::string, uint64_t> const& getAutomatonToMultiplicityMap() const;
+            static std::map<std::string, uint64_t> joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second);
+            void addMultiplicityMap(std::map<std::string, uint64_t> const& multiplicityMap);
             
-            void addNonsilentAction(std::string const& actionName);
-            std::set<std::string> const& getNonsilentActions() const;
-            
-            void setContainsNonStandardParallelComposition();
+            void setContainsNonStandardParallelComposition(bool value);
             bool containsNonStandardParallelComposition() const;
             
-            static std::map<std::string, uint64_t> joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second);
-            std::map<std::string, uint64_t> const& getAutomatonToMultiplicityMap() const;
+            std::string const& getActionName(uint64_t index) const;
+            uint64_t getActionIndex(std::string const& name) const;
+
+            void addNonSilentActionIndex(uint64_t index);
+            void addNonSilentActionIndices(std::set<uint64_t> const& indices);
+            bool hasNonSilentActionIndex(uint64_t index);
+            void addInputEnabledActionIndex(uint64_t index);
+
+            std::set<uint64_t> const& getNonSilentActionIndices() const;
+            std::set<uint64_t> const& getInputEnabledActionIndices() const;
+            
+            void setMappings(std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap);
             
         private:
+            /// The indices of the non-silent actions appearing in the topmost element of the composition.
+            std::set<uint64_t> nonSilentActionIndices;
+
+            /// The set of indices of actions for which the topmost element of the composition is input-enabled.
+            std::set<uint64_t> inputEnabledActionIndices;
+            
+            /// A mapping from action indices to names. Since the composition may introduce new action names, this may
+            /// extend the one from the underlying model.
+            std::map<uint64_t, std::string> indexToNameMap;
+            
+            /// A mapping from action names to their indices.
+            std::map<std::string, uint64_t> nameToIndexMap;
+
             /// A mapping from the automata's names to the amount of times they occur in the composition.
             std::map<std::string, uint64_t> automatonNameToMultiplicity;
             
-            /// The set of non-silent actions contained in the composition.
-            std::set<std::string> nonsilentActions;
-                        
             /// A flag indicating whether the composition contains any non-standard parallel composition.
             bool nonStandardParallelComposition;
         };
         
         class CompositionInformationVisitor : public CompositionVisitor {
         public:
-            CompositionInformationVisitor() = default;
-            
-            CompositionInformation getInformation(Composition const& composition, Model const& model);
+            CompositionInformationVisitor(Model const& model, Composition const& composition);
+            CompositionInformation getInformation();
 
             virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override;
             virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override;
+            
+        private:
+            uint64_t addOrGetActionIndex(std::string const& name);
+            
+            storm::jani::Model const& model;
+            Composition const& composition;
+            uint64_t nextFreeActionIndex;
+            std::map<std::string, uint64_t> nameToIndexMap;
+            std::map<uint64_t, std::string> indexToNameMap;
         };
         
     }

src/storage/jani/Model.cpp

@@ -277,7 +277,7 @@ namespace storm {
         }
                 
         uint64_t Model::getSilentActionIndex() const {
-            return silentActionIndex;
+            return SILENT_ACTION_INDEX;
         }
         
         Model Model::defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {

src/storage/jani/Model.h

@@ -232,11 +232,6 @@ namespace storm {
              */
             std::set<std::string> getActionNames(bool includeSilent = true) const;
             
-            /*!
-             * Retrieves the index of the silent action.
-             */
-            uint64_t getSilentActionIndex() const;
-            
             /*!
              * Defines the undefined constants of the model by the given expressions. The original model is not modified,
              * but instead a new model is created.
@@ -338,6 +333,11 @@ namespace storm {
              */
             static bool isSilentAction(std::string const& name);
             
+            /*!
+             * Retrieves the index of the silent action.
+             */
+            static uint64_t getSilentActionIndex();
+            
         private:
             /// The name of the silent action.
             static const std::string SILENT_ACTION_NAME;