some fixes to interpolation in game-based abstraction refinement

src/storm/abstraction/MenuGameAbstractor.h

@@ -48,6 +48,9 @@ namespace storm {
             /// Exports a representation of the current abstraction state in the dot format.
             virtual void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const = 0;
 
+            /// Retrieves the number of predicates currently in use.
+            virtual uint64_t getNumberOfPredicates() const = 0;
+            
         protected:
             void exportToDot(storm::abstraction::MenuGame<DdType, ValueType> const& currentGame, std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const;
         };

src/storm/abstraction/MenuGameRefiner.cpp

@@ -390,7 +390,7 @@ namespace storm {
             storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
             storm::dd::Bdd<Type> lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract);
             
-            bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
+            bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero() && !lowerChoice1.isZero() && !lowerChoice2.isZero();
             if (lowerChoicesDifferent) {
                 STORM_LOG_TRACE("Deriving predicate based on lower choice.");
                 predicates = derivePredicatesFromDifferingChoices((pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
@@ -405,7 +405,7 @@ namespace storm {
                 storm::dd::Bdd<Type> upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<Type> upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract);
                 
-                bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero();
+                bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero() && !upperChoice1.isZero() && !upperChoice2.isZero();
                 if (upperChoicesDifferent) {
                     STORM_LOG_TRACE("Deriving predicate based on upper choice.");
                     additionalPredicates = derivePredicatesFromDifferingChoices((pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2);
@@ -476,12 +476,26 @@ namespace storm {
                 
                 // Retrieve the variable updates that the predecessor needs to perform to get to the current state.
                 auto variableUpdates = abstractor.get().getVariableUpdates(std::get<1>(decodedPredecessor), std::get<2>(decodedPredecessor));
-                for (auto const& update : variableUpdates) {
-                    storm::expressions::Variable newVariable = oldToNewVariables.at(update.first);
-                    if (update.second.hasBooleanType()) {
-                        predicates.back().push_back(storm::expressions::iff(lastSubstitution.at(oldToNewVariables.at(update.first)), update.second.changeManager(expressionManager).substitute(substitution)));
+                for (auto const& oldNewVariablePair : oldToNewVariables) {
+                    storm::expressions::Variable const& newVariable = oldNewVariablePair.second;
+
+                    // If the variable was set, use its update expression.
+                    auto updateIt = variableUpdates.find(oldNewVariablePair.first);
+                    if (updateIt != variableUpdates.end()) {
+                        auto const& update = *updateIt;
+
+                        if (update.second.hasBooleanType()) {
+                            predicates.back().push_back(storm::expressions::iff(lastSubstitution.at(newVariable), update.second.changeManager(expressionManager).substitute(substitution)));
+                        } else {
+                            predicates.back().push_back(lastSubstitution.at(newVariable) == update.second.changeManager(expressionManager).substitute(substitution));
+                        }
                     } else {
-                        predicates.back().push_back(lastSubstitution.at(oldToNewVariables.at(update.first)) == update.second.changeManager(expressionManager).substitute(substitution));
+                        // Otherwise, make sure that the new variable maintains the old value.
+                        if (newVariable.hasBooleanType()) {
+                            predicates.back().push_back(storm::expressions::iff(lastSubstitution.at(newVariable), substitution.at(newVariable)));
+                        } else {
+                            predicates.back().push_back(lastSubstitution.at(newVariable) == substitution.at(newVariable));
+                        }
                     }
                 }
                 
@@ -581,6 +595,7 @@ namespace storm {
             
             // Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2
             // state that is also a prob 0 state.
+            auto oldMinPlayer1Strategy = minPlayer1Strategy;
             minPlayer1Strategy = (maxPlayer1Strategy && qualitativeResult.prob0Min.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy);
             
             // Compute all reached pivot states.
@@ -597,7 +612,49 @@ namespace storm {
             
             // Now that we have the pivot state candidates, we need to pick one.
             PivotStateResult<Type, ValueType> pivotStateResult = pickPivotState<Type, ValueType>(pivotSelectionHeuristic, game, pivotStateCandidatesResult, qualitativeResult, boost::none);
-            
+
+//            // SANITY CHECK TO MAKE SURE OUR STRATEGIES ARE NOT BROKEN.
+//            // FIXME.
+//            auto min1ChoiceInPivot = pivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy;
+//            STORM_LOG_ASSERT(!min1ChoiceInPivot.isZero(), "wth?");
+//            bool min1ChoiceInPivotIsProb0Min = !(min1ChoiceInPivot && qualitativeResult.prob0Min.getPlayer2States()).isZero();
+//            bool min1ChoiceInPivotIsProb0Max = !(min1ChoiceInPivot && qualitativeResult.prob0Max.getPlayer2States()).isZero();
+//            bool min1ChoiceInPivotIsProb1Min = !(min1ChoiceInPivot && qualitativeResult.prob1Min.getPlayer2States()).isZero();
+//            bool min1ChoiceInPivotIsProb1Max = !(min1ChoiceInPivot && qualitativeResult.prob1Max.getPlayer2States()).isZero();
+//            std::cout << "after redirection (min)" << std::endl;
+//            std::cout << "min choice is prob0 in min? " << min1ChoiceInPivotIsProb0Min << ", max? " << min1ChoiceInPivotIsProb0Max << std::endl;
+//            std::cout << "min choice is prob1 in min? " << min1ChoiceInPivotIsProb1Min << ", max? " << min1ChoiceInPivotIsProb1Max << std::endl;
+//            std::cout << "min" << std::endl;
+//            for (auto const& e : (min1ChoiceInPivot && minPlayer2Strategy).template toAdd<ValueType>()) {
+//                std::cout << e.first << " -> " << e.second << std::endl;
+//            }
+//            std::cout << "max" << std::endl;
+//            for (auto const& e : (min1ChoiceInPivot && maxPlayer2Strategy).template toAdd<ValueType>()) {
+//                std::cout << e.first << " -> " << e.second << std::endl;
+//            }
+//            bool different = (min1ChoiceInPivot && minPlayer2Strategy) != (min1ChoiceInPivot && maxPlayer2Strategy);
+//            std::cout << "min/max choice of player 2 is different? " << different << std::endl;
+//            bool min1MinPlayer2Choice = !(min1ChoiceInPivot && minPlayer2Strategy).isZero();
+//            bool min1MaxPlayer2Choice = !(min1ChoiceInPivot && maxPlayer2Strategy).isZero();
+//            std::cout << "max/min choice there? " << min1MinPlayer2Choice << std::endl;
+//            std::cout << "max/max choice there? " << min1MaxPlayer2Choice << std::endl;
+//
+//            auto max1ChoiceInPivot = pivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy;
+//            STORM_LOG_ASSERT(!max1ChoiceInPivot.isZero(), "wth?");
+//            bool max1ChoiceInPivotIsProb0Min = !(max1ChoiceInPivot && qualitativeResult.prob0Min.getPlayer2States()).isZero();
+//            bool max1ChoiceInPivotIsProb0Max = !(max1ChoiceInPivot && qualitativeResult.prob0Max.getPlayer2States()).isZero();
+//            bool max1ChoiceInPivotIsProb1Min = !(max1ChoiceInPivot && qualitativeResult.prob1Min.getPlayer2States()).isZero();
+//            bool max1ChoiceInPivotIsProb1Max = !(max1ChoiceInPivot && qualitativeResult.prob1Max.getPlayer2States()).isZero();
+//            std::cout << "after redirection (max)" << std::endl;
+//            std::cout << "max choice is prob0 in min? " << max1ChoiceInPivotIsProb0Min << ", max? " << max1ChoiceInPivotIsProb0Max << std::endl;
+//            std::cout << "max choice is prob1 in min? " << max1ChoiceInPivotIsProb1Min << ", max? " << max1ChoiceInPivotIsProb1Max << std::endl;
+//            different = (max1ChoiceInPivot && minPlayer2Strategy) != (max1ChoiceInPivot && maxPlayer2Strategy);
+//            std::cout << "min/max choice of player 2 is different? " << different << std::endl;
+//            bool max1MinPlayer2Choice = !(max1ChoiceInPivot && minPlayer2Strategy).isZero();
+//            bool max1MaxPlayer2Choice = !(max1ChoiceInPivot && maxPlayer2Strategy).isZero();
+//            std::cout << "max/min choice there? " << max1MinPlayer2Choice << std::endl;
+//            std::cout << "max/max choice there? " << max1MaxPlayer2Choice << std::endl;
+
             boost::optional<RefinementPredicates> predicates;
             if (useInterpolation) {
                 predicates = derivePredicatesFromInterpolation(game, pivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -208,6 +208,11 @@ namespace storm {
                 this->exportToDot(*currentGame, filename, highlightStates, filter);
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            uint64_t JaniMenuGameAbstractor<DdType, ValueType>::getNumberOfPredicates() const {
+                return abstractionInformation.getNumberOfPredicates();
+            }
+            
             // Explicitly instantiate the class.
             template class JaniMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
             template class JaniMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;

src/storm/abstraction/jani/JaniMenuGameAbstractor.h

@@ -109,6 +109,8 @@ namespace storm {
                  */
                 void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const override;
                 
+                virtual uint64_t getNumberOfPredicates() const override;
+                
             protected:
                 using MenuGameAbstractor<DdType, ValueType>::exportToDot;
                 

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -203,6 +203,11 @@ namespace storm {
                 this->exportToDot(*currentGame, filename, highlightStates, filter);
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            uint64_t PrismMenuGameAbstractor<DdType, ValueType>::getNumberOfPredicates() const {
+                return abstractionInformation.getNumberOfPredicates();
+            }
+            
             // Explicitly instantiate the class.
             template class PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
             template class PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -109,6 +109,8 @@ namespace storm {
                  */
                 virtual void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const override;
 
+                virtual uint64_t getNumberOfPredicates() const override;
+                
             protected:
                 using MenuGameAbstractor<DdType, ValueType>::exportToDot;
                 

src/storm/adapters/MathsatExpressionAdapter.h

@@ -116,6 +116,8 @@ namespace storm {
                 msat_term leftResult = boost::any_cast<msat_term>(expression.getFirstOperand()->accept(*this, data));
                 msat_term rightResult = boost::any_cast<msat_term>(expression.getSecondOperand()->accept(*this, data));
 
+                msat_term result = leftResult;
+                int_fast64_t exponent;
 				switch (expression.getOperatorType()) {
 					case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus:
 						return msat_make_plus(env, leftResult, rightResult);
@@ -124,11 +126,21 @@ namespace storm {
 					case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times:
 						return msat_make_times(env, leftResult, rightResult);
 					case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide:
-                        STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unsupported numerical binary operator: '/' (division) in expression.");
+                        return msat_make_divide(env, leftResult, rightResult);
 					case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min:
 						return msat_make_term_ite(env, msat_make_leq(env, leftResult, rightResult), leftResult, rightResult);
 					case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Max:
 						return msat_make_term_ite(env, msat_make_leq(env, leftResult, rightResult), rightResult, leftResult);
+                    case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Power:
+                        exponent = expression.getSecondOperand()->evaluateAsInt();
+                        STORM_LOG_THROW(exponent >= 0, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression with negative exponent.");
+                        --exponent;
+                        if (exponent > 0) {
+                            for (; exponent > 0; --exponent) {
+                                result = msat_make_times(env, result, leftResult);
+                            }
+                        }
+                        return result;
 					default:
                         STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical binary operator '" << static_cast<uint_fast64_t>(expression.getOperatorType()) << "' in expression " << expression << ".");
 				}

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -131,7 +131,7 @@ namespace storm {
             std::unique_ptr<CheckResult> result;
             
             if (checkTask.isBoundSet()) {
-                // Despite having a bound, we create a quanitative result so that the next layer can perform the comparison.
+                // Despite having a bound, we create a quantitative result so that the next layer can perform the comparison.
                 
                 if (player2Direction == storm::OptimizationDirection::Minimize) {
                     if (storm::logic::isLowerBound(checkTask.getBoundComparisonType())) {
@@ -361,7 +361,7 @@ namespace storm {
                 auto abstractionStart = std::chrono::high_resolution_clock::now();
                 storm::abstraction::MenuGame<Type, ValueType> game = abstractor->abstract();
                 auto abstractionEnd = std::chrono::high_resolution_clock::now();
-                STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
+                STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
                 
                 // (2) Prepare transition matrix BDD and target state BDD for later use.
                 storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();

src/storm/settings/modules/AbstractionSettings.cpp

@@ -25,7 +25,7 @@ namespace storm {
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "Sets which abstraction-refinement method to use.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of themethod to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods))
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods))
                                              .setDefaultValueString("bisim").build())
                                 .build());