From 9b80c65d72e8b964fcd8ba888f5a87869f4ca9f2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 8 Jun 2018 16:38:38 +0200 Subject: [PATCH] more and more debugging --- .../abstraction/GameBasedMdpModelChecker.cpp | 87 +++++++++++++++++-- src/storm/storage/SparseMatrix.cpp | 12 +++ src/storm/utility/constants.h | 4 +- 3 files changed, 95 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index c8b758516..89920bf59 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -476,7 +476,7 @@ namespace storm { uint64_t maybeStatePosition = 0; previousPlayer2States = 0; for (auto state : maybeStates) { - if (state == 1976 || state == 46452 || state == 114590 || state == 84730 || state == 84575 || state == 84562 || state == 31895 || state == 84574 || state == 84561 || state == 32933 || state == 86740 || state == 86734 || state == 31789 || state == 86740 || state == 84360 || state == 84358) { + if (state == 2324 || state == 50377 || state == 50209) { std::cout << "dealing with problematic state " << state << " whose local offset is " << maybeStatePosition << std::endl; } uint64_t chosenPlayer2State = startingStrategyPair->getPlayer1Strategy().getChoice(state); @@ -484,13 +484,13 @@ namespace storm { uint64_t previousPlayer2MaybeStatesForState = 0; for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { if (player2MaybeStates.get(player2State)) { - if (state == 1976 || state == 46452 || state == 114590 || state == 84730 || state == 84575 || state == 84562 || state == 31895 || state == 84574 || state == 84561 || state == 32933 || state == 86740 || state == 86734 || state == 31789 || state == 86740 || state == 84360 || state == 84358) { + if (state == 2324 || state == 50377 || state == 50209) { std::cout << "player 2 state " << player2State << " is a player 2 maybe state with local index " << previousPlayer2States << " ranging from row " << submatrix.getRowGroupIndices()[previousPlayer2States] << " to " << submatrix.getRowGroupIndices()[previousPlayer2States + 1] << std::endl; } if (player2State == chosenPlayer2State) { player1Scheduler[maybeStatePosition] = previousPlayer2MaybeStatesForState; - if (state == 1976 || state == 46452 || state == 114590 || state == 84730 || state == 84575 || state == 84562 || state == 31895 || state == 84574 || state == 84561 || state == 32933 || state == 86740 || state == 86734 || state == 31789 || state == 86740 || state == 84360 || state == 84358) { + if (state == 2324 || state == 50377 || state == 50209) { std::cout << "player 1 scheduler chooses " << previousPlayer2MaybeStatesForState << " which globally is " << player2State << std::endl; } } @@ -499,12 +499,12 @@ namespace storm { if (startingStrategyPair->getPlayer2Strategy().hasDefinedChoice(player2State)) { player2Scheduler[previousPlayer2States] = startingStrategyPair->getPlayer2Strategy().getChoice(player2State) - transitionMatrix.getRowGroupIndices() [player2State]; - if (state == 1976 || state == 46452 || state == 114590 || state == 84730 || state == 84575 || state == 84562 || state == 31895 || state == 84574 || state == 84561 || state == 32933 || state == 86740 || state == 86734 || state == 31789 || state == 86740 || state == 84360 || state == 84358) { + if (state == 2324 || state == 50377 || state == 50209) { std::cout << "copied over choice " << player2Scheduler[previousPlayer2States] << " for player 2 (global index " << startingStrategyPair->getPlayer2Strategy().getChoice(player2State) << ")" << std::endl; } } else { player2Scheduler[previousPlayer2States] = 0; - if (state == 1976 || state == 46452 || state == 114590 || state == 84730 || state == 84575 || state == 84562 || state == 31895 || state == 84574 || state == 84561 || state == 32933 || state == 86740 || state == 86734 || state == 31789 || state == 86740 || state == 84360 || state == 84358) { + if (state == 2324 || state == 50377 || state == 50209) { std::cout << "did not copy (undefined) choice for player 2 (global index " << startingStrategyPair->getPlayer2Strategy().getChoice(player2State) << ")" << std::endl; } } @@ -517,6 +517,37 @@ namespace storm { ++maybeStatePosition; } STORM_LOG_ASSERT(previousPlayer2States == submatrix.getRowGroupCount(), "Expected correct number of player 2 states."); + } else { + // If the starting strategy pair was provided, we need to extract the choices of the maybe states here. + uint64_t maybeStatePosition = 0; + previousPlayer2States = 0; + for (auto state : maybeStates) { + if (state == 2324 || state == 50377 || state == 50209) { + std::cout << "dealing with problematic state " << state << " whose local offset is " << maybeStatePosition << std::endl; + } + + if (state == 2324 || state == 50377 || state == 50209) { + std::cout << "player 1 scheduler chooses " << player1Scheduler[maybeStatePosition] << " which globally is " << (player1Groups[state] + player1Scheduler[maybeStatePosition]) << std::endl; + } + + uint64_t previousPlayer2MaybeStatesForState = 0; + for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { + if (player2MaybeStates.get(player2State)) { + if (state == 2324 || state == 50377 || state == 50209) { + std::cout << "player 2 state " << player2State << " is a player 2 maybe state with local index " << previousPlayer2States << " ranging from row " << submatrix.getRowGroupIndices()[previousPlayer2States] << " to " << submatrix.getRowGroupIndices()[previousPlayer2States + 1] << std::endl; + } + + if (state == 2324 || state == 50377 || state == 50209) { + std::cout << "player 2 scheduler chooses " << player2Scheduler[previousPlayer2States] << " for player 2 (global index " << (transitionMatrix.getRowGroupIndices()[player2State] + player2Scheduler[previousPlayer2States]) << ")" << std::endl; + } + ++previousPlayer2MaybeStatesForState; + ++previousPlayer2States; + } + } + + ++maybeStatePosition; + } + STORM_LOG_ASSERT(previousPlayer2States == submatrix.getRowGroupCount(), "Expected correct number of player 2 states."); } // Solve actual game and track schedulers. @@ -530,18 +561,27 @@ namespace storm { uint64_t previousPlayer2MaybeStates = 0; for (auto state : maybeStates) { uint64_t previousPlayer2MaybeStatesForState = 0; + bool madePlayer1Choice = false; for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { if (player1Scheduler[previousPlayer1MaybeStates] == previousPlayer2MaybeStatesForState) { + if (state == 2324 || state == 50377 || state == 50209) { + std::cout << "player 1 choosing " << player2State << " in " << state << std::endl; + } strategyPair.getPlayer1Strategy().setChoice(state, player2State); + madePlayer1Choice = true; } if (player2MaybeStates.get(player2State)) { + if (state == 2324 || state == 50377 || state == 50209) { + std::cout << "player 2 choosing " << (transitionMatrix.getRowGroupIndices()[player2State] + player2Scheduler[previousPlayer2MaybeStates]) << " in " << player2State << " for player 1 state " << state << std::endl; + } strategyPair.getPlayer2Strategy().setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State] + player2Scheduler[previousPlayer2MaybeStates]); ++previousPlayer2MaybeStatesForState; ++previousPlayer2MaybeStates; } } + STORM_LOG_ASSERT(madePlayer1Choice, "Player 1 state " << state << " did not make a choice, scheduler: " << player1Scheduler[previousPlayer1MaybeStates] << "."); ++previousPlayer1MaybeStates; } @@ -1157,6 +1197,41 @@ namespace storm { STORM_LOG_TRACE("Got maximal deviation of " << maxDiff << "."); STORM_LOG_WARN_COND(sanityComparator.isZero(maxDiff), "Deviation " << maxDiff << " between computed value (" << quantitativeResult.getMin().getValues()[maxState] << ") and sanity check value (" << sanityValues[maxState] << ") in state " << maxState << " appears to be too high. (Obtained bounds were [" << quantitativeResult.getMin().getValues()[maxState] << ", " << quantitativeResult.getMax().getValues()[maxState] << "].)"); if (!sanityComparator.isZero(maxDiff)) { + ExplicitGameExporter exporter; + storm::storage::BitVector newInitialStates(player1Groups.size() - 1); + newInitialStates.set(maxState); + exporter.exportToJson("game" + std::to_string(iteration) + "_min.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, &minStrategyPair, static_cast(nullptr)); + exporter.exportToJson("game" + std::to_string(iteration) + "_max.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, static_cast(nullptr), &maxStrategyPair); + + + // Perform DFS from max diff state in upper system. + std::vector stack; + stack.push_back(maxState); + storm::storage::BitVector reachable(dtmcMatrix.getRowCount()); + + while (!stack.empty()) { + uint64_t currentState = stack.back(); + stack.pop_back(); + + std::cout << "exploring player 1 state " << currentState << " with " << (player1Groups[currentState + 1] - player1Groups[currentState]) << " player 2 successors from" << player1Groups[currentState] << " to " << player1Groups[currentState + 1] << std::endl; + uint64_t player2State = minStrategyPair.getPlayer1Strategy().getChoice(currentState); + std::cout << "going to player 2 state " << player2State << " with " << (player2Groups[player2State + 1] - player2Groups[player2State]) << " player 2 choices from " << player2Groups[player2State] << " to " << player2Groups[player2State + 1] << std::endl; + uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State); + std::cout << "which takes choice " << player2Choice << " which locally is " << (player2Choice - transitionMatrix.getRowGroupIndices()[player2State]) << std::endl; + for (auto const& entry : transitionMatrix.getRow(player2Choice)) { + std::cout << entry.getColumn() << " -> " << entry.getValue() << std::endl; + auto successor = entry.getColumn(); + if (!reachable.get(successor)) { + if (!targetStates.get(successor)) { + reachable.set(successor); + stack.push_back(successor); + } else { + std::cout << "found target state " << std::endl; + } + } + } + } + exit(-1); } @@ -1493,7 +1568,7 @@ namespace storm { ExplicitQualitativeGameResultMinMax result; - ExplicitQualitativeGameResult problematicStates = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); +// ExplicitQualitativeGameResult problematicStates = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); 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); diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 24d9e55f7..6e8c2333b 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1630,6 +1630,11 @@ namespace storm { currentValue += elementIt->getValue() * vector[elementIt->getColumn()]; } + if (std::distance(result.begin(), resultIt) == 2240 || std::distance(result.begin(), resultIt) == 2241 || std::distance(result.begin(), resultIt) == 8262 || std::distance(result.begin(), resultIt) == 8263 || std::distance(result.begin(), resultIt) == 8266 || std::distance(result.begin(), resultIt) == 8267) { + std::cout << "got initial value " << currentValue << " for state " << std::distance(result.begin(), resultIt) << " in row " << currentRow << std::endl; + } + + if (choices) { selectedChoice = 0; if (*choiceIt == 0) { @@ -1645,6 +1650,10 @@ namespace storm { for (auto elementIte = this->begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) { newValue += elementIt->getValue() * vector[elementIt->getColumn()]; } + + if (std::distance(result.begin(), resultIt) == 2240 || std::distance(result.begin(), resultIt) == 2241 || std::distance(result.begin(), resultIt) == 8262 || std::distance(result.begin(), resultIt) == 8263 || std::distance(result.begin(), resultIt) == 8266 || std::distance(result.begin(), resultIt) == 8267) { + std::cout << "got value " << currentValue << " for state " << std::distance(result.begin(), resultIt) << " in row " << currentRow << std::endl; + } if (choices && currentRow == *choiceIt + *rowGroupIt) { oldSelectedChoiceValue = newValue; @@ -1664,6 +1673,9 @@ namespace storm { // Finally write value to target vector. *resultIt = currentValue; if (choices && compare(currentValue, oldSelectedChoiceValue)) { + if (std::distance(result.begin(), resultIt) == 2240 || std::distance(result.begin(), resultIt) == 2241 || std::distance(result.begin(), resultIt) == 8262 || std::distance(result.begin(), resultIt) == 8263 || std::distance(result.begin(), resultIt) == 8266 || std::distance(result.begin(), resultIt) == 8267) { + std::cout << "changing choice in " << std::distance(result.begin(), resultIt) << " from " << *choiceIt << " to " << selectedChoice << " because " << currentValue << " is better than " << oldSelectedChoiceValue << std::endl; + } *choiceIt = selectedChoice; } } diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h index 9d83a0a49..069303c04 100644 --- a/src/storm/utility/constants.h +++ b/src/storm/utility/constants.h @@ -38,7 +38,7 @@ namespace storm { struct DoubleLess { bool operator()(double a, double b) const { - return b - a > 1e-18; + return b - a > 1e-17; } }; @@ -54,7 +54,7 @@ namespace storm { struct DoubleGreater { bool operator()(double a, double b) const { - return a - b > 1e-18; + return a - b > 1e-17; } };