abstraction loop working for purely qualitative refinement

Former-commit-id: ce28ed97c2

src/abstraction/AbstractionInformation.cpp

@@ -54,6 +54,7 @@ namespace storm {
             allPredicateIdentities &= predicateIdentities.back();
             sourceVariables.insert(newMetaVariable.first);
             successorVariables.insert(newMetaVariable.second);
+            orderedSuccessorVariables.push_back(newMetaVariable.second);
             ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex;
             return predicateIndex;
         }
@@ -249,6 +250,11 @@ namespace storm {
             return successorVariables;
         }
         
+        template<storm::dd::DdType DdType>
+        std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getOrderedSuccessorVariables() const {
+            return orderedSuccessorVariables;
+        }
+        
         template<storm::dd::DdType DdType>
         storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::getAllPredicateIdentities() const {
             return allPredicateIdentities;

src/abstraction/AbstractionInformation.h

@@ -332,6 +332,13 @@ namespace storm {
              */
             std::set<storm::expressions::Variable> const& getSuccessorVariables() const;
 
+            /*!
+             * Retrieves the ordered collection of successor meta variables.
+             *
+             * @return All successor meta variables.
+             */
+            std::vector<storm::expressions::Variable> const& getOrderedSuccessorVariables() const;
+            
             /*!
              * Retrieves a BDD representing the identities of all predicates.
              *
@@ -472,9 +479,12 @@ namespace storm {
             /// The set of all source variables.
             std::set<storm::expressions::Variable> sourceVariables;
             
-            /// The set of all source variables.
+            /// The set of all successor variables.
             std::set<storm::expressions::Variable> successorVariables;
             
+            /// An ordered collection of the successor variables.
+            std::vector<storm::expressions::Variable> orderedSuccessorVariables;
+            
             /// The BDDs corresponding to the predicates.
             std::vector<std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>>> predicateBdds;
             

src/abstraction/prism/AbstractProgram.cpp

@@ -2,6 +2,8 @@
 
 #include "src/abstraction/BottomStateResult.h"
 
+#include "src/storage/BitVector.h"
+
 #include "src/storage/prism/Program.h"
 
 #include "src/storage/dd/DdManager.h"
@@ -110,30 +112,80 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            void AbstractProgram<DdType, ValueType>::refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) {
-//                std::cout << "refining in program!" << std::endl;
-//                lowerChoice.template toAdd<ValueType>().exportToDot("lchoice.dot");
-//                upperChoice.template toAdd<ValueType>().exportToDot("uchoice.dot");
-//                player1Choice.template toAdd<ValueType>().exportToDot("pl1_choice.dot");
-//                pivotState.template toAdd<ValueType>().exportToDot("pivotstate.dot");
+            std::map<uint_fast64_t, storm::storage::BitVector> AbstractProgram<DdType, ValueType>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const {
+                std::map<uint_fast64_t, storm::storage::BitVector> result;
+                
+                storm::dd::Add<DdType, ValueType> lowerChoiceAsAdd = choice.template toAdd<ValueType>();
+                for (auto const& successorValuePair : lowerChoiceAsAdd) {
+                    uint_fast64_t updateIndex = abstractionInformation.decodeAux(successorValuePair.first, 0, currentGame->getProbabilisticBranchingVariables().size());
+                    
+                    storm::storage::BitVector successor(abstractionInformation.getNumberOfPredicates());
+                    for (uint_fast64_t index = 0; index < abstractionInformation.getOrderedSuccessorVariables().size(); ++index) {
+                        auto const& successorVariable = abstractionInformation.getOrderedSuccessorVariables()[index];
+                        if (successorValuePair.first.getBooleanValue(successorVariable)) {
+                            successor.set(index);
+                        }
+                    }
                     
+                    result[updateIndex] = successor;
+                }
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AbstractProgram<DdType, ValueType>::refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) {
                 // Decode the index of the command chosen by player 1.
                 storm::dd::Add<DdType, ValueType> player1ChoiceAsAdd = player1Choice.template toAdd<ValueType>();
                 auto pl1It = player1ChoiceAsAdd.begin();
                 uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount());
-                
-                bool bottomSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero();
-                if (bottomSuccessor) {
                 storm::abstraction::prism::AbstractCommand<DdType, ValueType>& abstractCommand = modules.front().getCommands()[commandIndex];
+                storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand();
+
+                // Check whether there are bottom states in the game and whether one of the choices actually picks the
+                // bottom state as the successor.
+                bool buttomStateSuccessor = false;
+                if (!currentGame->getBottomStates().isZero()) {
+                    buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero();
+                }
+                
+                // If one of the choices picks the bottom state, the new predicate is based on the guard of the appropriate
+                // command (that is the player 1 choice).
+                if (buttomStateSuccessor) {
+                    STORM_LOG_DEBUG("One of the successors is a bottom state, taking a guard as a new predicate.");
                     abstractCommand.notifyGuardIsPredicate();
-                    storm::expressions::Expression newPredicate = abstractCommand.getConcreteCommand().getGuardExpression();
+                    storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression();
                     STORM_LOG_DEBUG("Derived new predicate: " << newPredicate);
                     this->refine({newPredicate});
                 } else {
-                    exit(-1);
+                    STORM_LOG_DEBUG("No bottom state successor. Deriving a new predicate using weakest precondition.");
+                    
+                    // Decode both choices to explicit mappings.
+                    std::map<uint_fast64_t, storm::storage::BitVector> lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice);
+                    std::map<uint_fast64_t, storm::storage::BitVector> upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice);
+                    STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode.");
+
+                    // Now go through the mappings and find points of deviation. Currently, we take the first deviation.
+                    storm::expressions::Expression newPredicate;
+                    auto lowerIt = lowerChoiceUpdateToSuccessorMapping.begin();
+                    auto lowerIte = lowerChoiceUpdateToSuccessorMapping.end();
+                    auto upperIt = upperChoiceUpdateToSuccessorMapping.begin();
+                    for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) {
+                        STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch.");
+                        uint_fast64_t updateIndex = lowerIt->first;
+                        bool deviates = lowerIt->second != upperIt->second;
+                        if (deviates) {
+                            for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) {
+                                if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) {
+                                    // Now we know the point of the deviation (command, update, predicate).
+                                    newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap());
+                                    break;
+                                }
+                            }
+                        }
                     }
                     
-                storm::dd::Add<DdType, ValueType> lowerChoiceAsAdd = lowerChoice.template toAdd<ValueType>();
+                    this->refine({newPredicate});
+                }
             }
             
             template <storm::dd::DdType DdType, typename ValueType>

src/abstraction/prism/AbstractProgram.h

@@ -100,6 +100,14 @@ namespace storm {
                  */
                 std::unique_ptr<MenuGame<DdType, ValueType>> buildGame();
                 
+                /*!
+                 * Decodes the given choice over the auxiliary and successor variables to a mapping from update indices
+                 * to bit vectors representing the successors under these updates.
+                 *
+                 * @param choice The choice to decode.
+                 */
+                std::map<uint_fast64_t, storm::storage::BitVector> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const;
+                
                 // The concrete program this abstract program refers to.
                 std::reference_wrapper<storm::prism::Program const> program;
 

src/exceptions/InvalidModelException.h

@@ -0,0 +1,13 @@
+#pragma once
+
+#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
+
+namespace storm {
+    namespace exceptions {
+        
+        STORM_NEW_EXCEPTION(InvalidModelException)
+        
+    } // namespace exceptions
+} // namespace storm
+

src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -1,7 +1,7 @@
 #include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
 
-#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
-#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 
 #include "src/models/symbolic/StandardRewardModel.h"
 
@@ -18,6 +18,7 @@
 
 #include "src/exceptions/NotSupportedException.h"
 #include "src/exceptions/InvalidPropertyException.h"
+#include "src/exceptions/InvalidModelException.h"
 
 #include "src/modelchecker/results/CheckResult.h"
 
@@ -57,7 +58,7 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
             storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
-            return performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula>(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula()));
+            return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula()));
         }
         
         template<storm::dd::DdType Type, typename ValueType>
