diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index e511c3e29..da11864b4 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -1097,9 +1097,14 @@ namespace storm { ValueType pivotStateDeviation = storm::utility::zero(); auto const& player2Grouping = transitionMatrix.getRowGroupIndices(); + storm::storage::BitVector visitedStates(initialStates.size()); while (!dijkstraQueue.empty()) { auto distanceStatePair = *dijkstraQueue.begin(); uint64_t currentState = distanceStatePair.second; + visitedStates.set(currentState); + std::cout << "current: " << currentState << std::endl; + std::cout << "visited: " << visitedStates << std::endl; + ValueType currentDistance = distanceStatePair.first; dijkstraQueue.erase(dijkstraQueue.begin()); @@ -1128,10 +1133,10 @@ namespace storm { if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && minStrategyPair.getPlayer2Strategy().getChoice(player2Successor) != maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor)) { isPivotState = true; } - } + } + // If it is indeed a pivot state, we can abort the search here. if (isPivotState) { - if (considerDeviation && foundPivotState) { ValueType deviationOfCurrentState = (*upperValues)[currentState] - (*lowerValues)[currentState]; if (deviationOfCurrentState > pivotStateDeviation) { @@ -1154,10 +1159,13 @@ namespace storm { } } + // TODO: remember the strategy from which we came and only go on to explore that further? + // Otherwise, we explore all its relevant successors. if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { uint64_t minPlayer2Successor = minStrategyPair.getPlayer1Strategy().getChoice(currentState); uint64_t minPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minPlayer2Successor); + STORM_LOG_ASSERT(!maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(minPlayer2Successor) || minStrategyPair.getPlayer2Strategy().getChoice(minPlayer2Successor) == minPlayer2Choice, "Did not expect deviation in player 2 strategy."); STORM_LOG_ASSERT(player2Grouping[minPlayer2Successor] <= minPlayer2Choice && minPlayer2Choice < player2Grouping[minPlayer2Successor + 1], "Illegal choice for player 2."); for (auto const& entry : transitionMatrix.getRow(minPlayer2Choice)) { @@ -1175,10 +1183,13 @@ namespace storm { dijkstraQueue.emplace(alternateDistance, player1Successor); } } + } else { + STORM_LOG_ASSERT(targetStates.get(currentState), "Expecting min strategy for non-target states."); } if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { uint64_t maxPlayer2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); uint64_t maxPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxPlayer2Successor); + STORM_LOG_ASSERT(!minStrategyPair.getPlayer2Strategy().hasDefinedChoice(maxPlayer2Successor) || minStrategyPair.getPlayer2Strategy().getChoice(maxPlayer2Successor) == maxPlayer2Choice, "Did not expect deviation in player 2 strategy."); STORM_LOG_ASSERT(player2Grouping[maxPlayer2Successor] <= maxPlayer2Choice && maxPlayer2Choice < player2Grouping[maxPlayer2Successor + 1], "Illegal choice for player 2."); for (auto const& entry : transitionMatrix.getRow(maxPlayer2Choice)) { @@ -1188,7 +1199,7 @@ namespace storm { } ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one(); - if (probabilityDistances ? alternateDistance > distances[player1Successor] : !probabilityDistances && alternateDistance < distances[player1Successor]) { + if (probabilityDistances ? alternateDistance > distances[player1Successor] : alternateDistance < distances[player1Successor]) { distances[player1Successor] = alternateDistance; if (generatePredecessors) { result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[maxPlayer2Successor]); @@ -1196,6 +1207,8 @@ namespace storm { dijkstraQueue.emplace(alternateDistance, player1Successor); } } + } else { + STORM_LOG_ASSERT(targetStates.get(currentState), "Expecting max strategy for non-target states."); } } @@ -1205,6 +1218,7 @@ namespace storm { // If we arrived at this point, we have explored all relevant states, but none of them was a pivot state, // which can happen when trying to refine using the qualitative result only. + STORM_LOG_TRACE("Did not find pivot state in explicit Dijkstra search."); return boost::none; } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 46dde3b65..f7374dd20 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -2,6 +2,7 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/symbolic/Dtmc.h" @@ -33,6 +34,7 @@ #include "storm/solver/SymbolicGameSolver.h" #include "storm/solver/StandardGameSolver.h" +#include "storm/environment/Environment.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" @@ -414,8 +416,10 @@ namespace storm { // If there is a previous result, unpack the previous values with respect to the new ODD. if (previousResult) { - previousResult.get().odd.oldToNewIndex(odd, [&previousResult,&result,player2Min] (uint64_t oldOffset, uint64_t newOffset) { - result.getValues()[newOffset] = player2Min ? previousResult.get().values.getMin().getValues()[oldOffset] : previousResult.get().values.getMax().getValues()[oldOffset]; + previousResult.get().odd.oldToNewIndex(odd, [&previousResult,&result,player2Min,player1Prob1States] (uint64_t oldOffset, uint64_t newOffset) { + if (!player2Min && !player1Prob1States.get(newOffset)) { + result.getValues()[newOffset] = player2Min ? previousResult.get().values.getMin().getValues()[oldOffset] : previousResult.get().values.getMax().getValues()[oldOffset]; + } }); } @@ -494,7 +498,7 @@ namespace storm { // Set values according to quantitative result (qualitative result has already been taken care of). storm::utility::vector::setVectorValues(result.getValues(), maybeStates, values); - + // Obtain strategies from solver and fuse them with the pre-existing strategy pair for the qualitative result. uint64_t previousPlayer1MaybeStates = 0; uint64_t previousPlayer2MaybeStates = 0; @@ -804,7 +808,7 @@ namespace storm { if (result) { return result; } - + // (8) Solve the max values and check whether we can give the answer already. quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, odd, &quantitativeResult.getMin(), &minStrategyPair)); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.getMax().getRange(initialStates)); @@ -820,6 +824,100 @@ namespace storm { return result; } +// std::cout << "target states " << targetStates << std::endl; + + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + std::cout << "state " << state << " has values [" << quantitativeResult.getMin().getValues()[state] << ", " << quantitativeResult.getMax().getValues()[state] << "]" << std::endl; + + STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << "."); + STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << "."); + + if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { + uint64_t lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state); + + STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (upper player 1 choice " << lowerPlayer1Choice << ")."); + uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); + + if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) { + uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); + + if (lowerPlayer2Choice != upperPlayer2Choice) { + ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); + ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); + + if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) { + minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice); + std::cout << "[min] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice << std::endl; + } + } + } + } + + if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { + uint64_t upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state); + + STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ")."); + uint64_t upperPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); + + if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) { + uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); + + if (lowerPlayer2Choice != upperPlayer2Choice) { + ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); + ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); + + if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) { + minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice); + std::cout << "[max] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice << std::endl; + } + } + } + } + } + + ///////// SANITY CHECK: apply lower strategy, obtain DTMC matrix and model check it. the values should + ///////// still be the lower ones. + storm::storage::SparseMatrixBuilder dtmcMatrixBuilder(player1Groups.size() - 1, player1Groups.size() - 1); + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + if (targetStates.get(state)) { + dtmcMatrixBuilder.addNextValue(state, state, storm::utility::one()); + } else { + uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minStrategyPair.getPlayer1Strategy().getChoice(state)); + for (auto const& entry : transitionMatrix.getRow(player2Choice)) { + dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue()); + } + } + } + auto dtmcMatrix = dtmcMatrixBuilder.build(); + std::vector sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(Environment(), storm::solver::SolveGoal(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false); + + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + std::cout << "state " << state << ": " << sanityValues[state] << " vs " << quantitativeResult.getMin().getValues()[state] << std::endl; + std::cout << "[min] state is prob0? " << qualitativeResult.getProb0Min().getStates().get(state) << ", prob1? " << qualitativeResult.getProb1Min().getStates().get(state) << std::endl; + STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]) < 1e-6, "Got weird min divergences!"); + } + ///////// SANITY CHECK: apply upper strategy, obtain DTMC matrix and model check it. the values should + ///////// still be the upper ones. + dtmcMatrixBuilder = storm::storage::SparseMatrixBuilder(player1Groups.size() - 1, player1Groups.size() - 1); + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + if (targetStates.get(state)) { + dtmcMatrixBuilder.addNextValue(state, state, storm::utility::one()); + } else { + uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxStrategyPair.getPlayer1Strategy().getChoice(state)); + for (auto const& entry : transitionMatrix.getRow(player2Choice)) { + dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue()); + } + } + } + dtmcMatrix = dtmcMatrixBuilder.build(); + sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(Environment(), storm::solver::SolveGoal(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false); + + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + std::cout << "state " << state << ": " << sanityValues[state] << " vs " << quantitativeResult.getMax().getValues()[state] << std::endl; + std::cout << "[max] state is prob0? " << qualitativeResult.getProb0Max().getStates().get(state) << ", prob1? " << qualitativeResult.getProb1Max().getStates().get(state) << std::endl; + STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]) < 1e-6, "Got weird max divergences!"); + } + // Make sure that all strategies are still valid strategies. STORM_LOG_ASSERT(minStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << minStrategyPair.getNumberOfUndefinedPlayer1States() << "."); STORM_LOG_ASSERT(maxStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << maxStrategyPair.getNumberOfUndefinedPlayer1States() << "."); @@ -926,7 +1024,6 @@ namespace storm { ExplicitQualitativeGameResultMinMax result; ExplicitQualitativeGameResult problematicStates = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); - std::cout << "Found " << problematicStates.getStates().getNumberOfSetBits() << " problematic states" << std::endl; result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair); result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair);