From f45b7f9171f0dbd80bab11ce5ba81b3943d23ceb Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 26 Aug 2016 15:00:59 +0200 Subject: [PATCH] fixed some bugs and started on quantitative refinement Former-commit-id: 31259ad29969c19f05fa6b1c4aa813ebd349de92 --- .../3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c | 4 +- resources/3rdparty/include_cudd.cmake | 2 +- src/abstraction/StateSetAbstractor.cpp | 3 - src/abstraction/prism/AbstractCommand.cpp | 11 ++- src/abstraction/prism/AbstractModule.cpp | 4 +- src/abstraction/prism/AbstractProgram.cpp | 2 +- src/abstraction/prism/GameBddResult.cpp | 4 +- src/abstraction/prism/GameBddResult.h | 3 +- .../abstraction/GameBasedMdpModelChecker.cpp | 80 ++++++++++++++----- src/models/symbolic/Model.cpp | 5 ++ src/models/symbolic/Model.h | 7 ++ src/solver/OptimizationDirection.cpp | 2 +- src/solver/SymbolicGameSolver.cpp | 61 ++++++++++++-- src/solver/SymbolicGameSolver.h | 4 +- src/storage/dd/cudd/InternalCuddAdd.cpp | 6 +- 15 files changed, 143 insertions(+), 55 deletions(-) diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c index 9ba2ab69a..4ffff8722 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c @@ -1007,7 +1007,7 @@ cuddAddMinAbstractRepresentativeRecur( return one; } if (cuddIsConstant(f)) { - res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube)); + res = cuddAddMinAbstractRepresentativeRecur(manager, f, cuddT(cube)); if (res == NULL) { return(NULL); } @@ -1193,7 +1193,7 @@ cuddAddMaxAbstractRepresentativeRecur( return one; } if (cuddIsConstant(f)) { - res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube)); + res = cuddAddMaxAbstractRepresentativeRecur(manager, f, cuddT(cube)); if (res == NULL) { return(NULL); } diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake index 1b26c6987..f8830d64c 100644 --- a/resources/3rdparty/include_cudd.cmake +++ b/resources/3rdparty/include_cudd.cmake @@ -28,4 +28,4 @@ add_dependencies(resources cudd3) message(STATUS "StoRM - Linking with CUDD ${CUDD_VERSION_STRING}") #message("StoRM - CUDD include dir: ${CUDD_INCLUDE_DIR}") -include_directories(${CUDD_INCLUDE_DIR}) \ No newline at end of file +include_directories(${CUDD_INCLUDE_DIR}) diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp index 77337751d..92c763e5c 100644 --- a/src/abstraction/StateSetAbstractor.cpp +++ b/src/abstraction/StateSetAbstractor.cpp @@ -65,7 +65,6 @@ namespace storm { template storm::dd::Bdd StateSetAbstractor::getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { - STORM_LOG_TRACE("Building source state BDD."); storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); for (auto const& variableIndexPair : relevantPredicatesAndVariables) { if (model.getBooleanValue(variableIndexPair.first)) { @@ -81,8 +80,6 @@ namespace storm { void StateSetAbstractor::recomputeCachedBdd() { // Now check whether we need to recompute the cached BDD. std::set newRelevantPredicateIndices = localExpressionInformation.getRelatedExpressions(concretePredicateVariables); - STORM_LOG_TRACE("Found " << newRelevantPredicateIndices.size() << " relevant predicates in abstractor."); - // Since the number of relevant predicates is monotonic, we can simply check for the size here. STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates."); bool recomputeBdd = newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size(); diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index cb46308a4..0f1dc3932 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -21,7 +21,7 @@ namespace storm { namespace abstraction { namespace prism { template - AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0, 0), decisionVariables(), guardIsPredicate(guardIsPredicate), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) { + AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), guardIsPredicate(guardIsPredicate), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -109,8 +109,9 @@ namespace storm { STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty."); STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty."); + // We start with the distribution index of 1, becase 0 is reserved for a potential bottom choice. + uint_fast64_t distributionIndex = 1; storm::dd::Bdd allDistributions = this->getAbstractionInformation().getDdManager().getBddZero(); - uint_fast64_t distributionIndex = 0; for (auto const& distribution : sourceDistributionsPair.second) { allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, numberOfVariablesNeeded); ++distributionIndex; @@ -126,7 +127,7 @@ namespace storm { STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions."); // Cache the result. - cachedDd = GameBddResult(resultBdd, numberOfVariablesNeeded, maximalNumberOfChoices); + cachedDd = GameBddResult(resultBdd, numberOfVariablesNeeded); } template @@ -215,7 +216,6 @@ namespace storm { template storm::dd::Bdd AbstractCommand::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { - STORM_LOG_TRACE("Building source state BDD."); storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) { if (model.getBooleanValue(variableIndexPair.first)) { @@ -231,7 +231,6 @@ namespace storm { template storm::dd::Bdd AbstractCommand::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const { - STORM_LOG_TRACE("Building distribution BDD."); storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { @@ -330,7 +329,7 @@ namespace storm { result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false); // Add the command encoding and the next free player 2 encoding. - result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); + result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(0, numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); return result; } diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp index 79c144c9d..b9b001bd7 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -41,11 +41,9 @@ namespace storm { // First, we retrieve the abstractions of all commands. std::vector> commandDdsAndUsedOptionVariableCounts; uint_fast64_t maximalNumberOfUsedOptionVariables = 0; - uint_fast64_t nextFreePlayer2Index = 0; for (auto& command : commands) { commandDdsAndUsedOptionVariableCounts.push_back(command.getAbstractBdd()); maximalNumberOfUsedOptionVariables = std::max(maximalNumberOfUsedOptionVariables, commandDdsAndUsedOptionVariableCounts.back().numberOfPlayer2Variables); - nextFreePlayer2Index = std::max(nextFreePlayer2Index, commandDdsAndUsedOptionVariableCounts.back().nextFreePlayer2Index); } // Then, we build the module BDD by adding the single command DDs. We need to make sure that all command @@ -54,7 +52,7 @@ namespace storm { for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) { result |= commandDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(commandDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables); } - return GameBddResult(result, maximalNumberOfUsedOptionVariables, nextFreePlayer2Index); + return GameBddResult(result, maximalNumberOfUsedOptionVariables); } template diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index a175b62ad..ec146d67e 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -180,7 +180,7 @@ namespace storm { 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()); + newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify(); break; } } diff --git a/src/abstraction/prism/GameBddResult.cpp b/src/abstraction/prism/GameBddResult.cpp index df22713d7..2e7df1f5e 100644 --- a/src/abstraction/prism/GameBddResult.cpp +++ b/src/abstraction/prism/GameBddResult.cpp @@ -5,12 +5,12 @@ namespace storm { namespace prism { template - GameBddResult::GameBddResult() : bdd(), numberOfPlayer2Variables(0), nextFreePlayer2Index(0) { + GameBddResult::GameBddResult() : bdd(), numberOfPlayer2Variables(0) { // Intentionally left empty. } template - GameBddResult::GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables, uint_fast64_t nextFreePlayer2Index) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables), nextFreePlayer2Index(nextFreePlayer2Index) { + GameBddResult::GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables) { // Intentionally left empty. } diff --git a/src/abstraction/prism/GameBddResult.h b/src/abstraction/prism/GameBddResult.h index c04309e98..02ad2f724 100644 --- a/src/abstraction/prism/GameBddResult.h +++ b/src/abstraction/prism/GameBddResult.h @@ -9,11 +9,10 @@ namespace storm { template struct GameBddResult { GameBddResult(); - GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables, uint_fast64_t nextFreePlayer2Index); + GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables); storm::dd::Bdd bdd; uint_fast64_t numberOfPlayer2Variables; - uint_fast64_t nextFreePlayer2Index; }; } diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 2357770af..18451494c 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -195,18 +195,19 @@ namespace storm { template void refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, detail::GameProb01Result const& prob01, storm::dd::Bdd const& transitionMatrixBdd) { - storm::dd::Bdd transitionsInIntersection = (transitionMatrixBdd && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy() && prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy()).existsAbstract(game.getNondeterminismVariables()); - - // First, we have to find the pivot state candidates. Start by constructing the reachable fragment of the - // state space *under both* strategy pairs. - storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), transitionsInIntersection, game.getRowVariables(), game.getColumnVariables()); - - // Then constrain this set by requiring that the two stratey pairs resolve the nondeterminism differently. - pivotStates &= (prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy()).exclusiveOr(prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy()).existsAbstract(game.getNondeterminismVariables()); + // Build the fragment of states that is reachable by any combination of the player 1 and player 2 strategies. + storm::dd::Bdd reachableTransitions = prob01.min.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy(); + reachableTransitions = (prob01.min.first.getPlayer1Strategy() && reachableTransitions) || (prob01.max.second.getPlayer1Strategy() && reachableTransitions); + reachableTransitions &= transitionMatrixBdd; + reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); + storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); + + // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different. + pivotStates &= ((prob01.min.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy()) && (prob01.min.first.getPlayer2Strategy().exclusiveOr(prob01.max.second.getPlayer2Strategy()))).existsAbstract(game.getNondeterminismVariables()); STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); // Now that we have the pivot state candidates, we need to pick one. - storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), transitionsInIntersection, game.getRowVariables(), game.getColumnVariables(), pivotStates); + storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates); // Compute the lower and the upper choice for the pivot state. std::set variablesToAbstract = game.getNondeterminismVariables(); @@ -235,7 +236,22 @@ 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) { + struct MaybeStateResult { + MaybeStateResult() = default; + + MaybeStateResult(storm::dd::Add const& values, storm::dd::Bdd const& player1Strategy, storm::dd::Bdd const& player2Strategy) : values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { + // Intentionally left empty. + } + + storm::dd::Add values; + storm::dd::Bdd player1Strategy; + storm::dd::Bdd player2Strategy; + }; + + template + MaybeStateResult 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> startInfo = boost::none) { + + STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << "."); // Compute the ingredients of the equation system. storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); @@ -248,14 +264,28 @@ namespace storm { submatrix *= maybeStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs()); // Cut the starting vector to the maybe states of this query. - if (startVector) { - startVector.get() *= maybeStatesAdd; + storm::dd::Add startVector; + if (startInfo) { + startVector = startInfo.get().values * maybeStatesAdd; + } else { + startVector = game.getManager().template getAddZero(); } // 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); + solver->setGeneratePlayersStrategies(true); + auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector); + storm::dd::Bdd player1Strategy = solver->getPlayer1Strategy(); + storm::dd::Bdd player2Strategy = solver->getPlayer2Strategy(); + + // If we were given a starting point, we fix the strategies now. That is, we only deviate from the + if (startInfo) { + player1Strategy = values.greater(startInfo.get().values).ite(player1Strategy, startInfo.get().player1Strategy); + player1Strategy = values.greater(startInfo.get().values).ite(player1Strategy, startInfo.get().player1Strategy); + } + + return MaybeStateResult(values, player1Strategy, player2Strategy); } template @@ -285,9 +315,8 @@ namespace storm { } storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedProgram, initialPredicates, smtSolverFactory); - for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) { - STORM_LOG_TRACE("Starting iteration " << 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. @@ -351,13 +380,16 @@ namespace storm { storm::dd::Add initialStatesAdd = game.getInitialStates().template toAdd(); ValueType minValue = (prob01.min.second.states && game.getInitialStates()) == game.getInitialStates() ? storm::utility::one() : storm::utility::zero(); + MaybeStateResult minMaybeStateResult; if (!maybeMin.isZero()) { - minResult += solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.states); + minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.states); + minResult += minMaybeStateResult.values; storm::dd::Add initialStateMin = initialStatesAdd * minResult; - STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() == 1, "Wrong number of results for initial states."); + // Here we can only require a non-zero count of *at most* one, because the result may actually be 0. + STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() <= 1, "Wrong number of results for initial states."); minValue = initialStateMin.getMax(); } - STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue); + STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue << "."); // Check whether we can abort the computation because of the lower value. result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, minValue); @@ -366,13 +398,18 @@ namespace storm { } ValueType maxValue = (prob01.max.second.states && game.getInitialStates()) == game.getInitialStates() ? storm::utility::one() : storm::utility::zero(); + MaybeStateResult maxMaybeStateResult; if (!maybeMax.isZero()) { - maxResult += solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.states, boost::optional>(minResult)); + // FIXME: fix strategy: only change if improved. + maxMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.states, boost::optional>(minMaybeStateResult)); + maxResult += maxMaybeStateResult.values; storm::dd::Add initialStateMax = (initialStatesAdd * maxResult); + // Unlike in the min-case, we can require a non-zero count of 1 here, because if the max was in + // fact 0, the result would be 0, which would have been detected earlier by the graph algorithms. STORM_LOG_ASSERT(initialStateMax.getNonZeroCount() == 1, "Wrong number of results for initial states."); maxValue = initialStateMax.getMax(); } - STORM_LOG_TRACE("Obtained quantitative upper bound " << minValue); + 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); @@ -386,6 +423,9 @@ namespace storm { if (result) { return result; } + + // If we arrived at this point, it means that we have all qualitative and quantitative information + // about the game, but we could not yet answer the query. In this case, we need to refine. STORM_LOG_ASSERT(false, "Quantiative refinement not yet there. :)"); } diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 97abf9581..ad1dadc6c 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -57,6 +57,11 @@ namespace storm { return *manager; } + template + std::shared_ptr> const& Model::getManagerAsSharedPointer() const { + return manager; + } + template storm::dd::Bdd const& Model::getReachableStates() const { return reachableStates; diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index 359ae8255..4483a2a6c 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -109,6 +109,13 @@ namespace storm { * @return The manager responsible for the DDs that represent this model. */ storm::dd::DdManager& getManager(); + + /*! + * Retrieves the manager responsible for the DDs that represent this model. + * + * @return The manager responsible for the DDs that represent this model. + */ + std::shared_ptr> const& getManagerAsSharedPointer() const; /*! * Retrieves the reachable states of the model. diff --git a/src/solver/OptimizationDirection.cpp b/src/solver/OptimizationDirection.cpp index cd88657b9..7c4691f69 100644 --- a/src/solver/OptimizationDirection.cpp +++ b/src/solver/OptimizationDirection.cpp @@ -31,7 +31,7 @@ namespace storm { } std::ostream& operator<<(std::ostream& out, OptimizationDirection d) { - return d == OptimizationDirection::Minimize ? out << "Minimize" : out << "Maximize"; + return d == OptimizationDirection::Minimize ? out << "minimize" : out << "maximize"; } } } diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index b6f73e6df..8788ce122 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -20,17 +20,27 @@ namespace storm { } template - SymbolicGameSolver::SymbolicGameSolver(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, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.template toAdd()), illegalPlayer2Mask(illegalPlayer2Mask.template toAdd()), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) { + SymbolicGameSolver::SymbolicGameSolver(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, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) { // Intentionally left empty. } template - storm::dd::Add SymbolicGameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b) const { + storm::dd::Add SymbolicGameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b) { // Set up the environment. storm::dd::Add xCopy = x; uint_fast64_t iterations = 0; bool converged = false; - + + // Prepare some data storage in case we need to generate strategies. + if (generatePlayer1Strategy) { + player1Strategy = A.getDdManager().getBddZero(); + } + boost::optional> previousPlayer2Values; + if (generatePlayer2Strategy) { + previousPlayer2Values = A.getDdManager().template getAddZero(); + player2Strategy = A.getDdManager().getBddZero(); + } + do { // Compute tmp = A * x + b. storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); @@ -39,15 +49,50 @@ namespace storm { // Now abstract from player 2 and player 1 variables. if (player2Goal == storm::OptimizationDirection::Maximize) { - tmp = tmp.maxAbstract(this->player2Variables); + storm::dd::Add newValues = tmp.maxAbstract(this->player2Variables); + + if (generatePlayer2Strategy) { + // Update only the choices that strictly improved the value. + storm::dd::Bdd maxChoices = tmp.maxAbstractRepresentative(this->player2Variables); + player2Strategy = newValues.greater(previousPlayer2Values.get()).ite(maxChoices, player2Strategy.get()); + previousPlayer2Values = newValues; + } + + tmp = newValues; } else { - tmp = (tmp + illegalPlayer2Mask).minAbstract(this->player2Variables); + tmp = (tmp + illegalPlayer2Mask); + storm::dd::Add newValues = tmp.minAbstract(this->player2Variables); + + if (generatePlayer2Strategy) { + player2Strategy = tmp.minAbstractRepresentative(this->player2Variables); + } + + tmp = newValues; } if (player1Goal == storm::OptimizationDirection::Maximize) { - tmp = tmp.maxAbstract(this->player1Variables); + tmp.exportToDot("pl1_val_" + std::to_string(iterations) + ".dot"); + storm::dd::Add newValues = tmp.maxAbstract(this->player1Variables); + + newValues.exportToDot("pl1_valabs_" + std::to_string(iterations) + ".dot"); + if (generatePlayer1Strategy) { + // Update only the choices that strictly improved the value. + storm::dd::Bdd maxChoices = tmp.maxAbstractRepresentative(this->player1Variables); + maxChoices.template toAdd().exportToDot("pl1_choices_" + std::to_string(iterations) + ".dot"); + player1Strategy = newValues.greater(xCopy).ite(maxChoices, player1Strategy.get()); + player1Strategy.get().template toAdd().exportToDot("pl1_" + std::to_string(iterations) + ".dot"); + } + + tmp = newValues; } else { - tmp = (tmp + illegalPlayer1Mask).minAbstract(this->player1Variables); + tmp = (tmp + illegalPlayer1Mask); + storm::dd::Add newValues = tmp.minAbstract(this->player1Variables); + + if (generatePlayer1Strategy) { + player1Strategy = tmp.minAbstractRepresentative(this->player1Variables); + } + + tmp = newValues; } // Now check if the process already converged within our precision. @@ -75,7 +120,7 @@ namespace storm { } template - void SymbolicGameSolver::setGeneratePlayerStrategies(bool value) { + void SymbolicGameSolver::setGeneratePlayersStrategies(bool value) { setGeneratePlayer1Strategy(value); setGeneratePlayer2Strategy(value); } diff --git a/src/solver/SymbolicGameSolver.h b/src/solver/SymbolicGameSolver.h index a6ac3c007..6ebe5d052 100644 --- a/src/solver/SymbolicGameSolver.h +++ b/src/solver/SymbolicGameSolver.h @@ -66,12 +66,12 @@ namespace storm { * @param b The vector to add after matrix-vector multiplication. * @return The solution vector. */ - virtual storm::dd::Add solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b) const; + virtual storm::dd::Add solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b); // Setters that enable the generation of the players' strategies. void setGeneratePlayer1Strategy(bool value); void setGeneratePlayer2Strategy(bool value); - void setGeneratePlayerStrategies(bool value); + void setGeneratePlayersStrategies(bool value); // Getters to retrieve the players' strategies. Only legal if they were generated. storm::dd::Bdd const& getPlayer1Strategy() const; diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 6162ef7c5..db4323c6a 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -149,8 +149,7 @@ namespace storm { template InternalBdd InternalAdd::minAbstractRepresentative(InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractRepresentative"); - //return InternalAdd(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd().getCuddAdd())); + return InternalBdd(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd().getCuddAdd())); } template @@ -165,8 +164,7 @@ namespace storm { template InternalBdd InternalAdd::maxAbstractRepresentative(InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: maxAbstractRepresentative"); - //return InternalAdd(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd().getCuddAdd())); + return InternalBdd(ddManager, this->getCuddAdd().MaxAbstractRepresentative(cube.toAdd().getCuddAdd())); } template