more work

Former-commit-id: 7182125a9e

src/storage/dd/CuddBdd.cpp

@@ -395,14 +395,18 @@ namespace storm {
         storm::expressions::Variable Bdd<DdType::CUDD>::toExpressionRec(DdNode const* dd, Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<DdNode const*, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const {
             STORM_LOG_ASSERT(dd == Cudd_Regular(dd), "Expected non-negated BDD node.");
             
-            // First, try to look up the current node.
-            auto nodeCounterIt = nodeToCounterMap.find(dd);
-            if (nodeCounterIt != nodeToCounterMap.end()) {
-                // If we have found the node, this means we can look up the counter-index pair and get the corresponding variable.
-                auto variableIt = countIndexToVariablePair.find(std::make_pair(nodeCounterIt->second, dd->index));
-                STORM_LOG_ASSERT(variableIt != countIndexToVariablePair.end(), "Unable to find node.");
-                return variableIt->second;
-            }
+            // First, try to look up the current node if it's not a terminal node. The result of terminal nodes must not
+            // be reused, since we want to be able to incrementally refine the expression later and that requires
+            // different variables for the one-leaf.
+//            if (!Cudd_IsConstant(dd)) {
+                auto nodeCounterIt = nodeToCounterMap.find(dd);
+                if (nodeCounterIt != nodeToCounterMap.end()) {
+                    // If we have found the node, this means we can look up the counter-index pair and get the corresponding variable.
+                    auto variableIt = countIndexToVariablePair.find(std::make_pair(nodeCounterIt->second, dd->index));
+                    STORM_LOG_ASSERT(variableIt != countIndexToVariablePair.end(), "Unable to find node.");
+                    return variableIt->second;
+                }
+//            }
 
             // If the node was not yet encountered, we create a variable and associate it with the appropriate expression.
             storm::expressions::Variable newVariable = manager.declareFreshBooleanVariable();

src/storage/prism/Program.cpp

@@ -360,6 +360,16 @@ namespace storm {
             return this->labels;
         }
         
+        std::vector<storm::expressions::Expression> Program::getAllGuards() const {
+            std::vector<storm::expressions::Expression> allGuards;
+            for (auto const& module : modules) {
+                for (auto const& command : module.getCommands()) {
+                    allGuards.push_back(command.getGuardExpression());
+                }
+            }
+            return allGuards;
+        }
+        
         storm::expressions::Expression const& Program::getLabelExpression(std::string const& label) const {
             auto const& labelIndexPair = labelToIndexMap.find(label);
             STORM_LOG_THROW(labelIndexPair != labelToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve expression for unknown label '" << label << "'.");

src/storage/prism/Program.h

@@ -360,6 +360,13 @@ namespace storm {
              */
             std::vector<Label> const& getLabels() const;
             
+            /*!
+             * Retrieves all guards appearing in the program.
+             *
+             * @return All guards appearing in the program.
+             */
+            std::vector<storm::expressions::Expression> getAllGuards() const;
+            
             /*!
              * Retrieves the expression associated with the given label, if it exists.
              *

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -17,7 +17,7 @@ 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>>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), currentGame(nullptr) {
+            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>>(), initialPredicates), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(), *this->smtSolverFactory), currentGame(nullptr) {
                 
                 // 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.
@@ -25,15 +25,12 @@ namespace storm {
                 
                 uint_fast64_t totalNumberOfCommands = 0;
                 uint_fast64_t maximalUpdateCount = 0;
+                std::vector<storm::expressions::Expression> allGuards;
                 for (auto const& module : program.getModules()) {
                     // If we were requested to add all guards to the set of predicates, we do so now.
                     for (auto const& command : module.getCommands()) {
                         if (addAllGuards) {
                             expressionInformation.predicates.push_back(command.getGuardExpression());
-                        } else {
-                            // If not all guards were added, we also need to populate the bottom state abstractor.
-                            std::cout << "adding " << !command.getGuardExpression() << std::endl;
-                            bottomStateAbstractor.addPredicate(!command.getGuardExpression());
                         }
                         maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(command.getNumberOfUpdates()));
                     }
@@ -42,33 +39,25 @@ namespace storm {
                 }
                 
                 // Create DD variable for the command encoding.
-                ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first;
+                ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1, std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first;
                 
                 // Create DD variable for update encoding.
-                ddInformation.updateDdVariable = ddInformation.manager->addMetaVariable("update", 0, maximalUpdateCount - 1).first;
+                ddInformation.updateDdVariable = ddInformation.manager->addMetaVariable("update", 0, maximalUpdateCount - 1, std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first;
                 
                 // 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) {
-                    storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index)).first;
+                    storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index), std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first;
                     ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getIdentity(newOptionVar).toBdd()));
                 }
                 
-                // Create DD variables for all predicates.
-                for (auto const& predicate : expressionInformation.predicates) {
-                    ddInformation.addPredicate(predicate);
-                }
-                
                 // For each module of the concrete program, we create an abstract counterpart.
                 for (auto const& module : program.getModules()) {
                     modules.emplace_back(module, expressionInformation, ddInformation, *this->smtSolverFactory);
                 }
                 
-                // Add the initial state expression to the initial state abstractor.
-                initialStateAbstractor.addPredicate(program.getInitialConstruct().getInitialStatesExpression());
-                
                 // Finally, retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later.
                 commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd();
                 
@@ -151,10 +140,10 @@ namespace storm {
                 if (addedAllGuards) {
                     bottomStates = ddInformation.manager->getBddZero();
                 } else {
-                    bottomStates = bottomStateAbstractor.getAbstractStates();
+                    // bottomStates = bottomStateAbstractor.getAbstractStates();
                 }
                 
-                std::cout << "found " << (reachableStates && bottomStates).getNonZeroCount() << " reachable bottom states" << std::endl;
+                // std::cout << "found " << (reachableStates && bottomStates).getNonZeroCount() << " reachable bottom states" << std::endl;
                 
                 // Find the deadlock states in the model.
                 storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables);

src/storage/prism/menu_games/AbstractionDdInformation.cpp

@@ -16,8 +16,10 @@ namespace storm {
         namespace menu_games {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager) : manager(manager), allPredicateIdentities(manager->getBddOne()) {
-                // Intentionally left empty.
+            AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager, std::vector<storm::expressions::Expression> const& initialPredicates) : manager(manager), allPredicateIdentities(manager->getBddOne()) {
+                for (auto const& predicate : initialPredicates) {
+                    this->addPredicate(predicate);
+                }
             }
             
             template <storm::dd::DdType DdType, typename ValueType>

src/storage/prism/menu_games/AbstractionDdInformation.h

@@ -32,8 +32,9 @@ namespace storm {
                  * Creates a new DdInformation that uses the given manager.
                  *
                  * @param manager The manager to use.
+                 * @param initialPredicates The initially considered predicates.
                  */
-                AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager);
+                AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager, std::vector<storm::expressions::Expression> const& initialPredicates = std::vector<storm::expressions::Expression>());
                 
                 /*!
                  * Encodes the given distribution index by using the given number of variables from the optionDdVariables

src/storage/prism/menu_games/StateSetAbstractor.cpp

@@ -13,13 +13,23 @@ namespace storm {
         namespace menu_games {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()) {
+            StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraintBdd(ddInformation.manager->getBddOne()) {
                 
                 // Assert all range expressions to enforce legal variable values.
                 for (auto const& rangeExpression : expressionInformation.rangeExpressions) {
                     smtSolver->add(rangeExpression);
                 }
                 
+                // Assert all state predicates.
+                for (auto const& predicate : statePredicates) {
+                    smtSolver->add(predicate);
+                    
+                    // Extract the variables of the predicate, so we know which variables were used when abstracting.
+                    std::set<storm::expressions::Variable> usedVariables = predicate.getVariables();
+                    concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end());
+                    variablePartition.relate(usedVariables);
+                }
+                
                 // 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) {
@@ -28,19 +38,6 @@ namespace storm {
                 this->refine(allPredicateIndices);
             }
             
-            template <storm::dd::DdType DdType, typename ValueType>
-            void StateSetAbstractor<DdType, ValueType>::addPredicate(storm::expressions::Expression const& predicate) {
-                smtSolver->add(predicate);
-                
-                // Extract the variables of the predicate, so we know which variables were used when abstracting.
-                std::set<storm::expressions::Variable> usedVariables = predicate.getVariables();
-                concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end());
-                variablePartition.relate(usedVariables);
-
-                // Remember that we have to recompute the BDD.
-                this->needsRecomputation = true;
-            }
-            
             template <storm::dd::DdType DdType, typename ValueType>
             void StateSetAbstractor<DdType, ValueType>::addMissingPredicates(std::set<uint_fast64_t> const& newRelevantPredicateIndices) {
                 std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newPredicateVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables, newRelevantPredicateIndices);
@@ -55,28 +52,12 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            void StateSetAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& newPredicates) {
+            void StateSetAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& newPredicates, boost::optional<storm::dd::Bdd<DdType>> const& constraintBdd) {
                 // Make the partition aware of the new predicates, which may make more predicates relevant to the abstraction.
                 for (auto const& predicateIndex : newPredicates) {
                     variablePartition.addExpression(expressionInformation.predicates[predicateIndex]);
                 }
-                
-                // Now check whether we need to recompute the cached BDD.
-                std::set<uint_fast64_t> newRelevantPredicateIndices = variablePartition.getRelatedExpressions(concretePredicateVariables);
-                STORM_LOG_TRACE("Found " << newRelevantPredicateIndices.size() << " relevant predicates in abstractor.");
-                
-                // Since the number of relevant predicates is monotonic, we can simply check for the size here.
-                STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates.");
-                bool recomputeDd = newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size();
-                
-                if (recomputeDd) {
-                    // If we need to recompute the BDD, we start by introducing decision variables and the corresponding
-                    // constraints in the SMT problem.
-                    addMissingPredicates(newRelevantPredicateIndices);
-                    
-                    // Finally recompute the cached BDD.
-                    this->recomputeCachedBdd();
-                }
+                this->recomputeCachedBdd();
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -98,6 +79,22 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             void StateSetAbstractor<DdType, ValueType>::recomputeCachedBdd() {
+                // Now check whether we need to recompute the cached BDD.
+                std::set<uint_fast64_t> newRelevantPredicateIndices = variablePartition.getRelatedExpressions(concretePredicateVariables);
+                STORM_LOG_TRACE("Found " << newRelevantPredicateIndices.size() << " relevant predicates in abstractor.");
+                
+                // Since the number of relevant predicates is monotonic, we can simply check for the size here.
+                STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates.");
+                bool recomputeBdd = newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size();
+                
+                if (!recomputeBdd) {
+                    return;
+                }
+
+                // If we need to recompute the BDD, we start by introducing decision variables and the corresponding
+                // constraints in the SMT problem.
+                addMissingPredicates(newRelevantPredicateIndices);
+                
                 STORM_LOG_TRACE("Recomputing BDD for state set abstraction.");
                 
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
@@ -109,9 +106,6 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> StateSetAbstractor<DdType, ValueType>::getAbstractStates() {
-                if (needsRecomputation) {
-                    this->refine();
-                }
                 return cachedBdd;
             }
             

src/storage/prism/menu_games/StateSetAbstractor.h

@@ -3,6 +3,9 @@
 
 #include <memory>
 #include <set>
+#include <boost/optional.hpp>
+
+#include "src/utility/OsDetection.h"
 
 #include "src/storage/dd/DdType.h"
 
@@ -35,27 +38,34 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             class StateSetAbstractor {
             public:
+                // Provide a no-op default constructor.
+                StateSetAbstractor() = default;
+
+                StateSetAbstractor(StateSetAbstractor const& other) = default;
+                StateSetAbstractor& operator=(StateSetAbstractor const& other) = default;
+                
+#ifndef WINDOWS
+                StateSetAbstractor(StateSetAbstractor&& other) = default;
+                StateSetAbstractor& operator=(StateSetAbstractor&& other) = default;
+#endif
+                
                 /*!
                  * Creates a state set abstractor.
                  *
                  * @param expressionInformation The expression-related information including the manager and the predicates.
                  * @param ddInformation The DD-related information including the manager.
+                 * @param statePredicates A set of predicates that have to hold in the concrete states this abstractor is
+                 * supposed to abstract.
                  * @param smtSolverFactory A factory that can create new SMT solvers.
                  */
-                StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
-                
-                /*!
-                 * Adds the given (concrete) predicate to the abstractor and therefore restricts the abstraction to
-                 * abstract states that contain at least some states satisfying the predicate.
-                 */
-                void addPredicate(storm::expressions::Expression const& predicate);
+                StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
                 
                 /*!
                  * Refines the abstractor by making the given predicates new abstract predicates.
                  *
                  * @param newPredicateIndices The indices of the new predicates.
                  */
-                void refine(std::vector<uint_fast64_t> const& newPredicateIndices = std::vector<uint_fast64_t>());
+                void refine(std::vector<uint_fast64_t> const& newPredicateIndices, boost::optional<storm::dd::Bdd<DdType>> const& constraintBdd = boost::none);
                 
                 /*!
                  * Retrieves the set of abstract states matching all predicates added to this abstractor.
@@ -112,6 +122,9 @@ namespace storm {
                 // The cached BDD representing the abstraction. This variable is written to in refinement steps (if work
                 // needed to be done).
                 storm::dd::Bdd<DdType> cachedBdd;
+                
+                // This BDD currently constrains the search for solutions.
+                storm::dd::Bdd<DdType> constraintBdd;
             };
         }
     }

src/storage/prism/menu_games/VariablePartition.cpp

@@ -92,13 +92,14 @@ namespace storm {
                         ++blocksToMergeIt;
                     } else {
                         // Otherwise just move the current block to the new partition.
-                        newVariableBlocks.emplace_back(std::move(variableBlocks[blockIndex]));
-                        newExpressionBlocks.emplace_back(std::move(expressionBlocks[blockIndex]));
-                        
+
                         // Adjust the mapping for all variables of the old block.
                         for (auto const& variable : variableBlocks[blockIndex]) {
-                            variableToBlockMapping[variable] = newVariableBlocks.size() - 1;
+                            variableToBlockMapping[variable] = newVariableBlocks.size();
                         }
+                        
+                        newVariableBlocks.emplace_back(std::move(variableBlocks[blockIndex]));
+                        newExpressionBlocks.emplace_back(std::move(expressionBlocks[blockIndex]));
                     }
                 }
                 

test/functional/abstraction/PrismMenuGameTest.cpp

@@ -295,7 +295,7 @@ TEST(PrismMenuGame, WlanAbstractionTest) {
     
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
     
-    EXPECT_EQ(279, game.getNumberOfTransitions());
+    EXPECT_EQ(281, game.getNumberOfTransitions());
     EXPECT_EQ(4, game.getNumberOfStates());
 }
 
@@ -317,7 +317,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
 
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
 
-    EXPECT_EQ(560, game.getNumberOfTransitions());
+    EXPECT_EQ(564, game.getNumberOfTransitions());
     EXPECT_EQ(8, game.getNumberOfStates());
 }