@@ -85,12 +86,7 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> getResultAfterQualitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::dd::DdManager<Type> const& ddManager, storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& initialStates, bool prob0) {
-            if (checkTask.isBoundSet()) {
-                bool result = getResultConsideringBound(prob0 ? storm::utility::zero<ValueType>() : storm::utility::one<ValueType>(), checkTask.getBound());
-                return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<Type>>(reachableStates, initialStates, result ? initialStates : ddManager.getBddZero());
-            } else {
-                return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<Type>>(reachableStates, initialStates, prob0 ? ddManager.template getAddZero<ValueType>() : initialStates.template toAdd<ValueType>());
-            }
+            return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), prob0 ? storm::utility::zero<ValueType>() : storm::utility::one<ValueType>());
         }
         
         template<storm::dd::DdType Type>
@@ -143,17 +139,17 @@ namespace storm {
             bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
             if (lowerChoicesDifferent) {
                 abstractor.refine(pivotState, (pivotState && prob01.min.first.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
-            }
-            
+            } else {
                 storm::dd::Bdd<Type> upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.max.second.getPlayer1Strategy();
                 storm::dd::Bdd<Type> upperChoice1 = (upperChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<Type> upperChoice2 = (upperChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
-            upperChoice1.template toAdd<ValueType>().exportToDot("uchoice1.dot");
-            upperChoice2.template toAdd<ValueType>().exportToDot("uchoice2.dot");
                 
                 bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero();
                 if (upperChoicesDifferent) {
                     abstractor.refine(pivotState, (pivotState && prob01.max.second.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2);
+                } else {
+                    STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates.");
+                }
             }
         }
         
@@ -171,13 +167,26 @@ namespace storm {
             }
             
             // Derive the optimization direction for player 1 (assuming menu-game abstraction).
-            storm::OptimizationDirection player1Direction = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize;
+            storm::OptimizationDirection player1Direction;
+            if (checkTask.isOptimizationDirectionSet()) {
+                player1Direction = checkTask.getOptimizationDirection();
+            } else if (checkTask.isBoundSet() && !originalProgram.isDeterministicModel()) {
+                player1Direction = storm::logic::isLowerBound(checkTask.getBoundComparisonType()) ? storm::OptimizationDirection::Minimize : storm::OptimizationDirection::Maximize;
+            } else {
+                STORM_LOG_THROW(originalProgram.isDeterministicModel(), storm::exceptions::InvalidPropertyException, "Requiring either min or max annotation in property for nondeterministic models.");
+                player1Direction = storm::OptimizationDirection::Maximize;
+            }
             
             storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedProgram, initialPredicates, smtSolverFactory);
             
+            for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) {
+                STORM_LOG_TRACE("Starting iteration " << iterations);
+                abstractor.exportToDot("game" + std::to_string(iterations) + ".dot");
+
                 // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
                 storm::abstraction::MenuGame<Type, ValueType> game = abstractor.abstract();
-            STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions.");
+                STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions.");
+                STORM_LOG_THROW(game.getInitialStates().getNonZeroCount(), storm::exceptions::InvalidModelException, "Cannot treat models with more than one (abstract) initial state.");
                 
                 // 1.5 build a BDD from the transition matrix for various later uses.
                 storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
@@ -193,34 +202,32 @@ namespace storm {
                 storm::dd::Bdd<Type> initialMaybeStates = game.getInitialStates() && (maybeMin || maybeMax);
                 if (initialMaybeStates.isZero()) {
                     // In this case, we know the result for the initial states for both player 2 minimizing and maximizing.
+                    STORM_LOG_TRACE("No initial state is a 'maybe' state. Refining abstraction based on qualitative check.");
                     
                     // If the result is 0 independent of the player 2 strategy, then we know the final result and can return it.
                     storm::dd::Bdd<Type> tmp = game.getInitialStates() && prob01.min.first.states && prob01.max.first.states;
                     if (tmp == game.getInitialStates()) {
-                    getResultAfterQualitativeCheck<Type, ValueType>(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), true);
+                        return getResultAfterQualitativeCheck<Type, ValueType>(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), true);
                     }
                     
                     // If the result is 1 independent of the player 2 strategy, then we know the final result and can return it.
                     tmp = game.getInitialStates() && prob01.min.second.states && prob01.max.second.states;
                     if (tmp == game.getInitialStates()) {
-                    getResultAfterQualitativeCheck<Type, ValueType>(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), false);
+                        return getResultAfterQualitativeCheck<Type, ValueType>(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), false);
                     }
                     
                     // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1)
                     // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine.
                     refineAfterQualitativeCheck(abstractor, game, prob01, transitionMatrixBdd);
-            }
-            
-            
-            
-//            std::unique_ptr<storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType>> gameSolverFactory = std::make_unique<storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType>>();
-//            gameSolverFactory->create(game.getTransitionMatrix(), game.getReachableStates());
-//            storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables
+                } else {
                     
-            // 3. if the bounds suffice to complete checkTask, return result now.
+                    // Do not numerically solve the game if there is a qualitative bound around.
                     
-            // 4. if the bounds do not suffice
+                    STORM_LOG_ASSERT(false, "Quantiative refinement not yet there. :)");
+                }
+            }
 
