Removes identity assignments

Former-commit-id: bdf15fd4c1

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;

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:

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() << "> ";

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

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);

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;

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);