more work on games

Former-commit-id: d89f025da4

src/storage/prism/menu_games/AbstractCommand.cpp

@@ -11,6 +11,8 @@
 #include "src/storage/prism/Command.h"
 #include "src/storage/prism/Update.h"
 
+#include "src/utility/macros.h"
+
 namespace storm {
     namespace prism {
         namespace menu_games {
@@ -24,6 +26,80 @@ namespace storm {
                 for (auto const& rangeExpression : expressionInformation.rangeExpressions) {
                     smtSolver->add(rangeExpression);
                 }
+                
+                // Assert the guard of the command.
+                smtSolver->add(command.getGuardExpression());
+
+                // Refine the command based on all initial predicates.
+                std::vector<uint_fast64_t> allPredicateIndices(expressionInformation.predicates.size());
+                for (auto index = 0; index < expressionInformation.predicates.size(); ++index) {
+                    allPredicateIndices[index] = index;
+                }
+                this->refine(allPredicateIndices);
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
+                // Add all predicates to the variable partition.
+                for (auto predicateIndex : predicates) {
+                    variablePartition.addExpression(expressionInformation.predicates[predicateIndex]);
+                }
+                
+                STORM_LOG_TRACE("Current variable partition is: " << variablePartition);
+                
+                // Next, 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 = this->computeRelevantPredicates();
+                
+                // If the DD does not need recomputation, we can return the cached result.
+                bool recomputeDd = this->relevantPredicatesChanged(newRelevantPredicates);
+                if (!recomputeDd) {
+                    // If the new predicates are unrelated to the BDD of this command, we need to multiply their identities.
+                    for (auto predicateIndex : predicates) {
+                        cachedDd.first &= ddInformation.predicateIdentities[predicateIndex];
+                    }
+                } else {
+                    // If the DD needs recomputation, it is because of new relevant predicates, so we need to assert the appropriate clauses in the solver.
+                    addMissingPredicates(newRelevantPredicates);
+                    
+                    // Finally recompute the cached BDD.
+                    this->recomputeCachedBdd();
+                }
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AbstractCommand<DdType, ValueType>::recomputeCachedBdd() {
+                STORM_LOG_TRACE("Recomputing BDD for command " << command.get());
+                
+                // Create a mapping from source state DDs to their distributions.
+                std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
+                smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); return true; } );
+                
+                // Now we search for the maximal number of choices of player 2 to determine how many DD variables we
+                // need to encode the nondeterminism.
+                uint_fast64_t maximalNumberOfChoices = 0;
+                for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
+                    maximalNumberOfChoices = std::max(maximalNumberOfChoices, static_cast<uint_fast64_t>(sourceDistributionsPair.second.size()));
+                }
+                
+                uint_fast64_t numberOfVariablesNeeded = static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices)));
+                
+                // Finally, build overall result.
+                storm::dd::Bdd<DdType> resultBdd = ddInformation.manager->getBddZero();
+                for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
+                    uint_fast64_t distributionIndex = 0;
+                    storm::dd::Bdd<DdType> allDistributions = ddInformation.manager->getBddZero();
+                    for (auto const& distribution : sourceDistributionsPair.second) {
+                        allDistributions |= distribution && ddInformation.encodeDistributionIndex(numberOfVariablesNeeded, distributionIndex);
+                    }
+                    resultBdd |= sourceDistributionsPair.first && allDistributions;
+                }
+                
+                resultBdd &= computeMissingSourceStateIdentities();
+                resultBdd &= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex());
+                
+                // Cache the result before returning it.
+                cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded);
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -126,6 +202,7 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
+                STORM_LOG_TRACE("Building source state BDD.");
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
                 for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
                     if (model.getBooleanValue(variableIndexPair.first)) {
@@ -139,11 +216,13 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const {
+                STORM_LOG_TRACE("Building distribution BDD.");
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
                 
                 for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
                     storm::dd::Bdd<DdType> updateBdd = ddInformation.manager->getBddOne();
 
+                    // Translate block variables for this update into a successor block.
                     for (auto const& variableIndexPair : relevantPredicatesAndVariables.second[updateIndex]) {
                         if (model.getBooleanValue(variableIndexPair.first)) {
                             updateBdd &= ddInformation.predicateBdds[variableIndexPair.second].second;
@@ -159,9 +238,12 @@ namespace storm {
                     auto secondIt = relevantPredicatesAndVariables.second[updateIndex].begin();
                     auto secondIte = relevantPredicatesAndVariables.second[updateIndex].end();
                     
+                    // Go through all relevant source predicates. This is guaranteed to be a superset of the set of
+                    // relevant successor predicates for any update.
                     for (; firstIt != firstIte; ++firstIt) {
+                        // If the predicates do not match, there is a predicate missing, so we need to add its identity.
                         if (secondIt == secondIte || firstIt->second != secondIt->second) {
-                            result &= ddInformation.predicateIdentities[firstIt->second];
+                            updateBdd &= ddInformation.predicateIdentities[firstIt->second];
                         } else if (secondIt != secondIte) {
                             ++secondIt;
                         }
@@ -172,49 +254,23 @@ namespace storm {
                 
                 return result;
             }
-                        
+            
             template <storm::dd::DdType DdType, typename ValueType>
-            std::pair<storm::dd::Bdd<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 = this->computeRelevantPredicates();
-
-                // If the DD does not need recomputation, we can return the cached result.
-                bool recomputeDd = this->relevantPredicatesChanged(newRelevantPredicates);
-                if (!recomputeDd) {
-                    // FIXME: multiply identity of new predicates
-                    return cachedDd;
-                }
-                
-                // If the DD needs recomputation, it is because of new relevant predicates, so we need to assert the appropriate clauses in the solver.
-                addMissingPredicates(newRelevantPredicates);
-
-                // Create a mapping from source state DDs to their distributions.
-                std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
-                smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); return true; } );
-                
-                // Now we search for the maximal number of choices of player 2 to determine how many DD variables we
-                // need to encode the nondeterminism.
-                uint_fast64_t maximalNumberOfChoices = 0;
-                for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
-                    maximalNumberOfChoices = std::max(maximalNumberOfChoices, static_cast<uint_fast64_t>(sourceDistributionsPair.second.size()));
-                }
-                
-                uint_fast64_t numberOfVariablesNeeded = static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices)));
+            storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingSourceStateIdentities() const {
+                auto relevantIt = relevantPredicatesAndVariables.first.begin();
+                auto relevantIte = relevantPredicatesAndVariables.first.end();
                 
-                // Finally, build overall result.
-                storm::dd::Bdd<DdType> resultBdd = ddInformation.manager->getBddZero();
-                for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
-                    uint_fast64_t distributionIndex = 0;
-                    storm::dd::Bdd<DdType> allDistributions = ddInformation.manager->getBddZero();
-                    for (auto const& distribution : sourceDistributionsPair.second) {
-                        allDistributions |= distribution && ddInformation.encodeDistributionIndex(numberOfVariablesNeeded, distributionIndex);
+                storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
+                for (uint_fast64_t predicateIndex = 0; predicateIndex < expressionInformation.predicates.size(); ++predicateIndex) {
+                    if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
+                        result &= ddInformation.predicateIdentities[predicateIndex];
                     }
-                    resultBdd |= sourceDistributionsPair.first && allDistributions;
                 }
-                
-                // Cache the result before returning it.
-                cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded);
+                return result;
+            }
+
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> AbstractCommand<DdType, ValueType>::getAbstractBdd() {
                 return cachedDd;
             }
             

src/storage/prism/menu_games/AbstractCommand.h

@@ -39,13 +39,20 @@ namespace storm {
                  */
                 AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
                 
+                /*!
+                 * Refines the abstract command with the given predicates.
+                 *
+                 * @param predicates The new predicates.
+                 */
+                void refine(std::vector<uint_fast64_t> const& predicates);
+                
                 /*!
                  * Computes the abstraction of the command wrt. to the current set of predicates.
                  *
                  * @return The abstraction of the command in the form of a BDD together with the number of DD variables
                  * used to encode the choices of player 2.
                  */
-                std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> computeDd();
+                std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> getAbstractBdd();
                 
             private:
                 /*!
@@ -105,6 +112,19 @@ namespace storm {
                  */
                 storm::dd::Bdd<DdType> getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const;
                 
+                /*!
+                 * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change.
+                 */
+                void recomputeCachedBdd();
+                
+                /*!
+                 * Computes the missing source state identities.
+                 *
+                 * @return A BDD that represents the source state identities for predicates that are irrelevant for the
+                 * source states.
+                 */
+                storm::dd::Bdd<DdType> computeMissingSourceStateIdentities() const;
+                
                 // An SMT responsible for this abstract command.
                 std::unique_ptr<storm::solver::SmtSolver> smtSolver;
 

src/storage/prism/menu_games/AbstractModule.cpp

@@ -22,19 +22,28 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Bdd<DdType> AbstractModule<DdType, ValueType>::computeDd() {
+            void AbstractModule<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
+                for (auto& command : commands) {
+                    command.refine(predicates);
+                }
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> AbstractModule<DdType, ValueType>::getAbstractBdd() {
                 // First, we retrieve the abstractions of all commands.
                 std::vector<std::pair<storm::dd::Bdd<DdType>, uint_fast64_t>> commandDdsAndUsedOptionVariableCounts;
+                uint_fast64_t maximalNumberOfUsedOptionVariables = 0;
                 for (auto& command : commands) {
-                    commandDdsAndUsedOptionVariableCounts.push_back(command.computeDd());
+                    commandDdsAndUsedOptionVariableCounts.push_back(command.getAbstractBdd());
+                    maximalNumberOfUsedOptionVariables = std::max(maximalNumberOfUsedOptionVariables, commandDdsAndUsedOptionVariableCounts.back().second);
                 }
                 
-                // Then, we build the module ADD by adding the single command DDs. We need to make sure that all command
+                // Then, we build the module BDD 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::Bdd<DdType> result = ddInformation.manager->getBddZero();
-                
-                // TODO
-                
+                for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) {
+                    result |= commandDd.first && ddInformation.getMissingOptionVariableCube(commandDd.second, maximalNumberOfUsedOptionVariables);
+                }
                 return result;
             }
             

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);
                 
