diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 0d30b5075..802ee6949 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -38,6 +38,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/utility/prism.h" #include "storm/utility/macros.h" @@ -475,24 +476,40 @@ namespace storm { uint64_t maybeStatePosition = 0; previousPlayer2States = 0; for (auto state : maybeStates) { + if (state == 25305 || state == 67442 || state == 67440) { + std::cout << "dealing with problematic state " << state << " whose local offset is " << maybeStatePosition << std::endl; + } uint64_t chosenPlayer2State = startingStrategyPair->getPlayer1Strategy().getChoice(state); - uint64_t previousPlayer2StatesForState = 0; + uint64_t previousPlayer2MaybeStatesForState = 0; for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { if (player2MaybeStates.get(player2State)) { + if (state == 25305 || state == 67442 || state == 67440) { + std::cout << "player 2 state " << player2State << " is a player 2 maybe state with local index " << previousPlayer2States << std::endl; + } + if (player2State == chosenPlayer2State) { - player1Scheduler[maybeStatePosition] = previousPlayer2StatesForState; + player1Scheduler[maybeStatePosition] = previousPlayer2MaybeStatesForState; + if (state == 25305 || state == 67442 || state == 67440) { + std::cout << "player 1 scheduler chooses " << previousPlayer2MaybeStatesForState << " which globally is " << player2State << std::endl; + } } - // Copy over the player 2 action (modulo making it local) as all rows for the state are taken. + // Copy over the player 2 action (modulo making it local) as all rows for the player 2 state are taken. if (startingStrategyPair->getPlayer2Strategy().hasDefinedChoice(player2State)) { player2Scheduler[previousPlayer2States] = startingStrategyPair->getPlayer2Strategy().getChoice(player2State) - transitionMatrix.getRowGroupIndices() [player2State]; + if (state == 25305 || state == 67442 || state == 67440) { + std::cout << "copied over choice " << player2Scheduler[previousPlayer2States] << " for player 2 (global index " << startingStrategyPair->getPlayer2Strategy().getChoice(player2State) << ")" << std::endl; + } } else { player2Scheduler[previousPlayer2States] = 0; + if (state == 25305 || state == 67442 || state == 67440) { + std::cout << "did not copy (undefined) choice for player 2 (global index " << startingStrategyPair->getPlayer2Strategy().getChoice(player2State) << ")" << std::endl; + } } - ++previousPlayer2StatesForState; + ++previousPlayer2MaybeStatesForState; ++previousPlayer2States; } } @@ -502,8 +519,14 @@ namespace storm { } // Solve actual game and track schedulers. + if (player1Scheduler.size() > 4713) { + std::cout << "before: player1Scheduler[4713] = " << player1Scheduler[4713] << std::endl; + } gameSolver->solveGame(env, player1Direction, player2Direction, values, b, &player1Scheduler, &player2Scheduler); - + if (player1Scheduler.size() > 67440) { + std::cout << "after: player1Scheduler[4713] = " << player1Scheduler[4713] << std::endl; + } + // Set values according to quantitative result (qualitative result has already been taken care of). storm::utility::vector::setVectorValues(result.getValues(), maybeStates, values); @@ -511,16 +534,16 @@ namespace storm { uint64_t previousPlayer1MaybeStates = 0; uint64_t previousPlayer2MaybeStates = 0; for (auto state : maybeStates) { - uint64_t previousPlayer2StatesForState = 0; + uint64_t previousPlayer2MaybeStatesForState = 0; for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { - if (player1Scheduler[previousPlayer1MaybeStates] == previousPlayer2StatesForState) { + if (player1Scheduler[previousPlayer1MaybeStates] == previousPlayer2MaybeStatesForState) { strategyPair.getPlayer1Strategy().setChoice(state, player2State); } if (player2MaybeStates.get(player2State)) { strategyPair.getPlayer2Strategy().setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State] + player2Scheduler[previousPlayer2MaybeStates]); - ++previousPlayer2StatesForState; + ++previousPlayer2MaybeStatesForState; ++previousPlayer2MaybeStates; } } @@ -895,6 +918,8 @@ namespace storm { } if (sanityCheck) { + storm::utility::ConstantsComparator sanityComparator(1e-6, true); + ///////// 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); @@ -913,9 +938,21 @@ namespace storm { auto dtmcMatrix = dtmcMatrixBuilder.build(); std::vector sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(Environment(), storm::solver::SolveGoal(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false); + ValueType maxDiff = storm::utility::zero(); + uint64_t maxState = 0; for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]) < 1e-4, "Got weird min divergences!"); + ValueType const& diff = std::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]); + if (diff > maxDiff) { + maxState = state; + maxDiff = diff; + } } + 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)) { + exit(-1); + } + ///////// 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); @@ -926,16 +963,68 @@ namespace storm { STORM_LOG_ASSERT(maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected max player 1 choice in state " << state << "."); STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(maxStrategyPair.getPlayer1Strategy().getChoice(state)), "Expected max player 2 choice in state " << state << " with player 2 choice " << maxStrategyPair.getPlayer1Strategy().getChoice(state) << "."); uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxStrategyPair.getPlayer1Strategy().getChoice(state)); + for (auto const& entry : transitionMatrix.getRow(player2Choice)) { dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue()); + if (state == 25305) { + std::cout << "entry " << entry.getColumn() << " -> " << entry.getValue() << std::endl; + std::cout << "values [" << quantitativeResult.getMin().getValues()[entry.getColumn()] << ", " << quantitativeResult.getMax().getValues()[entry.getColumn()] << "]" << std::endl; + } } } } dtmcMatrix = dtmcMatrixBuilder.build(); sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(Environment(), storm::solver::SolveGoal(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false); + maxDiff = storm::utility::zero(); + maxState = 0; for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - STORM_LOG_ASSERT(std::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]) < 1e-4, "Got weird max divergences!"); + ValueType const& diff = std::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]); + if (diff > maxDiff) { + maxState = state; + maxDiff = diff; + } + + if (dtmcMatrix.getRowCount() > 25305 && !targetStates.get(state)) { + uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxStrategyPair.getPlayer1Strategy().getChoice(state)); + for (auto const& entry : transitionMatrix.getRow(player2Choice)) { + if (state == 25305) { + std::cout << "entry " << entry.getColumn() << " -> " << entry.getValue() << std::endl; + std::cout << "sanity value " << sanityValues[entry.getColumn()] << std::endl; + } + } + } + } + STORM_LOG_TRACE("Got maximal deviation of " << maxDiff << "."); + STORM_LOG_WARN_COND(sanityComparator.isZero(maxDiff), "Deviation " << maxDiff << " between computed value (" << quantitativeResult.getMax().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)) { + // 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 << std::endl; + uint64_t player2State = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); + std::cout << "going to player 2 state " << player2State << std::endl; + uint64_t player2Choice = maxStrategyPair.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); + } + } + } + } + + exit(-1); } } } diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index c6b51b981..9f9abd952 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -693,7 +693,7 @@ namespace storm { * * @param useGroups If set to true, the constraint for the rows is interpreted as selecting whole row groups. * If it is not set, the row constraint is interpreted over the actual rows. Note that empty row groups will - * be dropped altogether. That is, if no row of a row group is selected *or* the row group is alread empty, + * be dropped altogether. That is, if no row of a row group is selected *or* the row group is already empty, * the submatrix will not have this row group. * @param constraint A bit vector indicating which rows to keep. * @param columnConstraint A bit vector indicating which columns to keep. diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 56494dc03..8b7301e72 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -725,6 +725,10 @@ namespace storm { } if (choices && f(*targetIt, oldSelectedChoiceValue)) { + uint64_t distance = std::distance(target.begin(), targetIt); + if (distance == 1693 || distance == 4715 || distance == 4713) { + std::cout << "improving value at " << distance << ": moving from " << *choiceIt << " to " << selectedChoice << " because " << *targetIt << " is better than " << oldSelectedChoiceValue << std::endl; + } *choiceIt = selectedChoice; } } else { @@ -792,7 +796,8 @@ namespace storm { */ template void reduceVectorMinOrMax(storm::solver::OptimizationDirection dir, std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { - if(dir == storm::solver::OptimizationDirection::Minimize) { + std::cout << "[" << dir << "]: reducing vector " << std::endl; + if (dir == storm::solver::OptimizationDirection::Minimize) { reduceVectorMin(source, target, rowGrouping, choices); } else { reduceVectorMax(source, target, rowGrouping, choices);