From 812b101c40c9077fc3a56edff439a32342e7ad5d Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Mon, 10 Aug 2015 16:15:09 +0200
Subject: [PATCH 1/2] better program checks, some extensions in model and
 matrix

Former-commit-id: 8efaaf2ca9902278654603ede3eddd7ffa8fbf90
---
 src/models/sparse/Mdp.cpp                     |  12 ++
 src/models/sparse/Mdp.h                       |   8 +
 src/models/sparse/Model.cpp                   |   5 +
 src/models/sparse/Model.h                     |  12 +-
 src/storage/SparseMatrix.cpp                  |   8 +
 src/storage/SparseMatrix.h                    |   8 +
 .../expressions/IfThenElseExpression.cpp      |   2 +-
 src/storage/prism/Program.cpp                 | 155 +++++++++++++-----
 src/storage/prism/Program.h                   |  24 ++-
 src/utility/cli.h                             | 113 ++++++-------
 10 files changed, 245 insertions(+), 102 deletions(-)

diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp
index 1c8bd1b50..469dfe54e 100644
--- a/src/models/sparse/Mdp.cpp
+++ b/src/models/sparse/Mdp.cpp
@@ -72,9 +72,21 @@ namespace storm {
                                              this->hasStateRewards() ? boost::optional<std::vector<ValueType>>(this->getStateRewardVector()) : boost::optional<std::vector<ValueType>>(),
                                              this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<ValueType>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<ValueType>>(),
                                              boost::optional<std::vector<LabelSet>>(newChoiceLabeling));
+                
                 return restrictedMdp;
             }
             