+            STORM_LOG_ASSERT(false, "This point must not be reached.");
             return nullptr;
         }
         
@@ -247,20 +254,22 @@ namespace storm {
             STORM_LOG_ASSERT(prob1Max.hasPlayer1Strategy(), "Unable to proceed without strategy.");
             STORM_LOG_ASSERT(prob1Max.hasPlayer2Strategy(), "Unable to proceed without strategy.");
 
-            STORM_LOG_DEBUG("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states.");
-            STORM_LOG_DEBUG("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states.");
+            STORM_LOG_TRACE("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states.");
+            STORM_LOG_TRACE("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states.");
             
             return detail::GameProb01Result<Type>(prob0Min, prob1Min, prob0Max, prob1Max);
         }
         
         template<storm::dd::DdType Type, typename ValueType>
         storm::expressions::Expression GameBasedMdpModelChecker<Type, ValueType>::getExpression(storm::logic::Formula const& formula) {
-            STORM_LOG_THROW(formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression.");
+            STORM_LOG_THROW(formula.isBooleanLiteralFormula() || formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression.");
             storm::expressions::Expression result;
             if (formula.isAtomicLabelFormula()) {
                 result = preprocessedProgram.getLabelExpression(formula.asAtomicLabelFormula().getLabel());
-            } else {
+            } else if (formula.isAtomicExpressionFormula()) {
                 result = formula.asAtomicExpressionFormula().getExpression();
+            } else {
+                result = formula.asBooleanLiteralFormula().isTrueFormula() ? originalProgram.getManager().boolean(true) : originalProgram.getManager().boolean(false);
             }
             return result;
         }