+                /*!
+                 * Refines the abstract module with the given predicates.
+                 *
+                 * @param predicates The new predicate indices.
+                 */
+                void refine(std::vector<uint_fast64_t> const& predicates);
+                
                 /*!
                  * Computes the abstraction of the module wrt. to the current set of predicates.
                  *
                  * @return The abstraction of the module in the form of a BDD.
                  */
-                storm::dd::Bdd<DdType> computeDd();
+                storm::dd::Bdd<DdType> getAbstractBdd();
                 
             private:
                 // A factory that can be used to create new SMT solvers.

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -56,15 +56,17 @@ namespace storm {
                 
                 // For each module of the concrete program, we create an abstract counterpart.
                 for (auto const& module : program.getModules()) {
-                    modules.emplace_back(module, expressionInformation, ddInformation, *smtSolverFactory);
+                    modules.emplace_back(module, expressionInformation, ddInformation, *this->smtSolverFactory);
                 }
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Add<DdType> AbstractProgram<DdType, ValueType>::computeDd() {
+            storm::dd::Add<DdType> AbstractProgram<DdType, ValueType>::getAbstractAdd() {
                 // As long as there is only one module, we build its game representation and return it.
+                
+                
                 // FIXME: multiply with probabilities for updates.
-                return modules.front().computeDd().toAdd();
+                return modules.front().getAbstractBdd().toAdd();
             }
             
             // Explicitly instantiate the class.

src/storage/prism/menu_games/AbstractProgram.h

@@ -41,7 +41,7 @@ namespace storm {
                  *
                  * @return The ADD representing the game.
                  */
-                storm::dd::Add<DdType> computeDd();
+                storm::dd::Add<DdType> getAbstractAdd();
                 
             private:
                 // A factory that can be used to create new SMT solvers.

src/storage/prism/menu_games/AbstractionDdInformation.cpp

@@ -37,10 +37,21 @@ namespace storm {
                 stream << predicate;
                 std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable = manager->addMetaVariable(stream.str());
                 predicateDdVariables.push_back(newMetaVariable);
-                predicateBdds.emplace_back(manager->getRange(newMetaVariable.first), manager->getRange(newMetaVariable.second));
+                predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1));
                 predicateIdentities.push_back(manager->getIdentity(newMetaVariable.first).equals(manager->getIdentity(newMetaVariable.second)).toBdd());
             }
          
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> AbstractionDdInformation<DdType, ValueType>::getMissingOptionVariableCube(uint_fast64_t lastUsed, uint_fast64_t lastToBe) const {
+                storm::dd::Bdd<DdType> result = manager->getBddOne();
+                
+                for (uint_fast64_t index = lastUsed + 1; index <= lastToBe; ++index) {
+                    result &= optionDdVariables[index].second;
+                }
+                
+                return result;
+            }
+            
             template struct AbstractionDdInformation<storm::dd::DdType::CUDD, double>;
             
         }

