From d638972bc80d5baf728df5562568bc51b8bed89c Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 3 Jul 2018 15:22:53 +0200 Subject: [PATCH] enabled pushing location assignments to edges --- src/storm/storage/jani/Automaton.cpp | 29 ++++++++++++++++++- src/storm/storage/jani/Automaton.h | 6 ++++ src/storm/storage/jani/Model.cpp | 5 ++++ src/storm/storage/jani/OrderedAssignments.cpp | 28 ++++++++++-------- src/storm/storage/jani/OrderedAssignments.h | 4 ++- src/storm/storage/jani/TemplateEdge.cpp | 6 ++-- src/storm/storage/jani/TemplateEdge.h | 4 ++- .../storage/jani/TemplateEdgeDestination.cpp | 4 +-- .../storage/jani/TemplateEdgeDestination.h | 2 +- 9 files changed, 67 insertions(+), 21 deletions(-) diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index f4c65c759..e962562d2 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -8,6 +8,7 @@ #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidTypeException.h" +#include "storm/exceptions/NotSupportedException.h" namespace storm { namespace jani { @@ -419,6 +420,33 @@ namespace storm { edges.pushAssignmentsToDestinations(); } + void Automaton::pushTransientRealLocationAssignmentsToEdges() { + std::set> encounteredTemplateEdges; + + for (uint64_t locationIndex = 0; locationIndex < locations.size(); ++locationIndex) { + auto& location = locations[locationIndex]; + auto edges = this->getEdgesFromLocation(locationIndex); + + for (auto& edge : edges) { + STORM_LOG_THROW(encounteredTemplateEdges.find(edge.getTemplateEdge()) == encounteredTemplateEdges.end(), storm::exceptions::NotSupportedException, "Pushing location assignments to edges is only supported for automata with unique template edges."); + + auto& templateEdge = edge.getTemplateEdge(); + encounteredTemplateEdges.insert(templateEdge); + + storm::jani::Location newLocation(location.getName()); + for (auto const& assignment : location.getAssignments().getTransientAssignments()) { + if (assignment.getVariable().isTransient() && assignment.getVariable().isRealVariable()) { + templateEdge->addTransientAssignment(assignment, true); + } else { + newLocation.addTransientAssignment(assignment); + } + } + + location = std::move(newLocation); + } + } + } + bool Automaton::hasTransientEdgeDestinationAssignments() const { for (auto const& edge : this->getEdges()) { if (edge.hasTransientEdgeDestinationAssignments()) { @@ -440,7 +468,6 @@ namespace storm { return true; } - bool Automaton::usesAssignmentLevels() const { return edges.usesAssignmentLevels(); } diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index c549ecca8..238f26896 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -294,6 +294,12 @@ namespace storm { */ void pushEdgeAssignmentsToDestinations(); + /*! + * Pushes the assignments to real-valued transient variables to the edges. + * Note: This is currently only supported if the template edges are uniquely coupled with one source location. + */ + void pushTransientRealLocationAssignmentsToEdges(); + /*! * Retrieves whether there is any transient edge destination assignment in the automaton. */ diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 47533126c..0cbbaae14 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -1107,6 +1107,11 @@ namespace storm { void Model::makeStandardJaniCompliant() { for (auto& automaton : automata) { + // For discrete-time models, we push the assignments to real-valued transient variables (rewards) to the + // edges. + if (this->isDiscreteTimeModel()) { + automaton.pushTransientRealLocationAssignmentsToEdges(); + } automaton.pushEdgeAssignmentsToDestinations(); } } diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index 99eb415a8..564baed9f 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -17,7 +17,7 @@ namespace storm { add(assignment); } - bool OrderedAssignments::add(Assignment const& assignment) { + bool OrderedAssignments::add(Assignment const& assignment, bool addToExisting) { // If the element is contained in this set of assignment, nothing needs to be added. if (this->contains(assignment)) { return false; @@ -27,18 +27,22 @@ namespace storm { auto it = lowerBound(assignment, allAssignments); if (it != allAssignments.end()) { - STORM_LOG_THROW(assignment.getExpressionVariable() != (*it)->getExpressionVariable(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression() << "') to variable '" << (*it)->getVariable().getName() << "' already exists."); - } - - // Finally, insert the new element in the correct vectors. - auto elementToInsert = std::make_shared(assignment); - allAssignments.emplace(it, elementToInsert); - if (assignment.isTransient()) { - auto transientIt = lowerBound(assignment, transientAssignments); - transientAssignments.emplace(transientIt, elementToInsert); + if ((!addToExisting || !assignment.getExpressionVariable().hasNumericalType())) { + STORM_LOG_THROW(assignment.getExpressionVariable() != (*it)->getExpressionVariable(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression() << "') to variable '" << (*it)->getVariable().getName() << "' already exists."); + } else if (addToExisting && assignment.getExpressionVariable().hasNumericalType()) { + (*it)->setAssignedExpression((*it)->getAssignedExpression() + assignment.getAssignedExpression()); + } } else { - auto nonTransientIt = lowerBound(assignment, nonTransientAssignments); - nonTransientAssignments.emplace(nonTransientIt, elementToInsert); + // Finally, insert the new element in the correct vectors. + auto elementToInsert = std::make_shared(assignment); + allAssignments.emplace(it, elementToInsert); + if (assignment.isTransient()) { + auto transientIt = lowerBound(assignment, transientAssignments); + transientAssignments.emplace(transientIt, elementToInsert); + } else { + auto nonTransientIt = lowerBound(assignment, nonTransientAssignments); + nonTransientAssignments.emplace(nonTransientIt, elementToInsert); + } } return true; diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index 8e307e6e0..428912bf1 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/src/storm/storage/jani/OrderedAssignments.h @@ -26,9 +26,11 @@ namespace storm { /*! * Adds the given assignment to the set of assignments. * + * @addToExisting If true the value of the assigned expression is added to a (potentially) previous assignment + * to the variable. If false and there is already an assignment, an exception is thrown. * @return True iff the assignment was added. */ - bool add(Assignment const& assignment); + bool add(Assignment const& assignment, bool addToExisting = false); /*! * Removes the given assignment from this set of assignments. diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index 987e4f6de..89d56a0d3 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/src/storm/storage/jani/TemplateEdge.cpp @@ -20,8 +20,8 @@ namespace storm { destinations.emplace_back(destination); } - bool TemplateEdge::addTransientAssignment(Assignment const& assignment) { - return assignments.add(assignment); + bool TemplateEdge::addTransientAssignment(Assignment const& assignment, bool addToExisting) { + return assignments.add(assignment, addToExisting); } void TemplateEdge::finalize(Model const& containingModel) { @@ -106,7 +106,7 @@ namespace storm { STORM_LOG_ASSERT(!destinations.empty(), "Need non-empty destinations for this transformation."); for (auto const& assignment : this->getAssignments()) { for (auto& destination : destinations) { - destination.addAssignment(assignment); + destination.addAssignment(assignment, true); } } this->assignments.clear(); diff --git a/src/storm/storage/jani/TemplateEdge.h b/src/storm/storage/jani/TemplateEdge.h index cccc1bb7f..dac58144b 100644 --- a/src/storm/storage/jani/TemplateEdge.h +++ b/src/storm/storage/jani/TemplateEdge.h @@ -40,9 +40,11 @@ namespace storm { * Adds a transient assignment to this edge. * * @param assignment The transient assignment to add. + * @param addToExisting Determines if adding the assigned expression to an already existing assignment is + * allowed (if the assigned variable is quantitative). * @return True if the assignment was added. */ - bool addTransientAssignment(Assignment const& assignment); + bool addTransientAssignment(Assignment const& assignment, bool addToExisting = false); /*! * Retrieves a set of (global) variables that are written by at least one of the edge's destinations. diff --git a/src/storm/storage/jani/TemplateEdgeDestination.cpp b/src/storm/storage/jani/TemplateEdgeDestination.cpp index 2d99a1ad1..b30bbda92 100644 --- a/src/storm/storage/jani/TemplateEdgeDestination.cpp +++ b/src/storm/storage/jani/TemplateEdgeDestination.cpp @@ -31,8 +31,8 @@ namespace storm { return assignments.remove(assignment); } - void TemplateEdgeDestination::addAssignment(Assignment const& assignment) { - assignments.add(assignment); + void TemplateEdgeDestination::addAssignment(Assignment const& assignment, bool addToExisting) { + assignments.add(assignment, addToExisting); } bool TemplateEdgeDestination::hasAssignment(Assignment const& assignment) const { diff --git a/src/storm/storage/jani/TemplateEdgeDestination.h b/src/storm/storage/jani/TemplateEdgeDestination.h index bb94125f9..e6ad889b8 100644 --- a/src/storm/storage/jani/TemplateEdgeDestination.h +++ b/src/storm/storage/jani/TemplateEdgeDestination.h @@ -27,7 +27,7 @@ namespace storm { // Convenience methods to access the assignments. bool hasAssignment(Assignment const& assignment) const; bool removeAssignment(Assignment const& assignment); - void addAssignment(Assignment const& assignment); + void addAssignment(Assignment const& assignment, bool addToExisting = false); /*! * Retrieves whether this destination has transient assignments.