From d3ece2a2e5e1a36069006c2e3d780134965c48c0 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 10 Mar 2020 12:06:03 +0100
Subject: [PATCH] Better simplification of prism commands.
---
src/storm/storage/prism/Command.cpp | 5 +++--
src/storm/storage/prism/Update.cpp | 12 ++++++++++++
src/storm/storage/prism/Update.h | 5 +++++
3 files changed, 20 insertions(+), 2 deletions(-)
diff --git a/src/storm/storage/prism/Command.cpp b/src/storm/storage/prism/Command.cpp
index 7ee1434d6..4b357c73a 100644
--- a/src/storm/storage/prism/Command.cpp
+++ b/src/storm/storage/prism/Command.cpp
@@ -85,9 +85,10 @@ namespace storm {
std::vector<Update> newUpdates;
newUpdates.reserve(this->getNumberOfUpdates());
for (auto const& update : this->getUpdates()) {
- newUpdates.emplace_back(update.removeIdentityAssignments());
+ newUpdates.emplace_back(update.simplify());
}
- return copyWithNewUpdates(std::move(newUpdates));
+ auto simpleGuard = guardExpression.simplify().reduceNesting();
+ return Command(this->globalIndex, this->markovian, this->getActionIndex(), this->getActionName(), simpleGuard, newUpdates, this->getFilename(), this->getLineNumber());
}
Command Command::copyWithNewUpdates(std::vector<Update> && newUpdates) const {
diff --git a/src/storm/storage/prism/Update.cpp b/src/storm/storage/prism/Update.cpp
index 832adae6f..d1c93e335 100644
--- a/src/storm/storage/prism/Update.cpp
+++ b/src/storm/storage/prism/Update.cpp
@@ -87,6 +87,18 @@ namespace storm {
return Update(this->globalIndex, this->likelihoodExpression, newAssignments, getFilename(), getLineNumber());
}
+ Update Update::simplify() const {
+ std::vector<Assignment> newAssignments;
+ newAssignments.reserve(getNumberOfAssignments());
+ for (auto const& ass : this->assignments) {
+ Assignment newAssignment(ass.getVariable(), ass.getExpression().simplify().reduceNesting(), ass.getFilename(), ass.getLineNumber());
+ if (!newAssignment.isIdentity()) {
+ newAssignments.push_back(std::move(newAssignment));
+ }
+ }
+ return Update(this->globalIndex, this->likelihoodExpression.simplify().reduceNesting(), newAssignments, getFilename(), getLineNumber());
+ }
+
std::ostream& operator<<(std::ostream& stream, Update const& update) {
stream << update.getLikelihoodExpression() << " : ";
if (update.getAssignments().empty()) {
diff --git a/src/storm/storage/prism/Update.h b/src/storm/storage/prism/Update.h
index 8f752a207..43e6132d7 100644
--- a/src/storm/storage/prism/Update.h
+++ b/src/storm/storage/prism/Update.h
@@ -93,6 +93,11 @@ namespace storm {
*/
Update removeIdentityAssignments() const;
+ /*!
+ * Simplifies the update in various ways (also removes identity assignments)
+ */
+ Update simplify() const;
+
friend std::ostream& operator<<(std::ostream& stream, Update const& assignment);
private: