Simplifying index levels

src/storm-gspn/builder/JaniGSPNBuilder.cpp

@@ -109,7 +109,9 @@ namespace storm {
                     probabilities.emplace_back(storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)));
                 }
 
-                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge((priorityGuard && guard).simplify());
+                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>((priorityGuard && guard).simplify());
+                automaton.registerTemplateEdge(templateEdge);
+
                 for (auto const& oa : oas) {
                     templateEdge->addDestination(storm::jani::TemplateEdgeDestination(oa));
                 }
@@ -139,7 +141,9 @@ namespace storm {
                     }
                 }
 
-                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(guard);
+                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(guard);
+                automaton.registerTemplateEdge(templateEdge);
+
                 templateEdge->addDestination(assignments);
                 storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans.getRate()), templateEdge, {locId}, {expressionManager->integer(1)});
                 automaton.addEdge(e);

src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp

@@ -118,7 +118,8 @@ namespace storm {
                                 assert(userVariableRestrictions.at(assignment.first).hasLeftBound() && userVariableRestrictions.at(assignment.first).hasRightBound());
                                 storm::expressions::Expression newCondition = simplifyExpression(edge.getCondition() && (assignment.second > bound.getRightBound().get() || assignment.second < bound.getLeftBound().get()));
                                 
-                                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(newCondition);
+                                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(newCondition);
+                                automaton.registerTemplateEdge(templateEdge);
                                 templateEdge->addDestination(storm::jani::TemplateEdgeDestination());
                                 storm::jani::Edge e(janiLocId.at(edge.getSourceId()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, {varOutOfBoundsLocations.at(assignment.first)}, {expManager->rational(1.0)});
                                 edges.push_back(e);
@@ -136,7 +137,8 @@ namespace storm {
             for(auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) {
                 ppg::ProgramLocation const& loc = it->second;
                 if (loc.nrOutgoingEdgeGroups() == 0) {
-                    std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(expManager->boolean(true));
+                    std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(expManager->boolean(true));
+                    automaton.registerTemplateEdge(templateEdge);
                     templateEdge->addDestination(storm::jani::TemplateEdgeDestination());
                     storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, {janiLocId.at(loc.id())}, {expManager->rational(1.0)});
                     automaton.addEdge(e);
@@ -146,7 +148,9 @@ namespace storm {
                         for(auto const& check : checks.first) {
                             automaton.addEdge(check);
                         }
-                        std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(simplifyExpression(edge->getCondition() && checks.second));
+                        std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(simplifyExpression(edge->getCondition() && checks.second));
+                        automaton.registerTemplateEdge(templateEdge);
+
                         std::vector<std::pair<uint64_t, storm::expressions::Expression>> destinationLocationsAndProbabilities = buildDestinations(automaton, *edge, *templateEdge);
 
                         storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, destinationLocationsAndProbabilities);
@@ -158,7 +162,9 @@ namespace storm {
                     {
                         STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Combi of nondeterminism and probabilistic choices within a loc not supported yet");
                     } else {
-                        std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(expManager->boolean(true));
+                        std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(expManager->boolean(true));
+                        automaton.registerTemplateEdge(templateEdge);
+
 
                         std::vector<storm::expressions::Expression> destinationProbabilities;
                         std::vector<uint64_t> destinationLocations;

src/storm/parser/JaniParser.cpp

@@ -138,6 +138,7 @@ namespace storm {
                     }
                 }
             }
+            model.finalize();
             return {model, properties};
         }
 
@@ -1039,7 +1040,7 @@ namespace storm {
                 }
                 assert(guardExpr.isInitialized());
                 
-                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(guardExpr);
+                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(guardExpr);
                 
                 STORM_LOG_THROW(edgeEntry.count("destinations") == 1, storm::exceptions::InvalidJaniException, "A single list of destinations must be given in edge from '" << sourceLoc << "' in automaton '" << name << "'");
                 std::vector<std::pair<uint64_t, storm::expressions::Expression>> destinationLocationsAndProbabilities;

src/storm/storage/jani/Automaton.cpp

@@ -297,10 +297,7 @@ namespace storm {
             return ConstEdges(it1, it2);
         }
         
-        std::shared_ptr<TemplateEdge> Automaton::createTemplateEdge(storm::expressions::Expression const& guard) {
-            templateEdges.emplace_back(std::make_shared<TemplateEdge>(guard));
-            return templateEdges.back();
-        }
+
         
         void Automaton::addEdge(Edge const& edge) {
             STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'.");
@@ -430,7 +427,10 @@ namespace storm {
                 edge.substitute(substitution);
             }
         }
-        
+        void Automaton::registerTemplateEdge(std::shared_ptr<TemplateEdge> const& te) {
+            templateEdges.insert(te);
+        }
+
         void Automaton::changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) {
             for (auto& location : locations) {
                 location.changeAssignmentVariables(remapping);
@@ -441,6 +441,11 @@ namespace storm {
         }
         
         void Automaton::finalize(Model const& containingModel) {
+            simplifyIndexedAssignments();
+            templateEdges.clear();
+            for (auto& edge : edges) {
+                templateEdges.insert(edge.getTemplateEdge());
+            }
             for (auto& templateEdge : templateEdges) {
                 templateEdge->finalize(containingModel);
             }
@@ -489,7 +494,13 @@ namespace storm {
                 templateEdge->liftTransientDestinationAssignments();
             }
         }
-        
+
+        void Automaton::simplifyIndexedAssignments() {
+            for (auto& edge : edges) {
+                edge.simplifyIndexedAssignments(variables);
+            }
+        }
+
         bool Automaton::usesAssignmentLevels() const {
             for (auto const& edge : this->getEdges()) {
                 if (edge.usesAssignmentLevels()) {

src/storm/storage/jani/Automaton.h

@@ -248,10 +248,10 @@ namespace storm {
             ConstEdges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const;
             
             /*!
-             * Creates a new template edge that can be used to create new edges.
+             * Adds the template edge to the list of edges
              */
-            std::shared_ptr<TemplateEdge> createTemplateEdge(storm::expressions::Expression const& guard);
-            
+            void registerTemplateEdge(std::shared_ptr<TemplateEdge> const&);
+
             /*!
              * Adds an edge to the automaton.
              */
@@ -363,6 +363,8 @@ namespace storm {
              * Retrieves whether the automaton uses an assignment level other than zero.
              */
             bool usesAssignmentLevels() const;
+
+            void simplifyIndexedAssignments();
             
             /*!
              * Checks the automaton for linearity.
@@ -389,7 +391,7 @@ namespace storm {
             std::vector<Edge> edges;
             
             /// The templates for the contained edges.
-            std::vector<std::shared_ptr<TemplateEdge>> templateEdges;
+            std::unordered_set<std::shared_ptr<TemplateEdge>> templateEdges;
             
             /// A mapping from location indices to the starting indices. If l is mapped to i, it means that the edges
             /// leaving location l start at index i of the edges vector.

src/storm/storage/jani/Edge.cpp

@@ -10,7 +10,7 @@
 namespace storm {
     namespace jani {
         
-        Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, std::shared_ptr<TemplateEdge const> const& templateEdge, std::vector<std::pair<uint64_t, storm::expressions::Expression>> const& destinationTargetLocationsAndProbabilities) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), templateEdge(templateEdge) {
+        Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, std::shared_ptr<TemplateEdge> const& templateEdge, std::vector<std::pair<uint64_t, storm::expressions::Expression>> const& destinationTargetLocationsAndProbabilities) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), templateEdge(templateEdge) {
             
             // Create the concrete destinations from the template edge.
             STORM_LOG_THROW(templateEdge->getNumberOfDestinations() == destinationTargetLocationsAndProbabilities.size(), storm::exceptions::InvalidArgumentException, "Sizes of template edge destinations and target locations mismatch.");
@@ -20,7 +20,7 @@ namespace storm {
             }
         }
         
-        Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, std::shared_ptr<TemplateEdge const> const& templateEdge, std::vector<uint64_t> const& destinationLocations, std::vector<storm::expressions::Expression> const& destinationProbabilities) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), templateEdge(templateEdge) {
+        Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, std::shared_ptr<TemplateEdge> const& templateEdge, std::vector<uint64_t> const& destinationLocations, std::vector<storm::expressions::Expression> const& destinationProbabilities) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), templateEdge(templateEdge) {
 
             // Create the concrete destinations from the template edge.
             STORM_LOG_THROW(templateEdge->getNumberOfDestinations() == destinationLocations.size() && destinationLocations.size() == destinationProbabilities.size(), storm::exceptions::InvalidArgumentException, "Sizes of template edge destinations and target locations mismatch.");
@@ -102,5 +102,21 @@ namespace storm {
         bool Edge::usesAssignmentLevels() const {
             return templateEdge->usesAssignmentLevels();
         }
+
+        void Edge::simplifyIndexedAssignments(VariableSet const& localVars) {
+            if(usesAssignmentLevels()) {
+                templateEdge = std::make_shared<TemplateEdge>(templateEdge->simplifyIndexedAssignments(!hasSilentAction(), localVars));
+                std::vector<EdgeDestination> newdestinations;
+                for (uint64_t i = 0; i < templateEdge->getNumberOfDestinations(); ++i) {
+                    auto const& templateDestination = templateEdge->getDestination(i);
+                    newdestinations.emplace_back(destinations[i].getLocationIndex(), destinations[i].getProbability(), templateDestination);
+                }
+                destinations = newdestinations;
+            }
+        }
+
+        std::shared_ptr<TemplateEdge> const& Edge::getTemplateEdge() {
+            return templateEdge;
+        }
     }
 }

src/storm/storage/jani/Edge.h

@@ -17,8 +17,8 @@ namespace storm {
         public:
             Edge() = default;
             
-            Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, std::shared_ptr<TemplateEdge const> const& templateEdge, std::vector<std::pair<uint64_t, storm::expressions::Expression>> const& destinationTargetLocationsAndProbabilities);
-            Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, std::shared_ptr<TemplateEdge const> const& templateEdge, std::vector<uint64_t> const& destinationLocations, std::vector<storm::expressions::Expression> const& destinationProbabilities);
+            Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, std::shared_ptr<TemplateEdge> const& templateEdge, std::vector<std::pair<uint64_t, storm::expressions::Expression>> const& destinationTargetLocationsAndProbabilities);
+            Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, std::shared_ptr<TemplateEdge> const& templateEdge, std::vector<uint64_t> const& destinationLocations, std::vector<storm::expressions::Expression> const& destinationProbabilities);
             
             /*!
              * Retrieves the index of the source location.
@@ -104,6 +104,14 @@ namespace storm {
              * Retrieves whether the edge uses an assignment level other than zero.
              */
             bool usesAssignmentLevels() const;
+
+            /*!
+             *
+             * @param localVars
+             */
+            void simplifyIndexedAssignments(VariableSet const& localVars);
+
+            std::shared_ptr<TemplateEdge> const& getTemplateEdge();
             
         private:
             /// The index of the source location.
@@ -116,8 +124,8 @@ namespace storm {
             /// models, this must be set to none.
             boost::optional<storm::expressions::Expression> rate;
             
-            /// The template of this edge: guards and destinations.
-            std::shared_ptr<TemplateEdge const> templateEdge;
+            /// The template of this edge: guards and destinations. Notice that after finalizing, the template edge might be reused; changing it is not permitted.
+            std::shared_ptr<TemplateEdge> templateEdge;
             
             /// The concrete destination objects.
             std::vector<EdgeDestination> destinations;

src/storm/storage/jani/Model.cpp

@@ -127,7 +127,9 @@ namespace storm {
         
         ConditionalMetaEdge createSynchronizedMetaEdge(Automaton& automaton, std::vector<std::reference_wrapper<Edge const>> const& edgesToSynchronize) {
             ConditionalMetaEdge result;
-            result.templateEdge = automaton.createTemplateEdge(createSynchronizedGuard(edgesToSynchronize));
+
+            result.templateEdge = std::make_shared<TemplateEdge>(createSynchronizedGuard(edgesToSynchronize));
+            automaton.registerTemplateEdge(result.templateEdge);
             
             for (auto const& edge : edgesToSynchronize) {
                 result.condition.push_back(edge.get().getSourceLocationIndex());
@@ -482,7 +484,8 @@ namespace storm {
                         conditionalMetaEdges.emplace_back();
                         ConditionalMetaEdge& conditionalMetaEdge = conditionalMetaEdges.back();
                         
-                        conditionalMetaEdge.templateEdge = newAutomaton.createTemplateEdge(edge.getGuard());
+                        conditionalMetaEdge.templateEdge = std::make_shared<TemplateEdge>(edge.getGuard());
+                        newAutomaton.registerTemplateEdge(conditionalMetaEdge.templateEdge);
                         conditionalMetaEdge.actionIndex = edge.getActionIndex();
                         conditionalMetaEdge.components.emplace_back(static_cast<uint64_t>(i));
                         conditionalMetaEdge.condition.emplace_back(edge.getSourceLocationIndex());

src/storm/storage/jani/OrderedAssignments.cpp

@@ -92,10 +92,12 @@ namespace storm {
         }
         
         int_fast64_t OrderedAssignments::getLowestLevel() const {
+            assert(!allAssignments.empty());
             return allAssignments.front()->getLevel();
         }
         
         int_fast64_t OrderedAssignments::getHighestLevel() const {
+            assert(!allAssignments.empty());
             return allAssignments.back()->getLevel();
         }
         
@@ -109,26 +111,29 @@ namespace storm {
         }
 
         OrderedAssignments OrderedAssignments::simplifyLevels(bool synchronous, VariableSet const& localVars) const {
-            if (!synchronous) {
-                bool changed = false;
-                std::vector<Assignment> newAssignments;
-                for (auto const& assignment : allAssignments) {
-                    newAssignments.push_back(*assignment);
-                    if (!isReadBeforeAssignment(assignment->getVariable(), upperBound(assignment->getLevel() - 1))) {
-                        if (!isWrittenBeforeAssignment(assignment->getVariable(), upperBound(assignment->getLevel()-1))) {
-                            newAssignments.back().setLevel(0);
-                            changed = true;
-                        }
-                    }
+            bool changed = false;
+            std::vector<Assignment> newAssignments;
+            for (auto const& assignment : allAssignments) {
+                newAssignments.push_back(*assignment);
+                if (synchronous && !localVars.hasVariable(assignment->getVariable())) {
+                    continue;
                 }
-                if (changed) {
-                    return OrderedAssignments(newAssignments).simplifyLevels(synchronous, localVars);
-                } else {
-                    return *this;
+                if (assignment->getLevel() == 0) {
+                    continue;
+                }
+                if (!isReadBeforeAssignment(assignment->getVariable(), upperBound(assignment->getLevel() - 1))) {
+                    if (!isWrittenBeforeAssignment(assignment->getVariable(), upperBound(assignment->getLevel()-1))) {
+                        newAssignments.back().setLevel(0);
+                        changed = true;
+                    }
                 }
+            }
+            if (changed) {
+                return OrderedAssignments(newAssignments).simplifyLevels(synchronous, localVars);
             } else {
                 return *this;
             }
+
         }
 
         detail::ConstAssignments OrderedAssignments::getAllAssignments() const {
@@ -183,10 +188,11 @@ namespace storm {
 
         bool OrderedAssignments::isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start) const {
             for (uint64_t i = start; i < assignmentNumber; i++) {
-                if (allAssignments.at(i)->getAssignedExpression().containsVariable(var.getExpressionVariable())) {
+                if (allAssignments.at(i)->getAssignedExpression().containsVariable({ var.getExpressionVariable() })) {
                     return true;
                 }
             }
+            return false;
         }
 
         bool OrderedAssignments::isWrittenBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start) const {
@@ -195,6 +201,7 @@ namespace storm {
                     return true;
                 }
             }
+            return false;
         }
 
         uint64_t OrderedAssignments::upperBound(int64_t index) const {
@@ -205,6 +212,7 @@ namespace storm {
                 }
                 ++result;
             }
+            return result;
         }
 
         bool OrderedAssignments::areLinear() const {
@@ -218,7 +226,11 @@ namespace storm {
         std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments) {
             stream << "[";
             for(auto const& e : assignments.allAssignments) {
-                stream << *e << std::endl;
+                stream << *e;
+                if (e->getLevel() != 0) {
+                    stream << " @" << e->getLevel();
+                }
+                stream << std::endl;
             }
             stream << "]";
             return stream;

src/storm/storage/jani/OrderedAssignments.h

@@ -150,7 +150,7 @@ namespace storm {
              * @param index The index we are interested in
              * @return
              */
-            uint64_t upperBound(int64_t index);
+            uint64_t upperBound(int64_t index) const;
 
             static std::vector<std::shared_ptr<Assignment>>::const_iterator lowerBound(Assignment const& assignment, std::vector<std::shared_ptr<Assignment>> const& assignments);
                         

src/storm/storage/jani/TemplateEdge.cpp

@@ -10,6 +10,11 @@ namespace storm {
         TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard) : guard(guard) {
             // Intentionally left empty.
         }
+
+        TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard, OrderedAssignments const& assignments, std::vector<TemplateEdgeDestination> const& destinations)
+                : guard(guard), assignments(assignments), destinations(destinations) {
+            // Intentionally left empty.
+        }
         
         void TemplateEdge::addDestination(TemplateEdgeDestination const& destination) {
             destinations.emplace_back(destination);
@@ -135,6 +140,16 @@ namespace storm {
             }
             return false;
         }
+
+
+        bool TemplateEdge::hasEdgeDestinationAssignments() const {
+            for (auto const& destination : destinations) {
+                if (destination.hasAssignments()) {
+                    return true;
+                }
+            }
+            return false;
+        }
         
         bool TemplateEdge::isLinear() const {
             storm::expressions::LinearityCheckVisitor linearityChecker;
@@ -145,6 +160,21 @@ namespace storm {
             }
             return result;
         }
-        
+
+        TemplateEdge TemplateEdge::simplifyIndexedAssignments(bool syncronized, VariableSet const& localVars) const {
+            // We currently only support cases where we have EITHER edge assignments or destination assignments.
+            if (assignments.empty()) {
+                // Only edge destination assignments:
+                TemplateEdge simplifiedTemplateEdge(guard);
+                for(auto const& dest : destinations) {
+                    simplifiedTemplateEdge.addDestination(dest.simplifyIndexedAssignments(syncronized, localVars));
+                }
+                return simplifiedTemplateEdge;
+            } else if(!hasEdgeDestinationAssignments()) {
+                return TemplateEdge(guard, assignments.simplifyLevels(syncronized, localVars), destinations);
+            } else {
+                return TemplateEdge(*this);
+            }
+        }
     }
 }

src/storm/storage/jani/TemplateEdge.h

@@ -16,7 +16,9 @@ namespace storm {
         class TemplateEdge {
         public:
             TemplateEdge() = default;
+            TemplateEdge(TemplateEdge const&) = default;
             TemplateEdge(storm::expressions::Expression const& guard);
+            TemplateEdge(storm::expressions::Expression const& guard, OrderedAssignments const& assignments, std::vector<TemplateEdgeDestination> const& destinations);
 
             storm::expressions::Expression const& getGuard() const;
 
@@ -88,6 +90,13 @@ namespace storm {
              * Checks the template edge for linearity.
              */
             bool isLinear() const;
+
+            bool hasEdgeDestinationAssignments() const;
+
+            /*!
+             * Simplify Indexed Assignments
+             */
+            TemplateEdge simplifyIndexedAssignments(bool syncronized, VariableSet const& localVars) const;
             
         private:
             // The guard of the template edge.

src/storm/storage/jani/TemplateEdgeDestination.cpp

@@ -50,5 +50,13 @@ namespace storm {
         bool TemplateEdgeDestination::isLinear() const {
             return assignments.areLinear();
         }
+
+        bool TemplateEdgeDestination::hasAssignments() const {
+            return !(assignments.empty());
+        }
+
+        TemplateEdgeDestination TemplateEdgeDestination::simplifyIndexedAssignments(bool syncronized, VariableSet const& localVars) const {
+            return TemplateEdgeDestination(assignments.simplifyLevels(syncronized, localVars));
+        }
     }
 }

src/storm/storage/jani/TemplateEdgeDestination.h

@@ -38,11 +38,21 @@ namespace storm {
              * Retrieves whether the edge uses an assignment level other than zero.
              */
             bool usesAssignmentLevels() const;
-            
+
+            /*!
+             * Checks whether the templ. edge destination contains one or more assignments
+             * @return True iff assignments exist
+             */
+            bool hasAssignments() const;
             /*!
              * Checks the template edge destination for linearity.
              */
             bool isLinear() const;
+
+            /*!
+             * Simplify Indexed Assignments
+             */
+            TemplateEdgeDestination simplifyIndexedAssignments(bool syncronized, VariableSet const& localVars) const;
             
         private:
             // The (ordered) assignments to make when choosing this destination.

src/storm/storage/prism/ToJaniConverter.cpp

@@ -202,7 +202,8 @@ namespace storm {
                 }
                 
                 for (auto const& command : module.getCommands()) {
-                    std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(command.getGuardExpression());
+                    std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(command.getGuardExpression());
+                    automaton.registerTemplateEdge(templateEdge);
                     actionIndicesOfModule.insert(janiModel.getActionIndex(command.getActionName()));
                     
                     boost::optional<storm::expressions::Expression> rateExpression;