From 9201c6420a8462fb3345353a82058ba776100abb Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 19 Aug 2015 10:17:11 +0200
Subject: [PATCH] Removes identity assignments
Former-commit-id: bdf15fd4c1bf67bd256a346e3ef14bfba238b5b9
---
src/storage/prism/Assignment.cpp | 15 +++++++++++++++
src/storage/prism/Assignment.h | 7 +++++++
src/storage/prism/Command.cpp | 16 ++++++++++++++++
src/storage/prism/Command.h | 8 ++++++++
src/storage/prism/Program.cpp | 12 ++++++++++--
src/storage/prism/Update.cpp | 17 ++++++++++++++++-
src/storage/prism/Update.h | 6 ++++++
7 files changed, 78 insertions(+), 3 deletions(-)
diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp
index 3628c76ef..a6c8b4456 100644
--- a/src/storage/prism/Assignment.cpp
+++ b/src/storage/prism/Assignment.cpp
@@ -1,4 +1,5 @@
#include "Assignment.h"
+#include <cassert>
namespace storm {
namespace prism {
@@ -22,6 +23,20 @@ namespace storm {
return Assignment(this->getVariable(), this->getExpression().substitute(substitution).simplify(), this->getFilename(), this->getLineNumber());
}
+ bool Assignment::isIdentity() const {
+ if(this->expression.isVariable()) {
+ assert(this->expression.getVariables().size() == 1);
+ //if( variable == *(this->expression.getVariables().begin())) {
+ // std::cout << variable.getName() << " == " << (this->expression.getVariables().begin())->getName() << std::endl;
+ //}
+ //else {
+ // std::cout << "********" << variable.getName() << " != " << (this->expression.getVariables().begin())->getName() << std::endl;
+ //}
+ return variable == *(this->expression.getVariables().begin());
+ }
+ return false;
+ }
+
std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
stream << "(" << assignment.getVariableName() << "' = " << assignment.getExpression() << ")";
return stream;
diff --git a/src/storage/prism/Assignment.h b/src/storage/prism/Assignment.h
index cb6006ba7..1c45a2b78 100644
--- a/src/storage/prism/Assignment.h
+++ b/src/storage/prism/Assignment.h
@@ -60,6 +60,13 @@ namespace storm {
*/
Assignment substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+ /*!
+ * Checks whether the assignment is an identity (lhs equals rhs)
+ *
+ * @return true iff the assignment is of the form a' = a.
+ */
+ bool isIdentity() const;
+
friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment);
private:
diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp
index e2b1d3698..5cad634e7 100644
--- a/src/storage/prism/Command.cpp
+++ b/src/storage/prism/Command.cpp
@@ -1,4 +1,5 @@
#include "Command.h"
+#include <cassert>
namespace storm {
namespace prism {
@@ -31,6 +32,7 @@ namespace storm {
}
storm::prism::Update const& Command::getUpdate(uint_fast64_t index) const {
+ assert(index < getNumberOfUpdates());
return this->updates[index];
}
@@ -71,6 +73,20 @@ namespace storm {
return true;
}
+ Command Command::removeIdentityAssignmentsFromUpdates() const {
+ std::vector<Update> newUpdates;
+ newUpdates.reserve(this->getNumberOfUpdates());
+ for (auto const& update : this->getUpdates()) {
+ newUpdates.emplace_back(update.removeIdentityAssignments());
+ }
+ return copyWithNewUpdates(std::move(newUpdates));
+
+ }
+
+ Command Command::copyWithNewUpdates(std::vector<Update> && newUpdates) const {
+ return Command(this->globalIndex, this->markovian, this->getActionIndex(), this->getActionName(), guardExpression, newUpdates, this->getFilename(), this->getLineNumber());
+ }
+
std::ostream& operator<<(std::ostream& stream, Command const& command) {
if (command.isMarkovian()) {
stream << "<" << command.getActionName() << "> ";
diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h
index dd8b2f9b6..658cce67d 100644
--- a/src/storage/prism/Command.h
+++ b/src/storage/prism/Command.h
@@ -128,6 +128,12 @@ namespace storm {
friend std::ostream& operator<<(std::ostream& stream, Command const& command);
+ /**
+ * Removes identity assignments from the updates
+ * @return The resulting command
+ */
+ Command removeIdentityAssignmentsFromUpdates() const;
+
private:
// The index of the action associated with this command.
uint_fast64_t actionIndex;
@@ -150,6 +156,8 @@ namespace storm {
// A flag indicating whether the command is labeled.
bool labeled;
+
+ Command copyWithNewUpdates(std::vector<Update>&& newUpdates) const;
};
} // namespace prism
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index d58d1a940..611943b16 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -781,6 +781,14 @@ namespace storm {
std::vector<Module> newModules;
std::vector<Constant> newConstants = this->getConstants();
for (auto const& module : this->getModules()) {
+ // Remove identity assignments from the updates
+ std::vector<Command> newCommands;
+ for (auto const& command : module.getCommands()) {
+ newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates());
+ }
+
+ // Substitute Variables by Global constants if possible.
+
std::map<storm::expressions::Variable, storm::expressions::Expression> booleanVars;
std::map<storm::expressions::Variable, storm::expressions::Expression> integerVars;
for (auto const& variable : module.getBooleanVariables()) {
@@ -790,7 +798,7 @@ namespace storm {
integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
}
- for (auto const& command : module.getCommands()) {
+ for (auto const& command : newCommands) {
// Check all updates.
for (auto const& update : command.getUpdates()) {
// Check all assignments.
@@ -821,7 +829,7 @@ namespace storm {
}
}
- newModules.emplace_back(module.getName(), newBVars, newIVars, module.getCommands());
+ newModules.emplace_back(module.getName(), newBVars, newIVars, newCommands);
for(auto const& entry : booleanVars) {
newConstants.emplace_back(entry.first, entry.second);
diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp
index c00a9fbd2..9adf3b5b8 100644
--- a/src/storage/prism/Update.cpp
+++ b/src/storage/prism/Update.cpp
@@ -52,12 +52,27 @@ namespace storm {
return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute(substitution), newAssignments, this->getFilename(), this->getLineNumber());
}
+ Update Update::removeIdentityAssignments() const {
+ std::vector<Assignment> newAssignments;
+ newAssignments.reserve(getNumberOfAssignments());
+ for(auto const& ass : this->assignments) {
+ if(!ass.isIdentity()) {
+ newAssignments.push_back(ass);
+ }
+ }
+ return Update(this->globalIndex, this->likelihoodExpression, newAssignments, getFilename(), getLineNumber());
+ }
+
std::ostream& operator<<(std::ostream& stream, Update const& update) {
stream << update.getLikelihoodExpression() << " : ";
+ if(update.getNumberOfAssignments() == 0) {
+ stream << "True";
+ }
+
uint_fast64_t i = 0;
for (auto const& assignment : update.getAssignments()) {
stream << assignment;
- if (i < update.getAssignments().size() - 1) {
+ if (i < update.getNumberOfAssignments() - 1) {
stream << " & ";
}
++i;
diff --git a/src/storage/prism/Update.h b/src/storage/prism/Update.h
index 1ea5470f8..7b9ebdbc1 100644
--- a/src/storage/prism/Update.h
+++ b/src/storage/prism/Update.h
@@ -73,6 +73,12 @@ namespace storm {
* @return The resulting update.
*/
Update substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+ /*!
+ * Removes all assignments which do not change the variable.
+ *
+ * @return The resulting update.
+ */
+ Update removeIdentityAssignments() const;
friend std::ostream& operator<<(std::ostream& stream, Update const& assignment);