The determined relevant predicates are now added to the SMT solver of an abstract command. Also, variable bounds are enforced.

Former-commit-id: 703b49e732

src/storage/prism/IntegerVariable.cpp

@@ -14,6 +14,10 @@ namespace storm {
             return this->upperBoundExpression;
         }
         
+        storm::expressions::Expression IntegerVariable::getRangeExpression() const {
+            return this->getLowerBoundExpression() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBoundExpression();
+        }
+        
         IntegerVariable IntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
         }

src/storage/prism/IntegerVariable.h

@@ -45,6 +45,13 @@ namespace storm {
              */
             storm::expressions::Expression const& getUpperBoundExpression() const;
             
+            /*!
+             * Retrieves an expression that characterizes the valid range of the variable.
+             *
+             * @return An expression that characterizes the valid range of the variable.
+             */
+            storm::expressions::Expression getRangeExpression() const;
+            
             /*!
              * Substitutes all identifiers in the boolean variable according to the given map.
              *

src/storage/prism/Module.cpp

@@ -54,6 +54,14 @@ namespace storm {
             return result;
         }
         
+        std::vector<storm::expressions::Expression> Module::getAllRangeExpressions() const {
+            std::vector<storm::expressions::Expression> result;
+            for (auto const& integerVariable : this->integerVariables) {
+                result.push_back(integerVariable.getRangeExpression());
+            }
+            return result;
+        }
+
         std::size_t Module::getNumberOfCommands() const {
             return this->commands.size();
         }

src/storage/prism/Module.h

@@ -104,6 +104,13 @@ namespace storm {
              */
             std::set<storm::expressions::Variable> getAllExpressionVariables() const;
             
+            /*!
+             * Retrieves a set of expressions characterizing the legal ranges of all variables declared in the module.
+             *
+             * @return The expressions characterizing the legal ranges of all variables declared in the module.
+             */
+            std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
+            
             /*!
              * Retrieves the number of commands of this module.
              *

src/storage/prism/Program.cpp

@@ -215,6 +215,20 @@ namespace storm {
             return result;
         }
         
+        std::vector<storm::expressions::Expression> Program::getAllRangeExpressions() const {
+            std::vector<storm::expressions::Expression> result;
+            for (auto const& globalIntegerVariable : this->globalIntegerVariables) {
+                result.push_back(globalIntegerVariable.getRangeExpression());
+            }
+            
+            for (auto const& module : modules) {
+                std::vector<storm::expressions::Expression> moduleRangeExpressions = module.getAllRangeExpressions();
+                result.insert(result.end(), moduleRangeExpressions.begin(), moduleRangeExpressions.end());
+            }
+            
+            return result;
+        }
+        
         bool Program::globalBooleanVariableExists(std::string const& variableName) const {
             return this->globalBooleanVariableToIndexMap.count(variableName) > 0;
         }

src/storage/prism/Program.h

@@ -173,6 +173,13 @@ namespace storm {
              */
             std::set<storm::expressions::Variable> getAllExpressionVariables() const;
             
+            /*!
+             * Retrieves a set of expressions characterizing the legal ranges of all variables.
+             *
+             * @return The expressions characterizing the legal ranges of all variables.
+             */
+            std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
+            
             /*!
              * Retrieves the number of global boolean variables of the program.
              *

src/storage/prism/Update.cpp

@@ -31,6 +31,16 @@ namespace storm {
             return this->getAssignments()[variableIndexPair->second];
         }
         
+        std::map<storm::expressions::Variable, storm::expressions::Expression> Update::getAsVariableToExpressionMap() const {
+            std::map<storm::expressions::Variable, storm::expressions::Expression> result;
+            
+            for (auto const& assignment : this->getAssignments()) {
+                result.emplace(assignment.getVariable(), assignment.getExpression());
+            }
+            
+            return result;
+        }
+        
         uint_fast64_t Update::getGlobalIndex() const {
             return this->globalIndex;
         }

src/storage/prism/Update.h

@@ -59,6 +59,13 @@ namespace storm {
              */
             storm::prism::Assignment const& getAssignment(std::string const& variableName) const;
             
+            /*!
+             * Creates a mapping representation of this update.
+             *
+             * @return A mapping from variables to expressions.
+             */
+            std::map<storm::expressions::Variable, storm::expressions::Expression> getAsVariableToExpressionMap() const;
+            
             /*!
              * Retrieves the global index of the update, that is, a unique index over all modules.
              *
@@ -73,6 +80,7 @@ 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. 
              * 

src/storage/prism/menu_games/AbstractCommand.cpp

@@ -3,6 +3,9 @@
 #include "src/storage/prism/menu_games/AbstractionExpressionInformation.h"
 #include "src/storage/prism/menu_games/AbstractionDdInformation.h"
 
+#include "src/storage/dd/CuddDdManager.h"
+#include "src/storage/dd/CuddAdd.h"
+
 #include "src/storage/prism/Command.h"
 #include "src/storage/prism/Update.h"
 
@@ -10,8 +13,15 @@ namespace storm {
     namespace prism {
         namespace menu_games {
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.expressionManager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command) {
-                // Intentionally left empty.
+            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.expressionManager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.ddManager->getAddZero(), 0)) {
+
+                // Make the second component of relevant predicates have the right size.
+                relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
+                
+                // Assert all range expressions to enforce legal variable values.
+                for (auto const& rangeExpression : expressionInformation.rangeExpressions) {
+                    smtSolver->add(rangeExpression);
+                }
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -42,6 +52,94 @@ namespace storm {
                 return result;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> AbstractCommand<DdType, ValueType>::computeRelevantPredicates() const {
+                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> result;
+
+                for (auto const& update : command.get().getUpdates()) {
+                    std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> relevantUpdatePredicates = computeRelevantPredicates(update.getAssignments());
+                    result.first.insert(relevantUpdatePredicates.first.begin(), relevantUpdatePredicates.first.end());
+                    result.second.push_back(relevantUpdatePredicates.second);
+                }
+                
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            bool AbstractCommand<DdType, ValueType>::relevantPredicatesChanged(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) const {
+                if (newRelevantPredicates.first.size() > relevantPredicatesAndVariables.first.size()) {
+                    return true;
+                }
+                
+                for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) {
+                    if (newRelevantPredicates.second[index].size() > relevantPredicatesAndVariables.second[index].size()) {
+                        return true;
+                    }
+                }
+                
+                return false;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> AbstractCommand<DdType, ValueType>::declareNewVariables(std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldRelevantPredicates, std::set<uint_fast64_t> const& newRelevantPredicates) {
+                std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> result;
+                
+                auto oldIt = oldRelevantPredicates.begin();
+                auto oldIte = oldRelevantPredicates.end();
+                for (auto newIt = newRelevantPredicates.begin(), newIte = newRelevantPredicates.end(); newIt != newIte; ++newIt) {
+                    // If the new variable does not yet exist as a source variable, we create it now.
+                    if (oldIt == oldIte || oldIt->second != *newIt) {
+                        result.push_back(std::make_pair(expressionInformation.expressionManager.declareFreshBooleanVariable(), *newIt));
+                    }
+                }
+                
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AbstractCommand<DdType, ValueType>::addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) {
+                // Determine and add new relevant source predicates.
+                std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first);
+                for (auto const& element : newSourceVariables) {
+                    smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second]));
+                }
+                
+                // Insert the new variables into the record of relevant source variables.
+                relevantPredicatesAndVariables.first.insert(relevantPredicatesAndVariables.first.end(), newSourceVariables.begin(), newSourceVariables.end());
+                std::sort(relevantPredicatesAndVariables.first.begin(), relevantPredicatesAndVariables.first.end(), [] (std::pair<storm::expressions::Variable, uint_fast64_t> const& first, std::pair<storm::expressions::Variable, uint_fast64_t> const& second) { return first.second < second.second; } );
+                
+                // Do the same for every update.
+                for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) {
+                    std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newTargetVariables = declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
+                    for (auto const& element : newSourceVariables) {
+                        smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second].substitute(command.get().getUpdate(index).getAsVariableToExpressionMap())));
+                    }
+                    
+                    relevantPredicatesAndVariables.second[index].insert(relevantPredicatesAndVariables.second[index].end(), newTargetVariables.begin(), newTargetVariables.end());
+                    std::sort(relevantPredicatesAndVariables.second[index].begin(), relevantPredicatesAndVariables.second[index].end(), [] (std::pair<storm::expressions::Variable, uint_fast64_t> const& first, std::pair<storm::expressions::Variable, uint_fast64_t> const& second) { return first.second < second.second; } );
+                }
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::pair<storm::dd::Add<DdType>, uint_fast64_t> AbstractCommand<DdType, ValueType>::computeDd() {
+                // First, we check whether there is work to be done by recomputing the relevant predicates and checking
+                // whether they changed.
+                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> newRelevantPredicates;
+                bool recomputeDd = this->relevantPredicatesChanged(newRelevantPredicates);
+                
+                if (recomputeDd) {
+                    relevantPredicates = std::move(newRelevantPredicates);
+                    
+                    
+                    
+                    storm::dd::Add<DdType> result;
+                    
+                    return result;
+                } else {
+                    return cachedDd;
+                }
+            }
+            
             template class AbstractCommand<storm::dd::DdType::CUDD, double>;
         }
     }

src/storage/prism/menu_games/AbstractCommand.h

@@ -37,9 +37,18 @@ namespace storm {
                  */
                 AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
                 
+                /*!
+                 * Computes the abstraction of the command wrt. to the current set of predicates.
+                 *
+                 * @return The abstraction of the command in the form of an ADD together with the number of DD variables
+                 * used to encode the choices of player 2.
+                 */
+                std::pair<storm::dd::Add<DdType>, uint_fast64_t> computeDd();
+                
             private:
                 /*!
-                 * Determines the relevant predicates for source as well as target states.
+                 * Determines the relevant predicates for source as well as target states wrt. to the given assignments
+                 * (that, for example, form an update).
                  *
                  * @param assignments The assignments that are to be considered.
                  * @return A pair whose first component represents the relevant source predicates and whose second
@@ -47,6 +56,37 @@ namespace storm {
                  */
                 std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> computeRelevantPredicates(std::vector<storm::prism::Assignment> const& assignments) const;
                 
+                /*!
+                 * Determines the relevant predicates for source as well as target states.
+                 *
+                 * @return A pair whose first component represents the relevant source predicates and whose second
+                 * component represents the relevant target state predicates.
+                 */
+                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> computeRelevantPredicates() const;
+
+                /*!
+                 * Checks whether the relevant predicates changed.
+                 *
+                 * @param newRelevantPredicates The new relevant predicates.
+                 */
+                bool relevantPredicatesChanged(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) const;
+                
+                /*!
+                 * Declares variables for the predicates that were added.
+                 *
+                 * @param oldRelevantPredicates The old relevant predicates (and the corresponding variables).
+                 * @return Pairs of variable and predicate (indices) for the new relevant predicates.
+                 */
+                std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> declareNewVariables(std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldRelevantPredicates, std::set<uint_fast64_t> const& newRelevantPredicates);
+                
+                /*!
+                 * Takes the new relevant predicates and creates the appropriate variables and assertions for the ones
+                 * that are currently missing.
+                 *
+                 * @param newRelevantPredicates The new relevant predicates.
+                 */
+                void addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates);
+                
                 // An SMT responsible for this abstract command.
                 std::unique_ptr<storm::solver::SmtSolver> smtSolver;
 
