From 8bc646ccb825c4f9d3ec4f21f4d8e1cc6bf4f2b0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 3 Feb 2015 05:31:52 +0100
Subject: [PATCH] Simplification of program when substituting constants.

Former-commit-id: d5ecb355f8c1a1ba45788873cbd3ee67c9c0fd4b
---
 src/storage/prism/Command.cpp | 2 +-
 src/storage/prism/Module.cpp  | 5 ++++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp
index fec849628..a476e2fd9 100644
--- a/src/storage/prism/Command.cpp
+++ b/src/storage/prism/Command.cpp
@@ -41,7 +41,7 @@ namespace storm {
                 newUpdates.emplace_back(update.substitute(substitution));
             }
             
-            return Command(this->getGlobalIndex(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber());
+            return Command(this->getGlobalIndex(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution).simplify(), newUpdates, this->getFilename(), this->getLineNumber());
         }
         
         bool Command::isLabeled() const {
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index bc40cbd78..e6adf07b1 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -161,7 +161,10 @@ namespace storm {
             std::vector<Command> newCommands;
             newCommands.reserve(this->getNumberOfCommands());
             for (auto const& command : this->getCommands()) {
-                newCommands.emplace_back(command.substitute(substitution));
+                Command newCommand = command.substitute(substitution);
+                if (!newCommand.getGuardExpression().isFalse()) {
+                    newCommands.emplace_back(newCommand);
+                }
             }
             
             return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber());