JANI next-state generator can now generate transitions from silent edges

Former-commit-id: 57e37b5850

src/builder/DdJaniModelBuilder.cpp

@@ -437,7 +437,7 @@ namespace storm {
                 }
             }
             
-            transitions *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationId()).template toAdd<ValueType>();
+            transitions *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd<ValueType>();
             
             return EdgeDestinationDd<Type, ValueType>(transitions, assignedGlobalVariables);
         }
@@ -841,7 +841,7 @@ namespace storm {
                     // If the edge is not labeled with the silent action, we have to analyze which portion of the global
                     // variables was written by any of the updates and make all update results equal w.r.t. this set. If
                     // the edge is labeled with the silent action, we can already multiply the identities of all global variables.
-                    if (edge.getActionId() != this->model.getSilentActionIndex()) {
+                    if (edge.getActionIndex() != this->model.getSilentActionIndex()) {
                         for (auto const& edgeDestinationDd : destinationDds) {
                             globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end());
                         }
@@ -867,7 +867,7 @@ namespace storm {
                     }
                     
                     // Add the source location and the guard.
-                    transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd<ValueType>() * guard;
+                    transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
                     
                     // If we multiply the ranges of global variables, make sure everything stays within its bounds.
                     if (!globalVariablesInSomeUpdate.empty()) {
@@ -895,7 +895,7 @@ namespace storm {
                     // Build the edge and add it if it adds transitions.
                     EdgeDd edgeDd = buildEdgeDd(automaton, edge);
                     if (!edgeDd.guard.isZero()) {
-                        result.actionIndexToEdges[edge.getActionId()].push_back(edgeDd);
+                        result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd);
                     }
                 }
                 
@@ -1271,7 +1271,7 @@ namespace storm {
                     // If the edge is not labeled with the silent action, we have to analyze which portion of the global
                     // variables was written by any of the updates and make all update results equal w.r.t. this set. If
                     // the edge is labeled with the silent action, we can already multiply the identities of all global variables.
-                    if (edge.getActionId() != this->model.getSilentActionIndex()) {
+                    if (edge.getActionIndex() != this->model.getSilentActionIndex()) {
                         for (auto const& edgeDestinationDd : destinationDds) {
                             globalVariablesInSomeDestination.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end());
                         }
@@ -1297,7 +1297,7 @@ namespace storm {
                     }
                     
                     // Add the source location and the guard.
-                    transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd<ValueType>() * guard;
+                    transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
                     
                     // If we multiply the ranges of global variables, make sure everything stays within its bounds.
                     if (!globalVariablesInSomeDestination.empty()) {
@@ -1319,7 +1319,7 @@ namespace storm {
                 // Translate the individual edges.
                 std::vector<EdgeDd> edgeDds;
                 for (auto const& edge : automaton.getEdges()) {
-                    if (edge.getActionId() == actionIndex) {
+                    if (edge.getActionIndex() == actionIndex) {
                         edgeDds.push_back(buildEdgeDd(automaton, edge));
                     }
                 }

src/generator/JaniNextStateGenerator.cpp

@@ -24,6 +24,7 @@ namespace storm {
         JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), VariableInformation(model), options), model(model) {
             STORM_LOG_THROW(!this->model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
             STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models.");
+            STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
             
             // If there are terminal states we need to handle, we now need to translate all labels to expressions.
             if (this->options.hasTerminalStates()) {
@@ -53,6 +54,11 @@ namespace storm {
         bool JaniNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
             return model.isDeterministicModel();
         }
+        
+        template<typename ValueType, typename StateType>
+        bool JaniNextStateGenerator<ValueType, StateType>::isDiscreteTimeModel() const {
+            return model.isDiscreteTimeModel();
+        }
 
         template<typename ValueType, typename StateType>
         std::vector<StateType> JaniNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
@@ -104,6 +110,11 @@ namespace storm {
         CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) {
             CompressedState newState(state);
             
+            // NOTE: the following process assumes that the assignments of the destination are ordered in such a way
+            // that the assignments to boolean variables precede the assignments to all integer variables and that
+            // within the types, the assignments to variables are ordered (in ascending order) by the expression variables.
+            // This is guaranteed for JANI models, by sorting the assignments as soon as an edge destination is created.
+            
             auto assignmentIt = destination.getAssignments().begin();
             auto assignmentIte = destination.getAssignments().end();
             
@@ -136,12 +147,114 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         StateBehavior<ValueType, StateType> JaniNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
+            // Prepare the result, in case we return early.
+            StateBehavior<ValueType, StateType> result;
+            
+            // If a terminal expression was set and we must not expand this state, return now.
+            if (!this->terminalStates.empty()) {
+                for (auto const& expressionBool : this->terminalStates) {
+                    if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) {
+                        return result;
+                    }
+                }
+            }
             
+            // Get all choices for the state.
+            std::vector<Choice<ValueType>> allChoices = getSilentActionChoices(*this->state, stateToIdCallback);
+            std::vector<Choice<ValueType>> allLabeledChoices = getNonsilentActionChoices(*this->state, stateToIdCallback);
+            for (auto& choice : allLabeledChoices) {
+                allChoices.push_back(std::move(choice));
+            }
+            
+            std::size_t totalNumberOfChoices = allChoices.size();
+            
+            // If there is not a single choice, we return immediately, because the state has no behavior (other than
+            // the state reward).
+            if (totalNumberOfChoices == 0) {
+                return result;
+            }
+            
+            // If the model is a deterministic model, we need to fuse the choices into one.
+            if (this->isDeterministicModel() && totalNumberOfChoices > 1) {
+                Choice<ValueType> globalChoice;
+                
+                // Iterate over all choices and combine the probabilities/rates into one choice.
+                for (auto const& choice : allChoices) {
+                    for (auto const& stateProbabilityPair : choice) {
+                        if (this->isDiscreteTimeModel()) {
+                            globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second / totalNumberOfChoices);
+                        } else {
+                            globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second);
+                        }
+                    }
+                    
+                    if (this->options.isBuildChoiceLabelsSet()) {
+                        globalChoice.addChoiceLabels(choice.getChoiceLabels());
+                    }
+                }
+                
+                // Move the newly fused choice in place.
+                allChoices.clear();
+                allChoices.push_back(std::move(globalChoice));
+            }
+            
+            // Move all remaining choices in place.
+            for (auto& choice : allChoices) {
+                result.addChoice(std::move(choice));
+            }
+            
+            result.setExpanded();
+            return result;
         }
         
         template<typename ValueType, typename StateType>
         std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
+            std::vector<Choice<ValueType>> result;
+            
+            // Iterate over all automata.
+            auto locationVariableIt = this->variableInformation.locationVariables.begin();
+            for (auto const& automaton : model.getAutomata()) {
+                
+                // Determine the location of the automaton in the given state.
+                uint64_t locationIndex = state.getAsInt(locationVariableIt->bitOffset, locationVariableIt->bitWidth);
+                
+                // Iterate over all edges from the source location.
+                for (auto const& edge : automaton.getEdgesFromLocation(locationIndex)) {
+                    // Skip the edge if it is labeled with a non-silent action.
+                    if (edge.getActionIndex() != model.getSilentActionIndex()) {
+                        continue;
+                    }
+                    
+                    // Skip the command, if it is not enabled.
+                    if (!this->evaluator.asBool(edge.getGuard())) {
+                        continue;
+                    }
+                    
+                    result.push_back(Choice<ValueType>(edge.getActionIndex()));
+                    Choice<ValueType>& choice = result.back();
+                    
+                    // Iterate over all updates of the current command.
+                    ValueType probabilitySum = storm::utility::zero<ValueType>();
+                    for (auto const& destination : edge.getDestinations()) {
+                        // Obtain target state index and add it to the list of known states. If it has not yet been
+                        // seen, we also add it to the set of states that have yet to be explored.
+                        StateType stateIndex = stateToIdCallback(applyUpdate(state, destination));
+                        
+                        // Update the choice by adding the probability/target state to it.
+                        ValueType probability = this->evaluator.asRational(destination.getProbability());
+                        choice.addProbability(stateIndex, probability);
+                        probabilitySum += probability;
+                    }
+                    
+                    // Check that the resulting distribution is in fact a distribution.
+                    STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ").");
+                }
+                
+                // After we have processed all edges of the current automaton, move to the next location variable.
+                ++locationVariableIt;
+            }
             
+            return result;
         }
         
         template<typename ValueType, typename StateType>

src/generator/JaniNextStateGenerator.h

@@ -16,6 +16,7 @@ namespace storm {
             
             virtual ModelType getModelType() const override;
             virtual bool isDeterministicModel() const override;
+            virtual bool isDiscreteTimeModel() const override;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
             
             virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;

src/generator/NextStateGenerator.h

@@ -165,6 +165,7 @@ namespace storm {
             uint64_t getStateSize() const;
             virtual ModelType getModelType() const = 0;
             virtual bool isDeterministicModel() const = 0;
+            virtual bool isDiscreteTimeModel() const = 0;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
             
             void load(CompressedState const& state);

src/generator/PrismNextStateGenerator.cpp

@@ -82,6 +82,11 @@ namespace storm {
             return program.isDeterministicModel();
         }
         
+        template<typename ValueType, typename StateType>
+        bool PrismNextStateGenerator<ValueType, StateType>::isDiscreteTimeModel() const {
+            return program.isDiscreteTimeModel();
+        }
+        
         template<typename ValueType, typename StateType>
         std::vector<StateType> PrismNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
             // Prepare an SMT solver to enumerate all initial states.
@@ -172,24 +177,24 @@ namespace storm {
             }
             
             // If the model is a deterministic model, we need to fuse the choices into one.
-            if (program.isDeterministicModel() && totalNumberOfChoices > 1) {
+            if (this->isDeterministicModel() && totalNumberOfChoices > 1) {
                 Choice<ValueType> globalChoice;
                 
                 // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
                 // this is equal to the number of choices, which is why we initialize it like this here.
-                ValueType totalExitRate = program.isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
+                ValueType totalExitRate = this->isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
                 
                 // Iterate over all choices and combine the probabilities/rates into one choice.
                 for (auto const& choice : allChoices) {
                     for (auto const& stateProbabilityPair : choice) {
-                        if (program.isDiscreteTimeModel()) {
+                        if (this->isDiscreteTimeModel()) {
                             globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second / totalNumberOfChoices);
                         } else {
                             globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second);
                         }
                     }
                     
-                    if (hasStateActionRewards && !program.isDiscreteTimeModel()) {
+                    if (hasStateActionRewards && !this->isDiscreteTimeModel()) {
                         totalExitRate += choice.getTotalMass();
                     }
                     

src/generator/PrismNextStateGenerator.h

@@ -17,6 +17,7 @@ namespace storm {
             
             virtual ModelType getModelType() const override;
             virtual bool isDeterministicModel() const override;
+            virtual bool isDiscreteTimeModel() const override;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
 
             virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;

src/generator/VariableInformation.cpp

@@ -17,6 +17,10 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        LocationVariableInformation::LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) {
+            // Intentionally left empty.
+        }
+        
         VariableInformation::VariableInformation(storm::prism::Program const& program) : totalBitOffset(0) {
             for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
                 booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset);
@@ -42,7 +46,7 @@ namespace storm {
                     totalBitOffset += bitwidth;
                 }
             }
-
+            
             sortVariables();
         }
         
@@ -59,6 +63,10 @@ namespace storm {
                 totalBitOffset += bitwidth;
             }
             for (auto const& automaton : model.getAutomata()) {
+                uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
+                locationVariables.emplace_back(automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
+                totalBitOffset += bitwidth;
+                
                 for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
                     booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
                     ++totalBitOffset;

src/generator/VariableInformation.h

@@ -17,7 +17,7 @@ namespace storm {
     
     namespace generator {
         
-        // A structure storing information about the boolean variables of the program.
+        // A structure storing information about the boolean variables of the model.
         struct BooleanVariableInformation {
             BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset);
             
@@ -28,7 +28,7 @@ namespace storm {
             uint_fast64_t bitOffset;
         };
         
-        // A structure storing information about the integer variables of the program.
+        // A structure storing information about the integer variables of the model.
         struct IntegerVariableInformation {
             IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
             
@@ -48,6 +48,20 @@ namespace storm {
             uint_fast64_t bitWidth;
         };
         
+        // A structure storing information about the location variables of the model.
+        struct LocationVariableInformation {
+            LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
+
+            // The highest possible location value.
+            uint64_t highestValue;
+            
+            // Its bit offset in the compressed state.
+            uint_fast64_t bitOffset;
+            
+            // Its bit width in the compressed state.
+            uint_fast64_t bitWidth;
+        };
+        
         // A structure storing information about the used variables of the program.
         struct VariableInformation {
             VariableInformation(storm::prism::Program const& program);
@@ -56,13 +70,16 @@ namespace storm {
             VariableInformation() = default;
             uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;
             
-            // The total bit offset over all variables.
+            /// The total bit offset over all variables.
             uint_fast64_t totalBitOffset;
             
-            // The known boolean variables.
+            /// The location variables.
+            std::vector<LocationVariableInformation> locationVariables;
+            
+            /// The boolean variables.
             std::vector<BooleanVariableInformation> booleanVariables;
             
-            // The known integer variables.
+            /// The integer variables.
             std::vector<IntegerVariableInformation> integerVariables;
             
         private:

src/models/sparse/Model.h

@@ -342,7 +342,7 @@ namespace storm {
                  * @param out The stream the information is to be printed to.
                  */
                 void printRewardModelsInformationToStream(std::ostream& out) const;
-                
+                                
             private:
                 //  A matrix representing transition relation.
                 storm::storage::SparseMatrix<ValueType> transitionMatrix;

src/storage/jani/Automaton.cpp

@@ -90,7 +90,7 @@ namespace storm {
             return locations.size() - 1;
         }
 
-        uint64_t Automaton::getLocationId(std::string const& name) const {
+        uint64_t Automaton::getLocationIndex(std::string const& name) const {
             assert(hasLocation(name));
             return locationToIndex.at(name);
         }
@@ -143,20 +143,20 @@ namespace storm {
         }
         
         void Automaton::addEdge(Edge const& edge) {
-            STORM_LOG_THROW(edge.getSourceLocationId() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationId() << "'.");
+            STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'.");
             
             // Find the right position for the edge and insert it properly.
             auto posIt = edges.begin();
-            std::advance(posIt, locationToStartingIndex[edge.getSourceLocationId() + 1]);
+            std::advance(posIt, locationToStartingIndex[edge.getSourceLocationIndex() + 1]);
             edges.insert(posIt, edge);
             
             // Now update the starting indices of all subsequent locations.
-            for (uint64_t locationIndex = edge.getSourceLocationId() + 1; locationIndex < locationToStartingIndex.size(); ++locationIndex) {
+            for (uint64_t locationIndex = edge.getSourceLocationIndex() + 1; locationIndex < locationToStartingIndex.size(); ++locationIndex) {
                 ++locationToStartingIndex[locationIndex];
             }
             
             // Update the set of action indices of this automaton.
-            actionIndices.insert(edge.getActionId());
+            actionIndices.insert(edge.getActionIndex());
         }
         
         std::vector<Edge>& Automaton::getEdges() {
@@ -170,7 +170,7 @@ namespace storm {
         std::set<uint64_t> Automaton::getActionIndices() const {
             std::set<uint64_t> result;
             for (auto const& edge : edges) {
-                result.insert(edge.getActionId());
+                result.insert(edge.getActionIndex());
             }
             return result;
         }

src/storage/jani/Automaton.h

@@ -123,7 +123,7 @@ namespace storm {
              *
              * @name the name of the location
              */
-            uint64_t getLocationId(std::string const& name) const;
+            uint64_t getLocationIndex(std::string const& name) const;
             
             /*!
              * Retrieves the locations of the automaton.

src/storage/jani/CompositionInformationVisitor.cpp

@@ -15,15 +15,26 @@ namespace storm {
         }
         
         void CompositionInformation::addNonsilentAction(std::string const& actionName) {
-            // FIXME
+            nonsilentActions.insert(actionName);
         }
         
         std::set<std::string> const& CompositionInformation::getNonsilentActions() const {
-            // FIXME
+            return nonsilentActions;
         }
         
-        void CompositionInformation::renameNonsilentActions(std::map<std::string, std::string> const& renaming) {
+        std::set<std::string> CompositionInformation::renameNonsilentActions(std::set<std::string> const& nonsilentActions, std::map<std::string, boost::optional<std::string>> const& renaming) {
-            // FIXME
+            std::set<std::string> newNonsilentActions;
+            for (auto const& entry : nonsilentActions) {
+                auto it = renaming.find(entry);
+                if (it != renaming.end()) {
+                    if (it->second) {
+                        newNonsilentActions.insert(it->second.get());
+                    }
+                } else {
+                    newNonsilentActions.insert(entry);
+                }
+            }
+            return newNonsilentActions;
         }
         
         void CompositionInformation::setContainsRenameComposition() {
@@ -59,19 +70,26 @@ namespace storm {
         }
         
         boost::any CompositionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) {
+            Model const& model = boost::any_cast<Model const&>(data);
+            Automaton const& automaton = model.getAutomaton(composition.getAutomatonName());
+            
             CompositionInformation result;
             result.increaseAutomatonMultiplicity(composition.getAutomatonName());
+            for (auto const& actionIndex : automaton.getActionIndices()) {
+                if (actionIndex != model.getSilentActionIndex()) {
+                    result.addNonsilentAction(model.getAction(actionIndex).getName());
+                }
+            }
             return result;
         }
         
         boost::any CompositionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) {
             CompositionInformation subresult = boost::any_cast<CompositionInformation>(composition.getSubcomposition().accept(*this, data));
-            subresult.setContainsRenameComposition();
+            std::set<std::string> nonsilentActions = CompositionInformation::renameNonsilentActions(subresult.getNonsilentActions(), composition.getRenaming());
-            return subresult;
+            return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsRestrictedParallelComposition());
         }
         
         boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) {
-            Model const& model = boost::any_cast<Model const&>(data);
             CompositionInformation left = boost::any_cast<CompositionInformation>(composition.getLeftSubcomposition().accept(*this, data));
             CompositionInformation right = boost::any_cast<CompositionInformation>(composition.getRightSubcomposition().accept(*this, data));
 
@@ -80,12 +98,19 @@ namespace storm {
             bool containsRestrictedParallelComposition = left.containsRestrictedParallelComposition() || right.containsRestrictedParallelComposition();
             std::map<std::string, uint64_t> joinedAutomatonToMultiplicity = CompositionInformation::joinMultiplicityMaps(left.getAutomatonToMultiplicityMap(), right.getAutomatonToMultiplicityMap());
             
+            std::set<std::string> nonsilentActions;
+            std::set_union(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(nonsilentActions, nonsilentActions.begin()));
+            
             // If there was no restricted parallel composition yet, maybe the current composition is one, so check it.
             if (!containsRestrictedParallelComposition) {
-                // FIXME.
+                std::set<std::string> commonNonsilentActions;
+                std::set_intersection(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(commonNonsilentActions, commonNonsilentActions.begin()));
+                if (commonNonsilentActions != composition.getSynchronizationAlphabet()) {
+                    containsRestrictedParallelComposition = true;
+                }
             }
             
-            return CompositionInformation(joinedAutomatonToMultiplicity, containsRenameComposition, containsRestrictedParallelComposition);
+            return CompositionInformation(joinedAutomatonToMultiplicity, nonsilentActions, containsRenameComposition, containsRestrictedParallelComposition);
         }
         
     }

src/storage/jani/CompositionInformationVisitor.h

@@ -4,6 +4,8 @@
 #include <set>
 #include <cstdint>
 
+#include <boost/optional.hpp>
+
 #include "src/storage/jani/CompositionVisitor.h"
 
 namespace storm {
@@ -20,7 +22,7 @@ namespace storm {
             
             void addNonsilentAction(std::string const& actionName);
             std::set<std::string> const& getNonsilentActions() const;
-            void renameNonsilentActions(std::map<std::string, std::string> const& renaming);
+            static std::set<std::string> renameNonsilentActions(std::set<std::string> const& nonsilentActions, std::map<std::string, boost::optional<std::string>> const& renaming);
             
             void setContainsRenameComposition();
             bool containsRenameComposition() const;

src/storage/jani/Edge.cpp

@@ -3,16 +3,16 @@
 namespace storm {
     namespace jani {
         
-        Edge::Edge(uint64_t sourceLocationId, uint64_t actionId, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations) : sourceLocationId(sourceLocationId), actionId(actionId), rate(rate), guard(guard), destinations(destinations) {
+        Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), guard(guard), destinations(destinations) {
             // Intentionally left empty.
         }
         
-        uint64_t Edge::getSourceLocationId() const {
+        uint64_t Edge::getSourceLocationIndex() const {
-            return sourceLocationId;
+            return sourceLocationIndex;
         }
         
-        uint64_t Edge::getActionId() const {
+        uint64_t Edge::getActionIndex() const {
-            return actionId;
+            return actionIndex;
         }
         
         bool Edge::hasRate() const {

src/storage/jani/Edge.h

@@ -9,17 +9,17 @@ namespace storm {
         
         class Edge {
         public:
-            Edge(uint64_t sourceLocationId, uint64_t actionId, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations = {});
+            Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations = {});
             
             /*!
-             * Retrieves the id of the source location.
+             * Retrieves the index of the source location.
              */
-            uint64_t getSourceLocationId() const;
+            uint64_t getSourceLocationIndex() const;
             
             /*!
              * Retrieves the id of the action with which this edge is labeled.
              */
-            uint64_t getActionId() const;
+            uint64_t getActionIndex() const;
             
             /*!
              * Retrieves whether this edge has an associated rate.
@@ -62,11 +62,11 @@ namespace storm {
             void addDestination(EdgeDestination const& destination);
             
         private:
-            // The id of the source location.
+            // The index of the source location.
-            uint64_t sourceLocationId;
+            uint64_t sourceLocationIndex;
             
-            // The id of the action with which this edge is labeled.
+            // The index of the action with which this edge is labeled.
-            uint64_t actionId;
+            uint64_t actionIndex;
             
             // The rate with which this edge is taken. This only applies to continuous-time models. For discrete-time
             // models, this must be set to none.

src/storage/jani/EdgeDestination.cpp

@@ -6,7 +6,7 @@
 namespace storm {
     namespace jani {
         
-        EdgeDestination::EdgeDestination(uint64_t locationId, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments, std::vector<RewardIncrement> const& rewardIncrements) : locationId(locationId), probability(probability), assignments(assignments), rewardIncrements(rewardIncrements) {
+        EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments, std::vector<RewardIncrement> const& rewardIncrements) : locationIndex(locationIndex), probability(probability), assignments(assignments), rewardIncrements(rewardIncrements) {
             sortAssignments();
         }
         
@@ -23,8 +23,8 @@ namespace storm {
             rewardIncrements.push_back(rewardIncrement);
         }
         
-        uint64_t EdgeDestination::getLocationId() const {
+        uint64_t EdgeDestination::getLocationIndex() const {
-            return locationId;
+            return locationIndex;
         }
         
         storm::expressions::Expression const& EdgeDestination::getProbability() const {

src/storage/jani/EdgeDestination.h

@@ -15,7 +15,7 @@ namespace storm {
             /*!
              * Creates a new edge destination.
              */
-            EdgeDestination(uint64_t locationId, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments = {}, std::vector<RewardIncrement> const& rewardIncrements = {});
+            EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments = {}, std::vector<RewardIncrement> const& rewardIncrements = {});
             
             /*!
              * Additionally performs the given assignment when choosing this destination.
@@ -30,7 +30,7 @@ namespace storm {
             /*!
              * Retrieves the id of the destination location.
              */
-            uint64_t getLocationId() const;
+            uint64_t getLocationIndex() const;
             
             /*!
              * Retrieves the probability of choosing this destination.
@@ -64,8 +64,8 @@ namespace storm {
              */
             void sortAssignments();
             
-            // The id of the destination location.
+            // The index of the destination location.
-            uint64_t locationId;
+            uint64_t locationIndex;
 
             // The probability to go to the destination.
             storm::expressions::Expression probability;

src/storage/jani/Exporter.cpp

@@ -242,7 +242,7 @@ namespace storm {
             
             appendIndent(out, indent + 1);
             appendField(out, "location");
-            appendValue(out, automaton.getLocation(destination.getLocationId()).getName());
+            appendValue(out, automaton.getLocation(destination.getLocationIndex()).getName());
             out << ",";
             clearLine(out);
             
@@ -275,13 +275,13 @@ namespace storm {
             
             appendIndent(out, indent + 1);
             appendField(out, "location");
-            appendValue(out, automaton.getLocation(edge.getSourceLocationId()).getName());
+            appendValue(out, automaton.getLocation(edge.getSourceLocationIndex()).getName());
             out << ",";
             clearLine(out);
             
             appendIndent(out, indent + 1);
             appendField(out, "action");
-            appendValue(out, model.getAction(edge.getActionId()).getName());
+            appendValue(out, model.getAction(edge.getActionIndex()).getName());
             out << ",";
             clearLine(out);
             

src/storage/jani/Model.cpp

@@ -2,9 +2,8 @@
 
 #include "src/storage/expressions/ExpressionManager.h"
 
-#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/Compositions.h"
-#include "src/storage/jani/ParallelComposition.h"
+#include "src/storage/jani/CompositionInformationVisitor.h"
-#include "src/storage/jani/RenameComposition.h"
 
 #include "src/utility/macros.h"
 #include "src/exceptions/WrongFormatException.h"
@@ -357,6 +356,10 @@ namespace storm {
             return this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::CTMC;
         }
         
+        bool Model::isDiscreteTimeModel() const {
+            return this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP;
+        }
+        
         std::vector<storm::expressions::Expression> Model::getAllRangeExpressions() const {
             std::vector<storm::expressions::Expression> result;
             for (auto const& variable : this->getGlobalVariables().getBoundedIntegerVariables()) {
@@ -392,5 +395,19 @@ namespace storm {
             
         }
         
+        bool Model::hasDefaultComposition() const {
+            CompositionInformationVisitor visitor;
+            CompositionInformation info = visitor.getInformation(this->getSystemComposition(), *this);
+            if (info.containsRestrictedParallelComposition() || info.containsRenameComposition()) {
+                return false;
+            }
+            for (auto const& multiplicity : info.getAutomatonToMultiplicityMap()) {
+                if (multiplicity.second > 1) {
+                    return false;
+                }
+            }
+            return true;
+        }
+        
     }
 }

src/storage/jani/Model.h

@@ -248,11 +248,22 @@ namespace storm {
              */
             bool isDeterministicModel() const;
             
+            /*!
+             * Determines whether this model is a discrete-time model.
+             */
+            bool isDiscreteTimeModel() const;
+            
             /*!
              * Retrieves a list of expressions that characterize the legal values of the variables in this model.
              */
             std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
             
+            /*!
+             * Retrieves whether this model has the default composition, that is it composes all automata in parallel
+             * and synchronizes over all common actions.
+             */
+            bool hasDefaultComposition() const;
+            
             /*!
              *  Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
              */

src/storage/jani/RewardIncrement.cpp

@@ -3,9 +3,17 @@
 namespace storm {
     namespace jani {
         
-        RewardIncrement::RewardIncrement(uint64_t rewardId, storm::expressions::Expression const& value) : rewardId(rewardId), value(value) {
+        RewardIncrement::RewardIncrement(uint64_t rewardIndex, storm::expressions::Expression const& value) : rewardIndex(rewardIndex), value(value) {
             // Intentionally left empty.
         }
         
+        uint64_t RewardIncrement::getRewardIndex() const {
+            return rewardIndex;
+        }
+        
+        storm::expressions::Expression const& RewardIncrement::getValue() const {
+            return value;
+        }
+        
     }
 }

src/storage/jani/RewardIncrement.h

@@ -10,16 +10,26 @@ namespace storm {
         class RewardIncrement {
         public:
             /*!
-             * Creates an increment of a reward (given by its id) by the given expression.
+             * Creates an increment of a reward (given by its index) by the given expression.
              *
-             * @param rewardId The id of the reward to increment.
+             * @param rewardIndex The index of the reward to increment.
              * @param value The expression defining the amount the reward is the incremented.
              */
-            RewardIncrement(uint64_t rewardId, storm::expressions::Expression const& value);
+            RewardIncrement(uint64_t rewardIndex, storm::expressions::Expression const& value);
+
+            /*!
+             * Retrieves the index of the reward to increment.
+             */
+            uint64_t getRewardIndex() const;
+            
+            /*!
+             * Retrieves the expression defining the amount by which the reward is to be incremented.
+             */
+            storm::expressions::Expression const& getValue() const;
             
         private:
-            // The id of the reward that is to be incremented.
+            // The index of the reward that is to be incremented.
-            uint64_t rewardId;
+            uint64_t rewardIndex;
             
             // The expression defining the amount the reward is to be incremented.
             storm::expressions::Expression value;