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<std::shared_ptr<storm::jani::TemplateEdge>> 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>(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>(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.