+            template <typename ValueType>
+            Mdp<ValueType> Mdp<ValueType>::restrictActions(storm::storage::BitVector const& enabledActions) const {
+                storm::storage::SparseMatrix<ValueType> restrictedTransitions = this->getTransitionMatrix().restrictRows(enabledActions);
+                if(this->hasTransitionRewards()) {
+                    return Mdp<ValueType>(restrictedTransitions, this->getStateLabeling(), this->getOptionalStateRewardVector(), boost::optional<storm::storage::SparseMatrix<ValueType>>(this->getTransitionRewardMatrix().restrictRows(enabledActions)), this->getOptionalChoiceLabeling());
+                } else {
+                    return Mdp<ValueType>( restrictedTransitions, this->getStateLabeling(), this->getOptionalStateRewardVector(), boost::optional<storm::storage::SparseMatrix<ValueType>>(), this->getOptionalChoiceLabeling());
+                }
+                
+            }
+            
             template <typename ValueType>
             bool Mdp<ValueType>::checkValidityOfProbabilityMatrix() const {
                 storm::utility::ConstantsComparator<ValueType> comparator;
diff --git a/src/models/sparse/Mdp.h b/src/models/sparse/Mdp.h
index 18879ee76..3b66d0e61 100644
--- a/src/models/sparse/Mdp.h
+++ b/src/models/sparse/Mdp.h
@@ -63,6 +63,14 @@ namespace storm {
                  */
                 Mdp<ValueType> restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const;
                 
+                /*!
+                 * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones given by the bitvector.
+                 * 
+                 * @param enabledActions A BitVector of lenght numberOfChoices(), which is one iff the action should be kept.
+                 * @return A subMDP.
+                 */
+                Mdp<ValueType> restrictActions(storm::storage::BitVector const& enabledActions) const;
+                
             private:
                 /*!
                  * Checks the probability matrix for validity.
diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp
index b2ca03c1d..506083cbc 100644
--- a/src/models/sparse/Model.cpp
+++ b/src/models/sparse/Model.cpp
@@ -113,6 +113,11 @@ namespace storm {
                 return choiceLabeling.get();
             }
             
+            template <typename ValueType>
+            boost::optional<std::vector<LabelSet>> const& Model<ValueType>::getOptionalChoiceLabeling() const {
+                return choiceLabeling;
+            }
+            
             template <typename ValueType>
             storm::models::sparse::StateLabeling const& Model<ValueType>::getStateLabeling() const {
                 return stateLabeling;
diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h
index 5457370e6..4d1901d1f 100644
--- a/src/models/sparse/Model.h
+++ b/src/models/sparse/Model.h
@@ -173,13 +173,20 @@ namespace storm {
                 boost::optional<std::vector<ValueType>> const& getOptionalStateRewardVector() const;
                 
                 /*!
-                 * Retrieves the labels for the choices of the model. Note that calling this method is only valud if the
-                 * model has a choice labling.
+                 * Retrieves the labels for the choices of the model. Note that calling this method is only valid if the
+                 * model has a choice labeling.
                  *
                  * @return The labels for the choices of the model.
                  */
                 std::vector<LabelSet> const& getChoiceLabeling() const;
                 
+                /*!
+                 * Retrieves an optional value that contains the choice labeling if there is one.
+                 * 
+                 * @return The labels for the choices, if they're saved.
+                 */
+                boost::optional<std::vector<LabelSet>> const&  getOptionalChoiceLabeling() const;
+                
                 /*!
                  * Returns the state labeling associated with this model.
                  *
@@ -194,6 +201,7 @@ namespace storm {
                  */
                 storm::models::sparse::StateLabeling& getStateLabeling();
                 
+                
                 /*!
                  * Retrieves whether this model has state rewards.
                  *
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index ce5419099..2cb9f995b 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -614,6 +614,14 @@ namespace storm {
             return matrixBuilder.build();
         }
         
+        template<typename ValueType>
+        SparseMatrix<ValueType> SparseMatrix<ValueType>::restrictRows(storm::storage::BitVector const& rowsToKeep) const {
+            // For now, we use the expensive call to submatrix.
+            SparseMatrix<ValueType> res(getSubmatrix(false, rowsToKeep, storm::storage::BitVector(getColumnCount(), true), false));
+            assert(getRowGroupCount() == res.getRowGroupCount());
+            return res;
+        }
+        
         template<typename ValueType>
         SparseMatrix<ValueType> SparseMatrix<ValueType>::selectRowsFromRowGroups(std::vector<index_type> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const {
             // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 35ff09658..7d7092377 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -610,6 +610,14 @@ namespace storm {
              */
             SparseMatrix getSubmatrix(bool useGroups, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalEntries = false) const;
             
+            /*!
+             * Restrict rows in grouped rows matrix. Ensures that the number of groups stays the same. 
+             * 
+             * @param rowsToKeep A bit vector indicating which rows to keep.
+             * 
+             */
+            SparseMatrix restrictRows(storm::storage::BitVector const& rowsToKeep) const;
+            
             /*!
              * Selects exactly one row from each row group of this matrix and returns the resulting matrix.
              *
diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp
index f3e65a94f..4692675bf 100644
--- a/src/storage/expressions/IfThenElseExpression.cpp
+++ b/src/storage/expressions/IfThenElseExpression.cpp
@@ -70,7 +70,7 @@ namespace storm {
 		}
         
         std::shared_ptr<BaseExpression const> IfThenElseExpression::simplify() const {
-            std::shared_ptr<BaseExpression const> conditionSimplified;
+            std::shared_ptr<BaseExpression const> conditionSimplified = this->condition->simplify();
             if (conditionSimplified->isTrue()) {
                 return this->thenExpression->simplify();
             } else if (conditionSimplified->isFalse()) {
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 0b61fd795..3792bea94 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -12,7 +12,16 @@
 
 namespace storm {
     namespace prism {
-        Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() {
+        Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool finalModel) 
+        : LocatedInformation(filename, lineNumber), manager(manager),
+            modelType(modelType), constants(constants), constantToIndexMap(),
+            globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(),
+            globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), 
+            formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), 
+            rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), 
+            labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), 
+            actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap()
+        {
             this->createMappings();
             
             // Create a new initial construct if the corresponding flag was set.
@@ -36,7 +45,8 @@ namespace storm {
                 this->initialConstruct = storm::prism::InitialConstruct(newInitialExpression, this->getInitialConstruct().getFilename(), this->getInitialConstruct().getLineNumber());
             }
 
-            if (checkValidity) {
+            if (finalModel) {
+
                 // If the model is supposed to be a CTMC, but contains probabilistic commands, we transform them to Markovian
                 // commands and issue a warning.
                 if (modelType == storm::prism::Program::ModelType::CTMC && storm::settings::generalSettings().isPrismCompatibilityEnabled()) {
@@ -51,9 +61,8 @@ namespace storm {
                     }
                     STORM_LOG_WARN_COND(!hasProbabilisticCommands, "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Consider rewriting the commands to use Markovian commands instead.");
                 }
-                
                 // Then check the validity.
-                this->checkValidity();
+                this->checkValidity(Program::ValidityCheckLevel::VALIDINPUT);
             }
         }
     
@@ -509,7 +518,8 @@ namespace storm {
             return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, false, newInitialConstruct, newLabels);
         }
         
-        void Program::checkValidity() const {
+        void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
+            
             // Start by checking the constant declarations.
             std::set<storm::expressions::Variable> all;
             std::set<storm::expressions::Variable> allGlobals;
@@ -602,40 +612,6 @@ namespace storm {
             std::set<storm::expressions::Variable> variablesAndConstants;
             std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
             
-            // We check for each global variable and each labeled command, whether there is at most one instance writing to that variable.
-            std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
-            std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommand;
-            for(auto const& module : this->getModules()) {
-                std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommandInThisModule;
-                std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommandInThisModule;
-                for (auto const& command : module.getCommands()) {
-                    if(!command.isLabeled()) continue;
-                    for (auto const& update : command.getUpdates()) {
-                         for (auto const& assignment : update.getAssignments()) {
-                             if(this->globalBooleanVariableExists(assignment.getVariable().getName())) {
-                                 globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
-                             }
-                             else if(this->globalIntegerVariableExists(assignment.getVariable().getName())) {
-                                 globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
-                             }
-                         }
-                    }
-                }
-                for(auto const& entry : globalIVarsWrittenToByCommandInThisModule) {
-                    if(globalIVarsWrittenToByCommand.find(entry) != globalIVarsWrittenToByCommand.end()) {
-                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": assignment of (possibly) synchronizing command with label '" << entry.second << "' writes to global variable '" << entry.first << "'.");
-                    }
-                }
-                for(auto const& entry : globalBVarsWrittenToByCommandInThisModule) {
-                    if(globalBVarsWrittenToByCommand.find(entry) != globalBVarsWrittenToByCommand.end()) {
-                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": assignment of (possibly) synchronizing command with label '" << entry.second << "' writes to global variable '" << entry.first << "'.");
-                    }
-                }
-                
-                globalBVarsWrittenToByCommand.insert(globalBVarsWrittenToByCommandInThisModule.begin(), globalBVarsWrittenToByCommandInThisModule.end());
-                globalIVarsWrittenToByCommand.insert(globalIVarsWrittenToByCommandInThisModule.begin(), globalIVarsWrittenToByCommandInThisModule.end());
-                
-            }
             
             // Check the commands of the modules.
             bool hasProbabilisticCommand = false;
@@ -654,7 +630,7 @@ namespace storm {
                     // Check the guard.
                     std::set<storm::expressions::Variable> containedVariables = command.getGuardExpression().getVariables();
                     bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
-                    STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard refers to unknown identifiers.");
+                    STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard " << command.getGuardExpression()  << " refers to unknown identifiers.");
                     STORM_LOG_THROW(command.getGuardExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'.");
                     
                     // Record which types of commands were seen.
@@ -762,6 +738,103 @@ namespace storm {
                 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
                 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers.");
             }
+            
+            if(lvl >= Program::ValidityCheckLevel::READYFORPROCESSING) {
+                // We check for each global variable and each labeled command, whether there is at most one instance writing to that variable.
+                std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
+                std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommand;
+                for(auto const& module : this->getModules()) {
+                    std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommandInThisModule;
+                    std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommandInThisModule;
+                    for (auto const& command : module.getCommands()) {
+                        if(!command.isLabeled()) continue;
+                        for (auto const& update : command.getUpdates()) {
+                             for (auto const& assignment : update.getAssignments()) {
+                                 if(this->globalBooleanVariableExists(assignment.getVariable().getName())) {
+                                     globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
+                                 }
+                                 else if(this->globalIntegerVariableExists(assignment.getVariable().getName())) {
+                                     globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
+                                 }
+                             }
+                        }
+                    }
+                    for(auto const& entry : globalIVarsWrittenToByCommandInThisModule) {
+                        if(globalIVarsWrittenToByCommand.find(entry) != globalIVarsWrittenToByCommand.end()) {
+                            STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": assignment of (possibly) synchronizing command with label '" << entry.second << "' writes to global variable '" << entry.first << "'.");
+                        }
+                    }
+                    for(auto const& entry : globalBVarsWrittenToByCommandInThisModule) {
+                        if(globalBVarsWrittenToByCommand.find(entry) != globalBVarsWrittenToByCommand.end()) {
+                            STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": assignment of (possibly) synchronizing command with label '" << entry.second << "' writes to global variable '" << entry.first << "'.");
+                        }
+                    }
+                }
+            }
+        }
+        
+        
+        Program Program::simplify() {
+            std::vector<Module> newModules;
+            std::vector<Constant> newConstants = this->getConstants();
+            for (auto const& module : this->getModules()) {
+                std::map<storm::expressions::Variable, storm::expressions::Expression> booleanVars;
+                std::map<storm::expressions::Variable, storm::expressions::Expression> integerVars;
+                for (auto const& variable : module.getBooleanVariables()) {
+                    booleanVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
+                }
+                for (auto const& variable : module.getIntegerVariables()) {
+                    integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
+                }
+                
+                for (auto const& command : module.getCommands()) {
+                    // Check all updates.
+                    for (auto const& update : command.getUpdates()) {
+                        // Check all assignments.
+                        for (auto const& assignment : update.getAssignments()) {
+                            auto bit = booleanVars.find(assignment.getVariable());
+                            if(bit != booleanVars.end()) {
+                                booleanVars.erase(bit);
+                            } else {
+                                auto iit = integerVars.find(assignment.getVariable());
+                                if(iit != integerVars.end()) {
+                                    integerVars.erase(iit);
+                                }
+                            }
+                        }
+                    }
+                }
+            
+                std::vector<storm::prism::BooleanVariable> newBVars;
+                for(auto const& variable : module.getBooleanVariables()) {
+                    if(booleanVars.count(variable.getExpressionVariable()) == 0) {
+                        newBVars.push_back(variable);
+                    }
+                }
+                std::vector<storm::prism::IntegerVariable> newIVars;
+                for(auto const& variable : module.getIntegerVariables()) {
+                    if(integerVars.count(variable.getExpressionVariable()) == 0) {
+                        newIVars.push_back(variable);
+                    }
+                }
+                
+                newModules.emplace_back(module.getName(), newBVars, newIVars, module.getCommands());
+                
+                for(auto const& entry : booleanVars) {
+                    newConstants.emplace_back(entry.first, entry.second);
+                }
+                
+                for(auto const& entry : integerVars) {
+                    newConstants.emplace_back(entry.first, entry.second);
+                }
+            }
+            
+            return replaceModulesAndConstantsInProgram(newModules, newConstants).substituteConstants();
+            
+        }
+        
+        Program Program::replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants) {
+            return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), false, getInitialConstruct(), getLabels(), "", 0, false);
         }
         
         storm::expressions::ExpressionManager const& Program::getManager() const {
@@ -816,5 +889,7 @@ namespace storm {
             return stream;
         }
         
+        
+        
     } // namespace prism
 } // namepsace storm
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 94bcf7353..6a124e4e0 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -24,6 +24,8 @@ namespace storm {
              */
             enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA};
             
+            enum class ValidityCheckLevel  : unsigned {VALIDINPUT = 0, READYFORPROCESSING = 1};
+            
             /*!
              * Creates a program with the given model type, undefined constants, global variables, modules, reward
              * models, labels and initial states.
@@ -45,9 +47,9 @@ namespace storm {
              * @param labels The labels defined for this program.
              * @param filename The filename in which the program is defined.
              * @param lineNumber The line number in which the program is defined.
-             * @param checkValidity If set to true, the program is checked for validity.
+             * @param finalModel If set to true, the program is checked for input-validity, as well as some post-processing.
              */
-            Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool checkValidity = true);
+            Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
             
             // Provide default implementations for constructors and assignments.
             Program() = default;
@@ -399,11 +401,17 @@ namespace storm {
              */
             Program substituteConstants() const;
             
+            /**
+             * Entry point for static analysis for simplify. As we use the same expression manager, we recommend to not use the original program any further. 
+             * @return A simplified, equivalent program.
+             */
+            Program simplify();
+            
             /*!
              * Checks the validity of the program. If the program is not valid, an exception is thrown with a message
              * that indicates the source of the problem.
              */
-            void checkValidity() const;
+            void checkValidity(Program::ValidityCheckLevel lvl = Program::ValidityCheckLevel::READYFORPROCESSING) const;
             
             friend std::ostream& operator<<(std::ostream& stream, Program const& program);
             
@@ -431,7 +439,7 @@ namespace storm {
             // The type of the model.
             ModelType modelType;
             
-            // The undefined constants of the program.
+            // The constants of the program.
             std::vector<Constant> constants;
             
             // A mapping from constant names to their corresponding indices.
@@ -490,6 +498,14 @@ namespace storm {
             
             // A mapping from variable names to the modules in which they were declared.
             std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
+            
+            /**
+             * Takes the current program and replaces all modules. As we reuse the expression manager, we recommend to not use the original program any further.
+             * @param newModules the modules which replace the old modules.
+             * @param newConstants the constants which replace the old constants.
+             * @return A program with the new modules and constants.
+             */
+            Program replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants);
         };
         
     } // namespace prism
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 3e1b820e4..8a28cb0e4 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -400,7 +400,10 @@ namespace storm {
                 boost::optional<storm::prism::Program> program;
                 if (settings.isSymbolicSet()) {
                     std::string const& programFile = settings.getSymbolicModelFilename();
-                    program = storm::parser::PrismParser::parse(programFile);
+                    program = storm::parser::PrismParser::parse(programFile).simplify();
+                    
+                    program->checkValidity();
+                    std::cout << program.get() << std::endl;
                 }
                 
                 // Then proceed to parsing the property (if given), since the model we are building may depend on the property.
@@ -416,68 +419,68 @@ namespace storm {
                     }
 					formulas.push_back(formula);
                 }
