From bde84d00730336759bddea237d13a2f0cfafdfe2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 24 Aug 2016 16:40:03 +0200 Subject: [PATCH] fixed symbolic game solver wrt. illegal masks. numerical solving step in game-based model checker working, but no refinement yet. Former-commit-id: 6189a1e5383114123d41d165eadaa0cee5a5e106 --- .../3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc | 11 +- .../3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh | 1 + resources/3rdparty/cudd-3.0.0/cudd/cudd.h | 2 + .../3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c | 130 +++++++++++++++++ .../3rdparty/cudd-3.0.0/cudd/cuddAddApply.c | 47 ++++++ resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h | 1 + src/abstraction/prism/AbstractProgram.cpp | 13 +- .../abstraction/GameBasedMdpModelChecker.cpp | 135 +++++++++++++++++- src/solver/SymbolicGameSolver.cpp | 22 +-- src/solver/SymbolicGameSolver.h | 14 +- src/storage/dd/Add.cpp | 6 + src/storage/dd/Add.h | 9 +- src/storage/dd/cudd/InternalCuddAdd.cpp | 5 + src/storage/dd/cudd/InternalCuddAdd.h | 9 +- src/storage/dd/sylvan/InternalSylvanAdd.cpp | 14 +- src/storage/dd/sylvan/InternalSylvanAdd.h | 9 +- src/utility/graph.cpp | 2 +- src/utility/solver.cpp | 4 +- src/utility/solver.h | 2 +- .../solver/FullySymbolicGameSolverTest.cpp | 18 ++- 20 files changed, 424 insertions(+), 30 deletions(-) diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc index d1adb4bbc..222b58f25 100644 --- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc +++ b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc @@ -2648,7 +2648,16 @@ ADD::MinAbstract(const ADD& cube) const checkReturnValue(result); return ADD(p, result); } // ADD::MinAbstract - + +ADD +ADD::MinAbstractExcept0(const ADD& cube) const +{ + DdManager *mgr = checkSameManager(cube); + DdNode *result = Cudd_addMinExcept0Abstract(mgr, node, cube.node); + checkReturnValue(result); + return ADD(p, result); +} // ADD::MinAbstractExcept0 + ADD ADD::MaxAbstract(const ADD& cube) const { diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh index a4ea48a41..b672e2965 100644 --- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh +++ b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh @@ -334,6 +334,7 @@ public: ADD UnivAbstract(const ADD& cube) const; ADD OrAbstract(const ADD& cube) const; ADD MinAbstract(const ADD& cube) const; + ADD MinAbstractExcept0(const ADD& cube) const; ADD MaxAbstract(const ADD& cube) const; ADD MinAbstractRepresentative(const ADD& cube) const; ADD MaxAbstractRepresentative(const ADD& cube) const; diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h index d0abcb7f0..20acf5854 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h +++ b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h @@ -667,6 +667,7 @@ extern DdNode * Cudd_addExistAbstract(DdManager *manager, DdNode *f, DdNode *cub extern DdNode * Cudd_addUnivAbstract(DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * Cudd_addOrAbstract(DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * Cudd_addMinAbstract(DdManager * manager, DdNode * f, DdNode * cube); +extern DdNode * Cudd_addMinExcept0Abstract(DdManager * manager, DdNode * f, DdNode * cube); extern DdNode * Cudd_addMaxAbstract(DdManager * manager, DdNode * f, DdNode * cube); extern DdNode * Cudd_addMinAbstractRepresentative(DdManager * manager, DdNode * f, DdNode * cube); extern DdNode * Cudd_addMaxAbstractRepresentative(DdManager * manager, DdNode * f, DdNode * cube); @@ -679,6 +680,7 @@ extern DdNode * Cudd_addSetNZ(DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addDivide(DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addMinus(DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addMinimum(DdManager *dd, DdNode **f, DdNode **g); +extern DdNode * Cudd_addMinimumExcept0(DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addMaximum(DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addOneZeroMaximum(DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addDiff(DdManager *dd, DdNode **f, DdNode **g); diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c index b9d914cfa..57c23d189 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c @@ -243,6 +243,44 @@ Cudd_addMinAbstract( } /* end of Cudd_addMinAbstract */ +/**Function******************************************************************** + + Synopsis [Abstracts all the variables in cube from the + ADD f by taking the minimum.] + + Description [Abstracts all the variables in cube from the ADD f + by taking the minimum over all possible values taken by the + variables. Returns the abstracted ADD if successful; NULL + otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_addUnivAbstract Cudd_addExistAbstract] + + Note: Added by Christian Dehnert 24/08/2016 + + ******************************************************************************/ +DdNode * +Cudd_addMinExcept0Abstract( + DdManager * manager, + DdNode * f, + DdNode * cube) +{ + DdNode *res; + + if (addCheckPositiveCube(manager, cube) == 0) { + (void) fprintf(manager->err,"Error: Can only abstract cubes"); + return(NULL); + } + + do { + manager->reordered = 0; + res = cuddAddMinExcept0AbstractRecur(manager, f, cube); + } while (manager->reordered == 1); + return(res); + +} /* end of Cudd_addMinExcept0Abstract */ + /**Function******************************************************************** Synopsis [Abstracts all the variables in cube from the @@ -750,6 +788,98 @@ cuddAddMinAbstractRecur( } /* end of cuddAddMinAbstractRecur */ +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_addMinAbstract.] + + Description [Performs the recursive step of Cudd_addMinAbstract. + Returns the ADD obtained by abstracting the variables of cube from f, + if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [] + + added 24/08/2016 by Christian Dehnert + + ******************************************************************************/ +DdNode * +cuddAddMinExcept0AbstractRecur( + DdManager * manager, + DdNode * f, + DdNode * cube) +{ + DdNode *T, *E, *res, *res1, *res2, *zero; + + zero = DD_ZERO(manager); + + /* Cube is guaranteed to be a cube at this point. */ + if (f == zero || cuddIsConstant(cube)) { + return(f); + } + + /* Abstract a variable that does not appear in f. */ + if (cuddI(manager,f->index) > cuddI(manager,cube->index)) { + res = cuddAddMinAbstractRecur(manager, f, cuddT(cube)); + return(res); + } + + if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstract, f, cube)) != NULL) { + return(res); + } + + + T = cuddT(f); + E = cuddE(f); + + /* If the two indices are the same, so are their levels. */ + if (f->index == cube->index) { + res1 = cuddAddMinAbstractRecur(manager, T, cuddT(cube)); + if (res1 == NULL) return(NULL); + cuddRef(res1); + res2 = cuddAddMinAbstractRecur(manager, E, cuddT(cube)); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } + cuddRef(res2); + res = cuddAddApplyRecur(manager, Cudd_addMinimumExcept0, res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + return(NULL); + } + cuddRef(res); + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + cuddCacheInsert2(manager, Cudd_addMinAbstract, f, cube, res); + cuddDeref(res); + return(res); + } + else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ + res1 = cuddAddMinAbstractRecur(manager, T, cube); + if (res1 == NULL) return(NULL); + cuddRef(res1); + res2 = cuddAddMinAbstractRecur(manager, E, cube); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } + cuddRef(res2); + res = (res1 == res2) ? res1 : + cuddUniqueInter(manager, (int) f->index, res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + return(NULL); + } + cuddDeref(res1); + cuddDeref(res2); + cuddCacheInsert2(manager, Cudd_addMinAbstract, f, cube, res); + return(res); + } + +} /* end of cuddAddMinAbstractRecur */ /**Function******************************************************************** diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c index b8716657c..01fc45fe6 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c @@ -406,6 +406,53 @@ Cudd_addMinimum( } /* end of Cudd_addMinimum */ +/** + @brief Integer and floating point min. + + @details Integer and floating point min for Cudd_addApply. + + @return NULL if not a terminal case; min(f,g) otherwise. + + @sideeffect None + + @see Cudd_addApply + + added 24/08/2016 + + */ +DdNode * +Cudd_addMinimumExcept0( + DdManager * dd, + DdNode ** f, + DdNode ** g) +{ + DdNode *F, *G; + + F = *f; G = *g; + if (F == DD_ZERO(dd)) return(G); + if (G == DD_ZERO(dd)) return(F); + if (F == DD_PLUS_INFINITY(dd)) return(G); + if (G == DD_PLUS_INFINITY(dd)) return(F); + if (F == G) return(F); +#if 0 + /* These special cases probably do not pay off. */ + if (F == DD_MINUS_INFINITY(dd)) return(F); + if (G == DD_MINUS_INFINITY(dd)) return(G); +#endif + if (cuddIsConstant(F) && cuddIsConstant(G)) { + if (cuddV(F) <= cuddV(G)) { + return(F); + } else { + return(G); + } + } + if (F > G) { /* swap f and g */ + *f = G; + *g = F; + } + return(NULL); + +} /* end of Cudd_addMinimumExcept0 */ /** @brief Integer and floating point max. diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h b/resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h index 4ba5fef03..f5af25cd2 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h @@ -1062,6 +1062,7 @@ extern DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode extern DdNode * cuddAddUnivAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * cuddAddOrAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * cuddAddMinAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube); +extern DdNode * cuddAddMinExcept0AbstractRecur (DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * cuddAddMaxAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * cuddAddMinAbstractRepresentativeRecur(DdManager * manager, DdNode * f, DdNode * cube); extern DdNode * cuddAddMaxAbstractRepresentativeRecur(DdManager * manager, DdNode * f, DdNode * cube); diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index c68269870..a175b62ad 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -154,13 +154,13 @@ namespace storm { // 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."); + STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate."); abstractCommand.notifyGuardIsPredicate(); storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression(); - STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); + STORM_LOG_TRACE("Derived new predicate: " << newPredicate); this->refine({newPredicate}); } else { - STORM_LOG_DEBUG("No bottom state successor. Deriving a new predicate using weakest precondition."); + STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); // Decode both choices to explicit mappings. std::map lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice); @@ -187,8 +187,15 @@ namespace storm { } } + STORM_LOG_TRACE("Derived new predicate: " << newPredicate); + this->refine({newPredicate}); } + + STORM_LOG_TRACE("Current set of predicates:"); + for (auto const& predicate : abstractionInformation.getPredicates()) { + STORM_LOG_TRACE(predicate); + } } template diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 86c0072eb..890614ccb 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -13,6 +13,9 @@ #include "src/logic/FragmentSpecification.h" +#include "src/solver/SymbolicGameSolver.h" + +#include "src/utility/solver.h" #include "src/utility/dd.h" #include "src/utility/macros.h" @@ -115,6 +118,55 @@ namespace storm { return result; } + + template + std::unique_ptr checkForResultAfterQuantitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection const& player2Direction, ValueType const& value) { + std::unique_ptr result; + + // If the minimum value exceeds an upper threshold or the maximum value is below a lower threshold, we can + // return the value because the property will definitely hold. Vice versa, if the minimum value exceeds an + // upper bound or the maximum value is below a lower bound, the property will definitely not hold and we can + // return the value. + if (checkTask.isBoundSet() && storm::logic::isLowerBound(checkTask.getBoundComparisonType())) { + if (player2Direction == storm::OptimizationDirection::Minimize) { + if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value > checkTask.getBoundThreshold()) + || (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value >= checkTask.getBoundThreshold())) { + result = std::make_unique>(storm::storage::sparse::state_type(0), value); + } + } else { + if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value <= checkTask.getBoundThreshold()) + || (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value < checkTask.getBoundThreshold())) { + result = std::make_unique>(storm::storage::sparse::state_type(0), value); + } + } + } else if (checkTask.isBoundSet() && !storm::logic::isLowerBound(checkTask.getBoundComparisonType())) { + if (player2Direction == storm::OptimizationDirection::Maximize) { + if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value < checkTask.getBoundThreshold()) || + (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value <= checkTask.getBoundThreshold())) { + result = std::make_unique>(storm::storage::sparse::state_type(0), value); + } + } else { + if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value >= checkTask.getBoundThreshold()) || + (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value > checkTask.getBoundThreshold())) { + result = std::make_unique>(storm::storage::sparse::state_type(0), value); + } + } + } + + return result; + } + + template + std::unique_ptr checkForResultAfterQuantitativeCheck(CheckTask const& checkTask, ValueType const& minValue, ValueType const& maxValue) { + std::unique_ptr result; + + // If the lower and upper bounds are close enough, we can return the result. + if (maxValue - minValue < storm::utility::convertNumber(1e-3)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), (minValue + maxValue) / ValueType(2)); + } + + return result; + } template storm::dd::Bdd pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates) { @@ -180,6 +232,30 @@ namespace storm { } } + template + storm::dd::Add solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& prob1States, boost::optional> startVector = boost::none) { + + // Compute the ingredients of the equation system. + storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); + storm::dd::Add submatrix = maybeStatesAdd * game.getTransitionMatrix(); + storm::dd::Add prob1StatesAsColumn = prob1States.template toAdd().swapVariables(game.getRowColumnMetaVariablePairs()); + storm::dd::Add subvector = submatrix * prob1StatesAsColumn; + subvector = subvector.sumAbstract(game.getColumnVariables()); + + // Cut away all columns targeting non-maybe states. + submatrix *= maybeStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs()); + + // Cut the starting vector to the maybe states of this query. + if (startVector) { + startVector.get() *= maybeStatesAdd; + } + + // Create the solver and solve the equation system. + storm::utility::solver::SymbolicGameSolverFactory solverFactory; + std::unique_ptr> solver = solverFactory.create(submatrix, maybeStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables()); + return solver->solveGame(player1Direction, player2Direction, startVector ? startVector.get() : game.getManager().template getAddZero(), subvector); + } + template std::unique_ptr GameBasedMdpModelChecker::performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); @@ -195,7 +271,9 @@ namespace storm { // Derive the optimization direction for player 1 (assuming menu-game abstraction). storm::OptimizationDirection player1Direction; - if (checkTask.isOptimizationDirectionSet()) { + if (originalProgram.isDeterministicModel()) { + player1Direction = storm::OptimizationDirection::Maximize; + } else if (checkTask.isOptimizationDirectionSet()) { player1Direction = checkTask.getOptimizationDirection(); } else if (checkTask.isBoundSet() && !originalProgram.isDeterministicModel()) { player1Direction = storm::logic::isLowerBound(checkTask.getBoundComparisonType()) ? storm::OptimizationDirection::Minimize : storm::OptimizationDirection::Maximize; @@ -239,8 +317,13 @@ namespace storm { storm::dd::Bdd maybeMin = !(prob01.min.first.states || prob01.min.second.states) && game.getReachableStates(); storm::dd::Bdd maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates(); + maybeMin.template toAdd().exportToDot("maybemin.dot"); + maybeMax.template toAdd().exportToDot("maybemax.dot"); + game.getInitialStates().template toAdd().exportToDot("init.dot"); + // 4. if the initial states are not maybe states, then we can refine at this point. storm::dd::Bdd initialMaybeStates = (game.getInitialStates() && maybeMin) || (game.getInitialStates() && maybeMax); + initialMaybeStates.template toAdd().exportToDot("initmaybe.dot"); 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."); @@ -255,13 +338,57 @@ namespace storm { return result; } + STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states."); + // 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); } else { + + // At this point, we know that we cannot answer the query without further numeric computation. + STORM_LOG_TRACE("Starting numerical solution step."); + + // Prepare some storage that we use on-demand during the quantitative solving step. + storm::dd::Add minResult = prob01.min.second.states.template toAdd(); + storm::dd::Add maxResult = prob01.max.second.states.template toAdd(); + storm::dd::Add initialStatesAdd = game.getInitialStates().template toAdd(); + + ValueType minValue = (prob01.min.second.states && game.getInitialStates()) == game.getInitialStates() ? storm::utility::one() : storm::utility::zero(); + if (!maybeMin.isZero()) { + minResult += solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.states); + storm::dd::Add initialStateMin = initialStatesAdd * minResult; + STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() == 1, "Wrong number of results for initial states."); + minValue = initialStateMin.getMax(); + } + STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue); - // If we can already answer the question, do not solve the game numerically. + // Check whether we can abort the computation because of the lower value. + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, minValue); + if (result) { + return result; + } + ValueType maxValue = (prob01.max.second.states && game.getInitialStates()) == game.getInitialStates() ? storm::utility::one() : storm::utility::zero(); + if (!maybeMax.isZero()) { + maxResult += solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.states, boost::optional>(minResult)); + storm::dd::Add initialStateMax = (initialStatesAdd * maxResult); + STORM_LOG_ASSERT(initialStateMax.getNonZeroCount() == 1, "Wrong number of results for initial states."); + maxValue = initialStateMax.getMax(); + } + STORM_LOG_TRACE("Obtained quantitative upper bound " << minValue); + + // Check whether we can abort the computation because of the upper value. + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, maxValue); + if (result) { + return result; + } + + STORM_LOG_DEBUG("Obtained quantitative bounds [" << minValue << ", " << maxValue << "] on the actual value for the initial states."); + + result = checkForResultAfterQuantitativeCheck(checkTask, minValue, maxValue); + if (result) { + return result; + } STORM_LOG_ASSERT(false, "Quantiative refinement not yet there. :)"); } @@ -279,8 +406,8 @@ namespace storm { STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || prob0.hasPlayer1Strategy(), "Unable to proceed without strategy."); STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || prob0.hasPlayer2Strategy(), "Unable to proceed without strategy."); - STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob0.hasPlayer1Strategy(), "Unable to proceed without strategy."); - STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob0.hasPlayer2Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob1.hasPlayer1Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob1.hasPlayer2Strategy(), "Unable to proceed without strategy."); STORM_LOG_TRACE("Player 1: " << player1Direction << ", player 2: " << player2Direction << ": " << prob0.states.getNonZeroCount() << " 'no' states, " << prob1.states.getNonZeroCount() << " 'yes' states."); return std::make_pair(prob0, prob1); diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index ccb762fbf..347e317c1 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -10,12 +10,12 @@ namespace storm { namespace solver { template - SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) : gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { + SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) : gameMatrix(gameMatrix), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.template toAdd()), illegalPlayer2Mask(illegalPlayer2Mask.template toAdd()), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { // Intentionally left empty. } template - SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { + SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), gameMatrix(gameMatrix), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.template toAdd()), illegalPlayer2Mask(illegalPlayer2Mask.template toAdd()), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { // Intentionally left empty. } @@ -33,16 +33,18 @@ namespace storm { tmp += b; // Now abstract from player 2 and player 1 variables. - switch (player2Goal) { - case OptimizationDirection::Minimize: tmp = tmp.minAbstract(this->player2Variables); break; - case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player2Variables); break; + if (player2Goal == storm::OptimizationDirection::Maximize) { + tmp = tmp.maxAbstract(this->player2Variables); + } else { + tmp = (tmp + illegalPlayer2Mask).minAbstract(this->player2Variables); } - - switch (player1Goal) { - case OptimizationDirection::Minimize: tmp = tmp.minAbstract(this->player1Variables); break; - case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player1Variables); break; + + if (player1Goal == storm::OptimizationDirection::Maximize) { + tmp = tmp.maxAbstract(this->player1Variables); + } else { + tmp = (tmp + illegalPlayer1Mask).minAbstract(this->player1Variables); } - + // Now check if the process already converged within our precision. converged = xCopy.equalModuloPrecision(tmp, precision, relative); diff --git a/src/solver/SymbolicGameSolver.h b/src/solver/SymbolicGameSolver.h index 286a5027c..91802a2bf 100644 --- a/src/solver/SymbolicGameSolver.h +++ b/src/solver/SymbolicGameSolver.h @@ -25,6 +25,8 @@ namespace storm { * * @param gameMatrix The matrix defining the coefficients of the game. * @param allRows A BDD characterizing all rows of the equation system. + * @param illegalPlayer1Mask A BDD characterizing the illegal choices of player 1. + * @param illegalPlayer2Mask A BDD characterizing the illegal choices of player 2. * @param rowMetaVariables The meta variables used to encode the rows of the matrix. * @param columnMetaVariables The meta variables used to encode the columns of the matrix. * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta @@ -32,13 +34,15 @@ namespace storm { * @param player1Variables The meta variables used to encode the player 1 choices. * @param player2Variables The meta variables used to encode the player 2 choices. */ - SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables); + SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables); /*! * Constructs a symbolic game solver with the given meta variable sets and pairs. * * @param gameMatrix The matrix defining the coefficients of the game. * @param allRows A BDD characterizing all rows of the equation system. + * @param illegalPlayer1Mask A BDD characterizing the illegal choices of player 1. + * @param illegalPlayer2Mask A BDD characterizing the illegal choices of player 2. * @param rowMetaVariables The meta variables used to encode the rows of the matrix. * @param columnMetaVariables The meta variables used to encode the columns of the matrix. * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta @@ -50,7 +54,7 @@ namespace storm { * equation system iteratively. * @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one. */ - SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); /*! * Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon @@ -71,6 +75,12 @@ namespace storm { // A BDD characterizing all rows of the equation system. storm::dd::Bdd const& allRows; + // An ADD that can be used to compensate for the illegal choices of player 1. + storm::dd::Add illegalPlayer1Mask; + + // An ADD that can be used to compensate for the illegal choices of player 2. + storm::dd::Add illegalPlayer2Mask; + // The row variables. std::set const& rowMetaVariables; diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 8c968bfcf..ceb97b14e 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -162,6 +162,12 @@ namespace storm { return Add(this->getDdManager(), internalAdd.minAbstract(cube), Dd::subtractMetaVariables(*this, cube)); } + template + Add Add::minAbstractExcept0(std::set const& metaVariables) const { + Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); + return Add(this->getDdManager(), internalAdd.minAbstractExcept0(cube), Dd::subtractMetaVariables(*this, cube)); + } + template Add Add::maxAbstract(std::set const& metaVariables) const { Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index 67747e0e4..13e4f8436 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -256,7 +256,14 @@ namespace storm { * @param metaVariables The meta variables from which to abstract. */ Add minAbstract(std::set const& metaVariables) const; - + + /*! + * Min-abstracts from the given meta variables but treats 0 as the largest possible value. + * + * @param metaVariables The meta variables from which to abstract. + */ + Add minAbstractExcept0(std::set const& metaVariables) const; + /*! * Max-abstracts from the given meta variables. * diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 522477bd6..d375a1661 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -146,6 +146,11 @@ namespace storm { return InternalAdd(ddManager, this->getCuddAdd().MinAbstract(cube.toAdd().getCuddAdd())); } + template + InternalAdd InternalAdd::minAbstractExcept0(InternalBdd const& cube) const { + return InternalAdd(ddManager, this->getCuddAdd().MinAbstractExcept0(cube.toAdd().getCuddAdd())); + } + template InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->getCuddAdd().MaxAbstract(cube.toAdd().getCuddAdd())); diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index 9b7bca255..191d79e32 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -259,7 +259,14 @@ namespace storm { * @param cube The cube from which to abstract. */ InternalAdd minAbstract(InternalBdd const& cube) const; - + + /*! + * Min-abstracts from the given cube, but treats 0 as the largest possible value. + * + * @param cube The cube from which to abstract. + */ + InternalAdd minAbstractExcept0(InternalBdd const& cube) const; + /*! * Max-abstracts from the given cube. * diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index af7832945..938520b26 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -305,13 +305,25 @@ namespace storm { InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMin(cube.sylvanBdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstract"); } #endif + + template + InternalAdd InternalAdd::minAbstractExcept0(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractExcept0"); + } + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::minAbstractExcept0(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractExcept0"); + } +#endif template InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index b073af6cb..a9d88ba6a 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -261,7 +261,14 @@ namespace storm { * @param cube The cube from which to abstract. */ InternalAdd minAbstract(InternalBdd const& cube) const; - + + /*! + * Min-abstracts from the given cube, but treats 0 as the largest possible value. + * + * @param cube The cube from which to abstract. + */ + InternalAdd minAbstractExcept0(InternalBdd const& cube) const; + /*! * Max-abstracts from the given cube. * diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index f357256be..5fd6b9682 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -955,7 +955,7 @@ namespace storm { solution = tmp; ++iterations; } - + // Since we have determined the inverse of the desired set, we need to complement it now. solution = !solution && model.getReachableStates(); diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index bd2a6e27f..3882d7881 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -35,8 +35,8 @@ namespace storm { } template - std::unique_ptr> SymbolicGameSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const { - return std::unique_ptr>(new storm::solver::SymbolicGameSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); + std::unique_ptr> SymbolicGameSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const { + return std::unique_ptr>(new storm::solver::SymbolicGameSolver(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); } template diff --git a/src/utility/solver.h b/src/utility/solver.h index 210c19645..4b26e7b24 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -72,7 +72,7 @@ namespace storm { template class SymbolicGameSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; + virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; }; template diff --git a/test/functional/solver/FullySymbolicGameSolverTest.cpp b/test/functional/solver/FullySymbolicGameSolverTest.cpp index d5098b5f5..8da44ca92 100644 --- a/test/functional/solver/FullySymbolicGameSolverTest.cpp +++ b/test/functional/solver/FullySymbolicGameSolverTest.cpp @@ -35,7 +35,14 @@ TEST(FullySymbolicGameSolverTest, Solve_Cudd) { matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 1).template toAdd() * manager->getEncoding(pl1.first, 1).template toAdd() * manager->getEncoding(pl2.first, 1).template toAdd() * manager->getConstant(1); std::unique_ptr> solverFactory(new storm::utility::solver::SymbolicGameSolverFactory()); - std::unique_ptr> solver = solverFactory->create(matrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables); + + storm::dd::Bdd tmp = matrix.toBdd().existsAbstract({state.second}); + storm::dd::Bdd illegalPlayer2Mask = !tmp && manager->getRange(state.first); + storm::dd::Bdd illegalPlayer1Mask = tmp.existsAbstract({pl2.first}); + illegalPlayer2Mask &= illegalPlayer1Mask; + illegalPlayer1Mask &= !illegalPlayer1Mask && manager->getRange(state.first); + + std::unique_ptr> solver = solverFactory->create(matrix, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables); // Create solution and target state vector. storm::dd::Add x = manager->template getAddZero(); @@ -93,7 +100,14 @@ TEST(FullySymbolicGameSolverTest, Solve_Sylvan) { matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 1).template toAdd() * manager->getEncoding(pl1.first, 1).template toAdd() * manager->getEncoding(pl2.first, 1).template toAdd() * manager->getConstant(1); std::unique_ptr> solverFactory(new storm::utility::solver::SymbolicGameSolverFactory()); - std::unique_ptr> solver = solverFactory->create(matrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables); + + storm::dd::Bdd tmp = matrix.toBdd().existsAbstract({state.second}); + storm::dd::Bdd illegalPlayer2Mask = !tmp && manager->getRange(state.first); + storm::dd::Bdd illegalPlayer1Mask = tmp.existsAbstract({pl2.first}); + illegalPlayer2Mask &= illegalPlayer1Mask; + illegalPlayer1Mask &= !illegalPlayer1Mask && manager->getRange(state.first); + + std::unique_ptr> solver = solverFactory->create(matrix, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables); // Create solution and target state vector. storm::dd::Add x = manager->template getAddZero();