bottom states appear to be working, tests not yet adapted

Former-commit-id: 801d99c128

src/abstraction/AbstractionInformation.cpp

@@ -152,6 +152,10 @@ namespace storm {
                 auxVariableBdds.push_back(ddManager->getEncoding(newVariable, 1));
             }
             STORM_LOG_DEBUG("Created " << auxVariableCount << " auxiliary variables.");
+            
+            bottomStateVariables = ddManager->addMetaVariable("bot");
+            bottomStateBdds = std::make_pair(ddManager->getEncoding(bottomStateVariables.first, 1), ddManager->getEncoding(bottomStateVariables.second, 1));
+            extendedPredicateDdVariables.push_back(bottomStateVariables);
         }
         
         template<storm::dd::DdType DdType>
@@ -204,6 +208,11 @@ namespace storm {
             return auxVariables;
         }
         
+        template<storm::dd::DdType DdType>
+        storm::expressions::Variable const& AbstractionInformation<DdType>::getAuxVariable(uint_fast64_t index) const {
+            return auxVariables[index];
+        }
+        
         template<storm::dd::DdType DdType>
         std::set<storm::expressions::Variable> AbstractionInformation<DdType>::getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) const {
             return std::set<storm::expressions::Variable>(auxVariables.begin() + start, auxVariables.begin() + end);
@@ -255,6 +264,37 @@ namespace storm {
             return predicateDdVariables;
         }
         
+        template<storm::dd::DdType DdType>
+        std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& AbstractionInformation<DdType>::getExtendedSourceSuccessorVariablePairs() const {
+            return extendedPredicateDdVariables;
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::expressions::Variable const& AbstractionInformation<DdType>::getBottomStateVariable(bool source) const {
+            if (source) {
+                return bottomStateVariables.first;
+            } else {
+                return bottomStateVariables.second;
+            }
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::getBottomStateBdd(bool source, bool negated) const {
+            if (source) {
+                if (negated) {
+                    return !bottomStateBdds.first;
+                } else {
+                    return bottomStateBdds.first;
+                }
+            } else {
+                if (negated) {
+                    return !bottomStateBdds.second;
+                } else {
+                    return bottomStateBdds.second;
+                }
+            }
+        }
+        
         template<storm::dd::DdType DdType>
         storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::encodePredicateAsSource(uint_fast64_t predicateIndex) const {
             return predicateBdds[predicateIndex].first;

src/abstraction/AbstractionInformation.h

@@ -258,6 +258,14 @@ namespace storm {
              * @return The meta variables associated with auxiliary information.
              */
             std::vector<storm::expressions::Variable> const& getAuxVariables() const;
+            
+            /*!
+             * Retrieves the auxiliary variable with the given index.
+             *
+             * @param index The index of the auxiliary variable to retrieve.
+             * @return The auxiliary variable with the given index.
+             */
+            storm::expressions::Variable const& getAuxVariable(uint_fast64_t index) const;
 
             /*!
              * Retrieves the requested set of auxiliary variables.
@@ -309,6 +317,30 @@ namespace storm {
              * @return The meta variable pairs for all predicates.
              */
             std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& getSourceSuccessorVariablePairs() const;
+
+            /*!
+             * Retrieves the meta variables pairs for all predicates together with the meta variables marking the bottom states.
+             *
+             * @return The meta variable pairs for all predicates and bottom states.
+             */
+            std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& getExtendedSourceSuccessorVariablePairs() const;
+
+            /*!
+             * Retrieves the meta variable marking the bottom states.
+             *
+             * @param source A flag indicating whether the source or successor meta variable is to be returned.
+             * @return The meta variable marking the bottom states.
+             */
+            storm::expressions::Variable const& getBottomStateVariable(bool source) const;
+            
+            /*!
+             * Retrieves the BDD that can be used to mark the bottom states.
+             *
+             * @param source A flag indicating whether the source or successor BDD is to be returned.
+             * @param negated A flag indicating whether the BDD should encode the bottom states or the non-bottom states.
+             * @return The BDD that can be used to mark bottom states.
+             */
+            storm::dd::Bdd<DdType> getBottomStateBdd(bool source, bool negated) const;
             
             /*!
              * Retrieves the BDD for the predicate with the given index over the source variables.
@@ -388,6 +420,9 @@ namespace storm {
             /// The DD variables corresponding to the predicates.
             std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> predicateDdVariables;
             
+            /// The DD variables corresponding to the predicates together with the DD variables marking the bottom states.
+            std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> extendedPredicateDdVariables;
+            
             /// The set of all source variables.
             std::set<storm::expressions::Variable> sourceVariables;
             
@@ -403,6 +438,12 @@ namespace storm {
             /// A BDD that represents the identity of all predicate variables.
             storm::dd::Bdd<DdType> allPredicateIdentities;
             
+            /// A meta variable pair that marks bottom states.
+            std::pair<storm::expressions::Variable, storm::expressions::Variable> bottomStateVariables;
+            
+            /// The BDDs associated with the bottom state variable pair.
+            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> bottomStateBdds;
+            
             /// A mapping from DD variable indices to the predicate index they represent.
             std::unordered_map<uint_fast64_t, uint_fast64_t> ddVariableIndexToPredicateIndexMap;
             

src/abstraction/prism/AbstractCommand.cpp

@@ -90,7 +90,7 @@ namespace storm {
                 }
                 
                 // We now compute how many variables we need to encode the choices. We add one to the maximal number of
-                // choices to
+                // choices to account for a possible transition to a bottom state.
                 uint_fast64_t numberOfVariablesNeeded = static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices + 1)));
                 
                 // Finally, build overall result.
@@ -241,7 +241,7 @@ namespace storm {
                         } else {
                             updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second);
                         }
-                        updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount());
+                        updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
                     }
                     
                     result |= updateBdd;
@@ -280,7 +280,7 @@ namespace storm {
                         }
                     }
                     
-                    result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount());
+                    result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
                 }
                 return result;
             }
@@ -316,13 +316,13 @@ namespace storm {
                 result.states = bottomStateAbstractor.getAbstractStates();
                 
                 // Now equip all these states with an actual transition to a bottom state.
-                result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities();
+                result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities() && this->getAbstractionInformation().getBottomStateBdd(false, false);
                 
-                // Add the command encoding and the next free player 2 encoding.
-                result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, cachedDd.numberOfPlayer2Variables);
+                // Mark the states as bottom states.
+                result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false);
                 
-                result.states.template toAdd<ValueType>().exportToDot("bottom_" + std::to_string(command.get().getGlobalIndex()) + ".dot");
-                result.transitions.template toAdd<ValueType>().exportToDot("bottom_trans_" + std::to_string(command.get().getGlobalIndex()) + ".dot");
+                // Add the command encoding and the next free player 2 encoding.
+                result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, cachedDd.numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount());
                 
                 return result;
             }
@@ -331,7 +331,7 @@ namespace storm {
             storm::dd::Add<DdType, ValueType> AbstractCommand<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
                 storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
                 for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
-                    result += this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression()));
+                    result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression()));
                 }
                 result *= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd<ValueType>();
                 return result;

src/abstraction/prism/AbstractModule.cpp

@@ -45,7 +45,7 @@ namespace storm {
                 // DDs use the same amount DD variable encoding the choices of player 2.
                 storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
                 for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) {
-                    result |= commandDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(maximalNumberOfUsedOptionVariables, commandDd.numberOfPlayer2Variables);
+                    result |= commandDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(commandDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables);
                 }
                 return GameBddResult<DdType>(result, maximalNumberOfUsedOptionVariables, nextFreePlayer2Index);
             }

src/abstraction/prism/AbstractProgram.cpp

@@ -56,7 +56,7 @@ namespace storm {
                 // NOTE: currently we assume that 100 player 2 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.
-                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))) + 1);
+                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
                 
                 // Now that we have created all other DD variables, we create the DD variables for the predicates.
                 std::vector<uint_fast64_t> allPredicateIndices;
@@ -129,12 +129,8 @@ namespace storm {
                 std::set<storm::expressions::Variable> variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount()));
                 auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables);
                 variablesToAbstract.insert(player2Variables.begin(), player2Variables.end());
-                auto auxVariables = abstractionInformation.getAuxVariableSet(1, abstractionInformation.getAuxVariableCount());
+                auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount());
                 variablesToAbstract.insert(auxVariables.begin(), auxVariables.end());
-                std::cout << "vars" << std::endl;
-                for (auto const& var : auxVariables) {
-                    std::cout << var.getName() << std::endl;
-                }
                 
                 // Do a reachability analysis on the raw transition relation.
                 storm::dd::Bdd<DdType> transitionRelation = game.bdd.existsAbstract(variablesToAbstract);
@@ -154,20 +150,38 @@ namespace storm {
 
                 // Compute bottom states and the appropriate transitions if necessary.
                 BottomStateResult<DdType> bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero());
+                bool hasBottomStates = false;
                 if (!addedAllGuards) {
                     bottomStateResult = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables);
+                    hasBottomStates = !bottomStateResult.states.isZero();
                 }
                 
                 // Construct the transition matrix by cutting away the transitions of unreachable states.
-                storm::dd::Add<DdType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>() * commandUpdateProbabilitiesAdd + deadlockTransitions;// + bottomStateResult.transitions.template toAdd<ValueType>();
-                transitionMatrix.exportToDot("trans_upd.dot");
+                storm::dd::Add<DdType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>() * commandUpdateProbabilitiesAdd + deadlockTransitions;
+                
+                // If there are bottom states, we need to mark all other states as non-bottom now.
+                if (hasBottomStates) {
+                    transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd<ValueType>();
+                    transitionMatrix += bottomStateResult.transitions.template toAdd<ValueType>();
+                    reachableStates &= abstractionInformation.getBottomStateBdd(true, true);
+                    reachableStates |= bottomStateResult.states;
+                }
             
                 std::set<storm::expressions::Variable> usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables);
                 
                 std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
                 allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end());
 
-                return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap());
+                std::set<storm::expressions::Variable> allSourceVariables(abstractionInformation.getSourceVariables());
+                if (hasBottomStates) {
+                    allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true));
+                }
+                std::set<storm::expressions::Variable> allSuccessorVariables(abstractionInformation.getSuccessorVariables());
+                if (hasBottomStates) {
+                    allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false));
+                }
+                
+                return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, hasBottomStates ? abstractionInformation.getExtendedSourceSuccessorVariablePairs() : abstractionInformation.getSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap());
             }
             
             template <storm::dd::DdType DdType, typename ValueType>