From 31fa43ab27c71a208777ff66058bd47a30f0c4f9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 21 Mar 2018 16:38:23 +0100 Subject: [PATCH] some fixes to interpolation in game-based abstraction refinement --- src/storm/abstraction/MenuGameAbstractor.h | 3 + src/storm/abstraction/MenuGameRefiner.cpp | 73 +++++++++++++++++-- .../jani/JaniMenuGameAbstractor.cpp | 5 ++ .../abstraction/jani/JaniMenuGameAbstractor.h | 2 + .../prism/PrismMenuGameAbstractor.cpp | 5 ++ .../prism/PrismMenuGameAbstractor.h | 2 + src/storm/adapters/MathsatExpressionAdapter.h | 14 +++- .../abstraction/GameBasedMdpModelChecker.cpp | 4 +- .../settings/modules/AbstractionSettings.cpp | 2 +- 9 files changed, 98 insertions(+), 12 deletions(-) diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index 946fb0a97..e82c1fb31 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/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 const& highlightStatesBdd, storm::dd::Bdd const& filter) const = 0; + /// Retrieves the number of predicates currently in use. + virtual uint64_t getNumberOfPredicates() const = 0; + protected: void exportToDot(storm::abstraction::MenuGame const& currentGame, std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const; }; diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 642cb83fb..e139a357f 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -390,7 +390,7 @@ namespace storm { storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); storm::dd::Bdd 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 upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); storm::dd::Bdd 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 pivotStateResult = pickPivotState(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()) { +// std::cout << e.first << " -> " << e.second << std::endl; +// } +// std::cout << "max" << std::endl; +// for (auto const& e : (min1ChoiceInPivot && maxPlayer2Strategy).template toAdd()) { +// 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 predicates; if (useInterpolation) { predicates = derivePredicatesFromInterpolation(game, pivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index b3c7a755a..a3900ab80 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -208,6 +208,11 @@ namespace storm { this->exportToDot(*currentGame, filename, highlightStates, filter); } + template + uint64_t JaniMenuGameAbstractor::getNumberOfPredicates() const { + return abstractionInformation.getNumberOfPredicates(); + } + // Explicitly instantiate the class. template class JaniMenuGameAbstractor; template class JaniMenuGameAbstractor; diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index 3a478fcb0..0a4cc36ed 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -109,6 +109,8 @@ namespace storm { */ void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override; + virtual uint64_t getNumberOfPredicates() const override; + protected: using MenuGameAbstractor::exportToDot; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 4cb3d46eb..a93e62e67 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -203,6 +203,11 @@ namespace storm { this->exportToDot(*currentGame, filename, highlightStates, filter); } + template + uint64_t PrismMenuGameAbstractor::getNumberOfPredicates() const { + return abstractionInformation.getNumberOfPredicates(); + } + // Explicitly instantiate the class. template class PrismMenuGameAbstractor; template class PrismMenuGameAbstractor; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index 49dc8e9dc..931170df9 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -109,6 +109,8 @@ namespace storm { */ virtual void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override; + virtual uint64_t getNumberOfPredicates() const override; + protected: using MenuGameAbstractor::exportToDot; diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h index 357c482b3..4b4d7cb57 100644 --- a/src/storm/adapters/MathsatExpressionAdapter.h +++ b/src/storm/adapters/MathsatExpressionAdapter.h @@ -116,6 +116,8 @@ namespace storm { msat_term leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); msat_term rightResult = boost::any_cast(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(expression.getOperatorType()) << "' in expression " << expression << "."); } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 36af17be0..6a42b6530 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -131,7 +131,7 @@ namespace storm { std::unique_ptr 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 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(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(abstractionEnd - abstractionStart).count() << "ms)."); // (2) Prepare transition matrix BDD and target state BDD for later use. storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 4835019d4..fd384321f 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -25,7 +25,7 @@ namespace storm { AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { std::vector 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());