-				else if (settings.isPropertyFileSet()) {
-					std::cout << "Reading properties from " << settings.getPropertiesFilename() << std::endl;
+                else if (settings.isPropertyFileSet()) {
+                        std::cout << "Reading properties from " << settings.getPropertiesFilename() << std::endl;
 
-					std::ifstream inputFileStream(settings.getPropertiesFilename(), std::ios::in);
+                        std::ifstream inputFileStream(settings.getPropertiesFilename(), std::ios::in);
 
-					std::vector<std::string> properties;
+                        std::vector<std::string> properties;
 
-					if (inputFileStream.good()) {
-						try {
-							while (inputFileStream.good()) {
-								std::string prop;
-								std::getline(inputFileStream, prop);
-								if (!prop.empty()) {
-									properties.push_back(prop);
-								}
-							}
-						}
-						catch (std::exception& e) {
-							inputFileStream.close();
-							throw e;
-						}
-						inputFileStream.close();
-					} else {
-						STORM_LOG_ERROR("Unable to read property file.");
-					}
+                        if (inputFileStream.good()) {
+                                try {
+                                        while (inputFileStream.good()) {
+                                                std::string prop;
+                                                std::getline(inputFileStream, prop);
+                                                if (!prop.empty()) {
+                                                        properties.push_back(prop);
+                                                }
+                                        }
+                                }
+                                catch (std::exception& e) {
+                                        inputFileStream.close();
+                                        throw e;
+                                }
+                                inputFileStream.close();
+                        } else {
+                                STORM_LOG_ERROR("Unable to read property file.");
+                        }
 
-					for (std::string prop : properties) {
-						boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
-						try {
-							if (program) {
-								storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
-								formula = formulaParser.parseFromString(prop);
-							} else {
-								storm::parser::FormulaParser formulaParser;
-								formula = formulaParser.parseFromString(prop);
-							}
-							formulas.push_back(formula);
-						}
-						catch (storm::exceptions::WrongFormatException &e) {
-							STORM_LOG_WARN("Unable to parse line as formula: " << prop);
-						}
-					}
-					std::cout << "Parsed " << formulas.size() << " properties from file " << settings.getPropertiesFilename() << std::endl;
-				}
-                
-				for (boost::optional<std::shared_ptr<storm::logic::Formula>> formula : formulas) {
-					if (settings.isSymbolicSet()) {
+                        for (std::string prop : properties) {
+                                boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
+                                try {
+                                        if (program) {
+                                                storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
+                                                formula = formulaParser.parseFromString(prop);
+                                        } else {
+                                                storm::parser::FormulaParser formulaParser;
+                                                formula = formulaParser.parseFromString(prop);
+                                        }
+                                        formulas.push_back(formula);
+                                }
+                                catch (storm::exceptions::WrongFormatException &e) {
+                                        STORM_LOG_WARN("Unable to parse line as formula: " << prop);
+                                }
+                        }
+                        std::cout << "Parsed " << formulas.size() << " properties from file " << settings.getPropertiesFilename() << std::endl;
+                }
+
+                for (boost::optional<std::shared_ptr<storm::logic::Formula>> formula : formulas) {
+                        if (settings.isSymbolicSet()) {
 #ifdef STORM_HAVE_CARL
-						if (settings.isParametricSet()) {
-							buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
-						} else {
+                                if (settings.isParametricSet()) {
+                                        buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
+                                } else {
 #endif
-							buildAndCheckSymbolicModel<double>(program.get(), formula);
+                                        buildAndCheckSymbolicModel<double>(program.get(), formula);
 #ifdef STORM_HAVE_CARL
-						}
+                                }
 #endif
-					} else if (settings.isExplicitSet()) {
-						buildAndCheckExplicitModel<double>(formula);
-					} else {
-						STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
-					}
-				}
+                        } else if (settings.isExplicitSet()) {
+                                buildAndCheckExplicitModel<double>(formula);
+                        } else {
+                                STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
+                        }
+                }
             }
         }
     }

From 44e609ce86f994674f04df5ba9ea4d4473c42a55 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Mon, 10 Aug 2015 16:19:12 +0200
Subject: [PATCH 2/2] merge fix

Former-commit-id: 3fe4dba33f639d74debead984d249d27715a7deb
---
 src/storage/prism/Program.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 4a595181f..9d6f10c8f 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -12,7 +12,6 @@
 
 namespace storm {
     namespace prism {
-<<<<<<< HEAD
         Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool finalModel) 
         : LocatedInformation(filename, lineNumber), manager(manager),
             modelType(modelType), constants(constants), constantToIndexMap(),