more work on menu-game abstraction PRISM programs

Former-commit-id: acc54b7f15

src/CMakeLists.txt

@@ -35,7 +35,8 @@ file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJ
 file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp)
 file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp)
 file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp)
-file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp)
+file(GLOB STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp)
+file(GLOB STORM_STORAGE_PRISM_MENU_GAME_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/menu_games/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/menu_games/*.cpp)
 file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp)
 file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp)
 
@@ -80,6 +81,7 @@ source_group(storage FILES ${STORM_STORAGE_FILES})
 source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES})
 source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES})
 source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES})
+source_group(storage\\prism\\menu_games FILES ${STORM_STORAGE_PRISM_MENU_GAME_FILES})
 source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES})
 source_group(utility FILES ${STORM_UTILITY_FILES})
 

src/adapters/Z3ExpressionAdapter.h

@@ -47,6 +47,7 @@ namespace storm {
             z3::expr translateExpression(storm::expressions::Variable const& variable);
             
             storm::expressions::Expression translateExpression(z3::expr const& expr);
+            
             /*!
              * Finds the counterpart to the given z3 variable declaration.
              *
@@ -82,6 +83,7 @@ namespace storm {
              * @param variable The variable for which to create a Z3 counterpart.
              */
             z3::expr createVariable(storm::expressions::Variable const& variable);
+            
             // The manager that can be used to build expressions.
             storm::expressions::ExpressionManager& manager;
 

src/storage/prism/menu_games/AbstractCommand.cpp

@@ -0,0 +1,17 @@
+#include "src/storage/prism/menu_games/AbstractCommand.h"
+
+#include "src/storage/prism/Command.h"
+#include "src/storage/prism/Update.h"
+
+namespace storm {
+    namespace prism {
+        namespace menu_games {
+            template <storm::dd::DdType DdType, typename ValueType>
+            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::expressions::ExpressionManager& expressionManager, storm::prism::Command const& command, std::vector<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : expressionManager(expressionManager), smtSolver(smtSolverFactory.create(expressionManager)), predicates(initialPredicates), command(command) {
+                // Intentionally left empty.
+            }
+            
+            template class AbstractCommand<storm::dd::DdType::CUDD, double>;
+        }
+    }
+}

src/storage/prism/menu_games/AbstractCommand.h

@@ -0,0 +1,48 @@
+#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_
+#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_
+
+#include <memory>
+
+#include "src/storage/dd/DdType.h"
+#include "src/storage/expressions/Expression.h"
+
+#include "src/solver/SmtSolver.h"
+#include "src/utility/solver.h"
+
+namespace storm {
+    namespace prism {
+        // Forward-declare concrete command and update classes.
+        class Command;
+        
+        namespace menu_games {
+            template <storm::dd::DdType DdType, typename ValueType>
+            class AbstractCommand {
+            public:
+                /*!
+                 * Constructs an abstract command from the given command and the initial predicates.
+                 *
+                 * @param expressionManager The manager responsible for the expressions of the command.
+                 * @param command The concrete command for which to build the abstraction.
+                 * @param initialPredicates The initial set of predicates.
+                 * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
+                 */
+                AbstractCommand(storm::expressions::ExpressionManager& expressionManager, storm::prism::Command const& command, std::vector<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+                
+            private:
+                // The manager responsible for the expressions of the command and the SMT solvers.
+                storm::expressions::ExpressionManager& expressionManager;
+                
+                // An SMT responsible for this abstract command.
+                std::unique_ptr<storm::solver::SmtSolver> smtSolver;
+                
+                // The current set of predicates used in the abstraction.
+                std::vector<storm::expressions::Expression> predicates;
+                
+                // The concrete command this abstract command refers to.
+                std::reference_wrapper<Command const> command;
+            };
+        }
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_ */

src/storage/prism/menu_games/AbstractModule.cpp

@@ -0,0 +1,21 @@
+#include "src/storage/prism/menu_games/AbstractModule.h"
+
+#include "src/storage/prism/Module.h"
+
+namespace storm {
+    namespace prism {
+        namespace menu_games {
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            AbstractModule<DdType, ValueType>::AbstractModule(storm::expressions::ExpressionManager& expressionManager, storm::prism::Module const& module, std::vector<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : expressionManager(expressionManager), smtSolverFactory(smtSolverFactory), predicates(initialPredicates), commands(), module(module) {
+                
+                // For each concrete command, we create an abstract counterpart.
+                for (auto const& command : module.getCommands()) {
+                    commands.emplace_back(expressionManager, command, initialPredicates, smtSolverFactory);
+                }
+            }
+            
+            template class AbstractModule<storm::dd::DdType::CUDD, double>;
+        }
+    }
+}

src/storage/prism/menu_games/AbstractModule.h

@@ -0,0 +1,51 @@
+#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTMODULE_H_
+#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTMODULE_H_
+
+#include "src/storage/dd/DdType.h"
+
+#include "src/storage/prism/menu_games/AbstractCommand.h"
+
+#include "src/storage/expressions/Expression.h"
+
+#include "src/utility/solver.h"
+
+namespace storm {
+    namespace prism {
+        // Forward-declare concrete module class.
+        class Module;
+        
+        namespace menu_games {
+            template <storm::dd::DdType DdType, typename ValueType>
+            class AbstractModule {
+            public:
+                /*!
+                 * Constructs an abstract module from the given module and the initial predicates.
+                 *
+                 * @param expressionManager The manager responsible for the expressions of the command.
+                 * @param module The concrete module for which to build the abstraction.
+                 * @param initialPredicates The initial set of predicates.
+                 * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
+                 */
+                AbstractModule(storm::expressions::ExpressionManager& expressionManager, storm::prism::Module const& module, std::vector<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+                
+            private:
+                // The manager responsible for the expressions of the module and the SMT solvers.
+                storm::expressions::ExpressionManager& expressionManager;
+                
+                // 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 abstract commands of the abstract module.
+                std::vector<AbstractCommand<DdType, ValueType>> commands;
+                
+                // The concrete module this abstract module refers to.
+                std::reference_wrapper<Module const> module;
+            };
+        }
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTMODULE_H_ */

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -0,0 +1,64 @@
+#include "src/storage/prism/menu_games/AbstractProgram.h"
+
+#include <sstream>
+
+#include "src/storage/prism/Program.h"
+
+#include "src/storage/dd/CuddDdManager.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/WrongFormatException.h"
+
+namespace storm {
+    namespace prism {
+        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) : expressionManager(expressionManager), smtSolverFactory(std::move(smtSolverFactory)), predicates(initialPredicates), ddManager(new storm::dd::DdManager<DdType>()), predicateDdVariables(), commandDdVariable(), optionDdVariables(), 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.");
+                
+                uint_fast64_t totalNumberOfCommands = 0;
+                for (auto const& module : program.getModules()) {
+                    // If we were requested to add all guards to the set of predicates, we do so now.
+                    if (addAllGuards) {
+                        for (auto const& command : module.getCommands()) {
+                            predicates.push_back(command.getGuardExpression());
+                        }
+                    }
+                    
+                    totalNumberOfCommands += module.getNumberOfCommands();
+                }
+                
+                // Create DD variables for all predicates.
+                for (auto const& predicate : predicates) {
+                    std::stringstream stream;
+                    stream << predicate;
+                    predicateDdVariables.push_back(ddManager->addMetaVariable(stream.str()));
+                }
+                
+                // Create DD variable for the command encoding.
+                commandDdVariable = ddManager->addMetaVariable("command", 0, totalNumberOfCommands - 1);
+                
+                // Create DD variables encoding the nondeterministic choices of player 2.
+                // NOTE: currently we assume that 100 variables suffice, which corresponds to 2^100 possible choices.
+                // If for some reason this should not be enough, we could grow this vector dynamically, but odds are
+                // that it's impossible to treat such models in any event.
+                for (uint_fast64_t index = 0; index < 100; ++index) {
+                    optionDdVariables.push_back(ddManager->addMetaVariable("opt" + std::to_string(index)));
+                }
+                
+                // For each module of the concrete program, we create an abstract counterpart.
+                for (auto const& module : program.getModules()) {
+                    modules.emplace_back(expressionManager, module, predicates, *smtSolverFactory);
+                }
+            }
+            
+            // Explicitly instantiate the class.
+            template class AbstractProgram<storm::dd::DdType::CUDD, double>;
+            
+        }
+    }
+}

src/storage/prism/menu_games/AbstractProgram.h

@@ -0,0 +1,69 @@
+#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTPROGRAM_H_
+#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTPROGRAM_H_
+
+#include "src/storage/dd/DdType.h"
+
+#include "src/storage/prism/menu_games/AbstractModule.h"
+
+#include "src/storage/expressions/Expression.h"
+
+#include "src/utility/solver.h"
+
+namespace storm {
+    namespace dd {
+        template <storm::dd::DdType DdType>
+        class DdManager;
+    }
+    
+    namespace prism {
+        // Forward-declare concrete Program class.
+        class Program;
+        
+        namespace menu_games {
+            template <storm::dd::DdType DdType, typename ValueType>
+            class AbstractProgram {
+            public:
+                /*!
+                 * Constructs an abstract program from the given program and the initial predicates.
+                 *
+                 * @param expressionManager The manager responsible for the expressions of the program.
+                 * @param program The concrete program for which to build the abstraction.
+                 * @param initialPredicates The initial set of predicates.
+                 * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
+                 * @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates.
+                 */
+                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:
+                // The manager responsible for the expressions of the program and the SMT solvers.
+                storm::expressions::ExpressionManager& expressionManager;
+                
+                // A factory that can be used to create new SMT solvers.
+                std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
+                
+                // The current set of predicates used in the abstraction.
+                std::vector<storm::expressions::Expression> predicates;
+                
+                // The manager responsible for the DDs.
+                std::shared_ptr<storm::dd::DdManager<DdType>> ddManager;
+                
+                // The DD variables corresponding to the predicates.
+                std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> predicateDdVariables;
+                
+                // The DD variable encoding the command (i.e., the nondeterministic choices of player 1).
+                std::pair<storm::expressions::Variable, storm::expressions::Variable> commandDdVariable;
+                
+                // The DD variables encoding the nondeterministic choices of player 2.
+                std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> optionDdVariables;
+                
+                // The abstract modules of the abstract program.
+                std::vector<AbstractModule<DdType, ValueType>> modules;
+                
+                // The concrete program this abstract program refers to.
+                std::reference_wrapper<Program const> program;
+            };
+        }
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTPROGRAM_H_ */