src/storage/prism/menu_games/AbstractionDdInformation.h

@@ -50,6 +50,15 @@ namespace storm {
                  */
                 void addPredicate(storm::expressions::Expression const& predicate);
                 
+                /*!
+                 * Retrieves the cube of option variables in the range (lastUsed, lastToBe] the given indices.
+                 *
+                 * @param lastUsed The last variable before the range to return.
+                 * @param lastToBe The last variable of the range to return.
+                 * @return The cube of variables in the given range.
+                 */
+                storm::dd::Bdd<DdType> getMissingOptionVariableCube(uint_fast64_t lastUsed, uint_fast64_t lastToBe) const;
+                
                 // The manager responsible for the DDs.
                 std::shared_ptr<storm::dd::DdManager<DdType>> manager;
                 

src/storage/prism/menu_games/VariablePartition.cpp

@@ -7,7 +7,15 @@
 namespace storm {
     namespace prism {
         namespace menu_games {
-            VariablePartition::VariablePartition(std::set<storm::expressions::Variable> const& relevantVariables, std::vector<storm::expressions::Expression> const& expressions) : relevantVariables(relevantVariables), expressionBlocks(expressions.size()) {
+            VariablePartition::VariablePartition(std::set<storm::expressions::Variable> const& relevantVariables, std::vector<storm::expressions::Expression> const& expressions) : relevantVariables(relevantVariables), expressionBlocks(relevantVariables.size()) {
+                // Assign each variable to a new block.
+                uint_fast64_t currentBlock = 0;
+                for (auto const& variable : relevantVariables) {
+                    this->variableToBlockMapping[variable] = currentBlock;
+                    this->variableToExpressionsMapping[variable] = std::set<uint_fast64_t>();
+                }
+                
+                // Add all expressions, which might relate some variables.
                 for (auto const& expression : expressions) {
                     this->addExpression(expression);
                 }

test/functional/abstraction/PrismMenuGameTest.cpp

@@ -24,6 +24,9 @@ TEST(PrismMenuGame, CommandAbstractionTest) {
     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);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction = abstractProgram.getAbstractAdd();
+    abstraction.exportToDot("abstr.dot");
 }
 
 #endif