@@ -61,6 +101,13 @@ namespace storm {
                 
                 // The partition of variables and expressions.
                 VariablePartition variablePartition;
+                
+                // The currently relevant source/target predicates and the corresponding variables.
+                std::pair<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>, std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>>> relevantPredicatesAndVariables;
+                
+                // The most recent result of a call to computeDd. If nothing has changed regarding the relevant
+                // predicates, this result may be reused.
+                std::pair<storm::dd::Add<DdType>, uint_fast64_t> cachedDd;
             };
         }
     }

src/storage/prism/menu_games/AbstractModule.cpp

@@ -3,6 +3,9 @@
 #include "src/storage/prism/menu_games/AbstractionExpressionInformation.h"
 #include "src/storage/prism/menu_games/AbstractionDdInformation.h"
 
+#include "src/storage/dd/CuddDdManager.h"
+#include "src/storage/dd/CuddAdd.h"
+
 #include "src/storage/prism/Module.h"
 
 namespace storm {
@@ -10,7 +13,7 @@ namespace storm {
         namespace menu_games {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractModule<DdType, ValueType>::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), commands(), module(module) {
+            AbstractModule<DdType, ValueType>::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), ddInformation(ddInformation), commands(), module(module) {
                 
                 // For each concrete command, we create an abstract counterpart.
                 for (auto const& command : module.getCommands()) {
@@ -18,6 +21,23 @@ namespace storm {
                 }
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Add<DdType> AbstractModule<DdType, ValueType>::computeDd() {
+                // First, we retrieve the abstractions of all commands.
+                std::vector<std::pair<storm::dd::Add<DdType>, uint_fast64_t>> commandDdsAndUsedOptionVariableCounts;
+                for (auto const& command : commands) {
+                    commandDdsAndUsedOptionVariableCounts.push_back(command.computeDd());
+                }
+                
+                // Then, we build the module ADD by adding the single command DDs. We need to make sure that all command
+                // DDs use the same amount DD variable encoding the choices of player 2.
+                storm::dd::Add<DdType> result = ddInformation.ddManager->getAddZero();
+                
+                // TODO
+                
+                return result;
+            }
+            
             template class AbstractModule<storm::dd::DdType::CUDD, double>;
         }
     }

src/storage/prism/menu_games/AbstractModule.h

@@ -33,12 +33,19 @@ namespace storm {
                  */
                 AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
                 
+                /*!
+                 * Computes the abstraction of the module wrt. to the current set of predicates.
+                 *
+                 * @return The abstraction of the module in the form of an ADD.
+                 */
+                storm::dd::Add<DdType> computeDd();
+                
             private:
                 // A factory that can be used to create new SMT solvers.
                 storm::utility::solver::SmtSolverFactory const& smtSolverFactory;
                 
-                // The current set of predicates used in the abstraction.
-                std::vector<storm::expressions::Expression> predicates;
+                // The DD-related information.
+                AbstractionDdInformation<DdType, ValueType> const& ddInformation;
                 
                 // The abstract commands of the abstract module.
                 std::vector<AbstractCommand<DdType, ValueType>> commands;

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -5,6 +5,7 @@
 #include "src/storage/prism/Program.h"
 
 #include "src/storage/dd/CuddDdManager.h"
+#include "src/storage/dd/CuddAdd.h"
 
 #include "src/utility/macros.h"
 #include "src/utility/solver.h"
@@ -15,15 +16,12 @@ namespace storm {
         namespace menu_games {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>(new storm::dd::DdManager<DdType>())), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables()), modules(), program(program) {
+            AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program) {
                 
                 // For now, we assume that there is a single module. If the program has more than one module, it needs
                 // to be flattened before the procedure.
                 STORM_LOG_THROW(program.getNumberOfModules() == 1, storm::exceptions::WrongFormatException, "Cannot create abstract program from program containing too many modules.");
                 
-                std::set<storm::expressions::Variable> allVariables;
-                
-                
                 uint_fast64_t totalNumberOfCommands = 0;
                 uint_fast64_t maximalUpdateCount = 0;
                 for (auto const& module : program.getModules()) {
@@ -65,6 +63,12 @@ namespace storm {
                 }
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Add<DdType> AbstractProgram<DdType, ValueType>::computeDd() {
+                // As long as there is only one module, we build its game representation and return it.
+                return modules.front().computeDd();
+            }
+            
             // Explicitly instantiate the class.
             template class AbstractProgram<storm::dd::DdType::CUDD, double>;
             

src/storage/prism/menu_games/AbstractProgram.h

@@ -36,8 +36,14 @@ namespace storm {
                  */
                 AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::unique_ptr<storm::utility::solver::SmtSolverFactory>(new storm::utility::solver::SmtSolverFactory()), bool addAllGuards = false);
                 
-            private:
+                /*!
+                 * Uses the current set of predicates to derive the abstract menu game in the form of an ADD.
+                 *
+                 * @return The ADD representing the game.
+                 */
+                storm::dd::Add<DdType> computeDd();
                 
+            private:
                 // A factory that can be used to create new SMT solvers.
                 std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
                 

src/storage/prism/menu_games/AbstractionDdInformation.cpp

@@ -10,6 +10,8 @@ namespace storm {
             AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager) : ddManager(manager) {
                 // Intentionally left empty.
             }
+         
+            template class AbstractionDdInformation<storm::dd::DdType::CUDD, double>;
             
         }
     }

src/storage/prism/menu_games/AbstractionExpressionInformation.cpp

@@ -7,7 +7,7 @@ namespace storm {
     namespace prism {
         namespace menu_games {
             
-            AbstractionExpressionInformation::AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector<storm::expressions::Expression> const& predicates, std::set<storm::expressions::Variable> const& variables) : expressionManager(expressionManager), predicates(predicates), variables(variables) {
+            AbstractionExpressionInformation::AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector<storm::expressions::Expression> const& predicates, std::set<storm::expressions::Variable> const& variables, std::vector<storm::expressions::Expression> const& rangeExpressions) : expressionManager(expressionManager), predicates(predicates), variables(variables), rangeExpressions(rangeExpressions) {
                 // Intentionally left empty.
             }
             

src/storage/prism/menu_games/AbstractionExpressionInformation.h

@@ -21,7 +21,7 @@ namespace storm {
                  *
                  * @param expressionManager The expression manager to use.
                  */
-                AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector<storm::expressions::Expression> const& predicates = std::vector<storm::expressions::Expression>(), std::set<storm::expressions::Variable> const& variables = std::set<storm::expressions::Variable>());
+                AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector<storm::expressions::Expression> const& predicates = std::vector<storm::expressions::Expression>(), std::set<storm::expressions::Variable> const& variables = std::set<storm::expressions::Variable>(), std::vector<storm::expressions::Expression> const& rangeExpressions = std::vector<storm::expressions::Expression>());
                 
                 // The manager responsible for the expressions of the program and the SMT solvers.
                 storm::expressions::ExpressionManager& expressionManager;
@@ -31,6 +31,9 @@ namespace storm {
                 
                 // The set of all variables.
                 std::set<storm::expressions::Variable> variables;
+
+                // The expression characterizing the legal ranges of all variables.
+                std::vector<storm::expressions::Expression> rangeExpressions;
             };
         }
     }

test/functional/abstraction/PrismMenuGameTest.cpp

@@ -0,0 +1,29 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_MSAT
+
+#include "src/parser/PrismParser.h"
+
+#include "src/storage/prism/menu_games/AbstractProgram.h"
+
+#include "src/storage/expressions/Expression.h"
+
+#include "src/storage/dd/CuddDd.h"
+#include "src/storage/dd/CuddAdd.h"
+#include "src/storage/dd/CuddBdd.h"
+
+#include "src/utility/solver.h"
+
+TEST(PrismMenuGame, CommandAbstractionTest) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+}
+
+#endif