From 8e32d3fa8f4931e9eb08607f6dfd64e9553ba5c4 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 10 Feb 2017 22:44:12 +0100 Subject: [PATCH] Simplifying index levels --- src/storm-gspn/builder/JaniGSPNBuilder.cpp | 8 +++- .../builder/JaniProgramGraphBuilder.cpp | 14 ++++-- src/storm/parser/JaniParser.cpp | 3 +- src/storm/storage/jani/Automaton.cpp | 23 +++++++--- src/storm/storage/jani/Automaton.h | 10 ++-- src/storm/storage/jani/Edge.cpp | 20 +++++++- src/storm/storage/jani/Edge.h | 16 +++++-- src/storm/storage/jani/Model.cpp | 7 ++- src/storm/storage/jani/OrderedAssignments.cpp | 46 ++++++++++++------- src/storm/storage/jani/OrderedAssignments.h | 2 +- src/storm/storage/jani/TemplateEdge.cpp | 32 ++++++++++++- src/storm/storage/jani/TemplateEdge.h | 9 ++++ .../storage/jani/TemplateEdgeDestination.cpp | 8 ++++ .../storage/jani/TemplateEdgeDestination.h | 12 ++++- src/storm/storage/prism/ToJaniConverter.cpp | 3 +- 15 files changed, 167 insertions(+), 46 deletions(-) diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index d5e8846ea..cd81bb266 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/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 templateEdge = automaton.createTemplateEdge((priorityGuard && guard).simplify()); + std::shared_ptr templateEdge = std::make_shared((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 templateEdge = automaton.createTemplateEdge(guard); + std::shared_ptr templateEdge = std::make_shared(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); diff --git a/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp b/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp index 4741fc374..0db2787bb 100644 --- a/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp +++ b/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 templateEdge = automaton.createTemplateEdge(newCondition); + std::shared_ptr templateEdge = std::make_shared(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 templateEdge = automaton.createTemplateEdge(expManager->boolean(true)); + std::shared_ptr templateEdge = std::make_shared(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 templateEdge = automaton.createTemplateEdge(simplifyExpression(edge->getCondition() && checks.second)); + std::shared_ptr templateEdge = std::make_shared(simplifyExpression(edge->getCondition() && checks.second)); + automaton.registerTemplateEdge(templateEdge); + std::vector> 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 templateEdge = automaton.createTemplateEdge(expManager->boolean(true)); + std::shared_ptr templateEdge = std::make_shared(expManager->boolean(true)); + automaton.registerTemplateEdge(templateEdge); + std::vector destinationProbabilities; std::vector destinationLocations; diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index c8f0c15e8..8fac23926 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/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 templateEdge = automaton.createTemplateEdge(guardExpr); + std::shared_ptr templateEdge = std::make_shared(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> destinationLocationsAndProbabilities; diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 8fc6a80dd..7817fea56 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -297,10 +297,7 @@ namespace storm { return ConstEdges(it1, it2); } - std::shared_ptr Automaton::createTemplateEdge(storm::expressions::Expression const& guard) { - templateEdges.emplace_back(std::make_shared(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 const& te) { + templateEdges.insert(te); + } + void Automaton::changeAssignmentVariables(std::map> 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()) { diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index f67283030..d9bd2a517 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/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 createTemplateEdge(storm::expressions::Expression const& guard); - + void registerTemplateEdge(std::shared_ptr 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 edges; /// The templates for the contained edges. - std::vector> templateEdges; + std::unordered_set> 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. diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp index 27fd5e57a..7efa96926 100644 --- a/src/storm/storage/jani/Edge.cpp +++ b/src/storm/storage/jani/Edge.cpp @@ -10,7 +10,7 @@ namespace storm { namespace jani { - Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, std::shared_ptr const& templateEdge, std::vector> const& destinationTargetLocationsAndProbabilities) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), templateEdge(templateEdge) { + Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, std::shared_ptr const& templateEdge, std::vector> 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 const& rate, std::shared_ptr const& templateEdge, std::vector const& destinationLocations, std::vector const& destinationProbabilities) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), templateEdge(templateEdge) { + Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, std::shared_ptr const& templateEdge, std::vector const& destinationLocations, std::vector 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->simplifyIndexedAssignments(!hasSilentAction(), localVars)); + std::vector 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 const& Edge::getTemplateEdge() { + return templateEdge; + } } } diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h index 62568afcb..af98706ae 100644 --- a/src/storm/storage/jani/Edge.h +++ b/src/storm/storage/jani/Edge.h @@ -17,8 +17,8 @@ namespace storm { public: Edge() = default; - Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, std::shared_ptr const& templateEdge, std::vector> const& destinationTargetLocationsAndProbabilities); - Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, std::shared_ptr const& templateEdge, std::vector const& destinationLocations, std::vector const& destinationProbabilities); + Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, std::shared_ptr const& templateEdge, std::vector> const& destinationTargetLocationsAndProbabilities); + Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, std::shared_ptr const& templateEdge, std::vector const& destinationLocations, std::vector 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 const& getTemplateEdge(); private: /// The index of the source location. @@ -116,8 +124,8 @@ namespace storm { /// models, this must be set to none. boost::optional rate; - /// The template of this edge: guards and destinations. - std::shared_ptr 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; /// The concrete destination objects. std::vector destinations; diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 083b8f7fb..982d4a51f 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -127,7 +127,9 @@ namespace storm { ConditionalMetaEdge createSynchronizedMetaEdge(Automaton& automaton, std::vector> const& edgesToSynchronize) { ConditionalMetaEdge result; - result.templateEdge = automaton.createTemplateEdge(createSynchronizedGuard(edgesToSynchronize)); + + result.templateEdge = std::make_shared(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(edge.getGuard()); + newAutomaton.registerTemplateEdge(conditionalMetaEdge.templateEdge); conditionalMetaEdge.actionIndex = edge.getActionIndex(); conditionalMetaEdge.components.emplace_back(static_cast(i)); conditionalMetaEdge.condition.emplace_back(edge.getSourceLocationIndex()); diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index a77dcb035..a0261a4c4 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/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 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 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; diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index 97d7e732d..b5471d50a 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/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>::const_iterator lowerBound(Assignment const& assignment, std::vector> const& assignments); diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index 07b305ffc..a788685f8 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/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 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); + } + } } } diff --git a/src/storm/storage/jani/TemplateEdge.h b/src/storm/storage/jani/TemplateEdge.h index a68fba7c3..cccc1bb7f 100644 --- a/src/storm/storage/jani/TemplateEdge.h +++ b/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 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. diff --git a/src/storm/storage/jani/TemplateEdgeDestination.cpp b/src/storm/storage/jani/TemplateEdgeDestination.cpp index e374f7322..2d99a1ad1 100644 --- a/src/storm/storage/jani/TemplateEdgeDestination.cpp +++ b/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)); + } } } diff --git a/src/storm/storage/jani/TemplateEdgeDestination.h b/src/storm/storage/jani/TemplateEdgeDestination.h index 5285c0b8d..bb94125f9 100644 --- a/src/storm/storage/jani/TemplateEdgeDestination.h +++ b/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. diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 21a806374..23e3215f7 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -202,7 +202,8 @@ namespace storm { } for (auto const& command : module.getCommands()) { - std::shared_ptr templateEdge = automaton.createTemplateEdge(command.getGuardExpression()); + std::shared_ptr templateEdge = std::make_shared(command.getGuardExpression()); + automaton.registerTemplateEdge(templateEdge); actionIndicesOfModule.insert(janiModel.getActionIndex(command.getActionName())); boost::optional rateExpression;