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 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 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 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 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 && 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&& 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 newModules; std::vector newConstants = this->getConstants(); for (auto const& module : this->getModules()) { + // Remove identity assignments from the updates + std::vector newCommands; + for (auto const& command : module.getCommands()) { + newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates()); + } + + // Substitute Variables by Global constants if possible. + std::map booleanVars; std::map 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 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 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);