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 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 && 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 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: