diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index f8209ee99..6a1dd8cdc 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -394,11 +394,8 @@ namespace storm { // Derive predicates from lower choice. storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; - lowerChoice.template toAdd().exportToDot("lower.dot"); storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); - lowerChoice1.template toAdd().exportToDot("lower1.dot"); storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - lowerChoice2.template toAdd().exportToDot("lower2.dot"); bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero() && !lowerChoice1.isZero() && !lowerChoice2.isZero(); if (lowerChoicesDifferent) { @@ -610,7 +607,7 @@ namespace storm { // Add variable update expression. predicates.back().emplace_back(allVariableUpdateExpression); - + // Add the guard of the choice. predicates.back().emplace_back(abstractor.get().getGuard(currentAction).changeManager(expressionManager).substitute(substitution)); @@ -649,14 +646,14 @@ namespace storm { for (auto const& predicate : step) { interpolatingSolver.add(predicate); } - ++stepCounter; - storm::solver::SmtSolver::CheckResult result = interpolatingSolver.check(); // If the result already became unsatisfiable if (result == storm::solver::SmtSolver::CheckResult::Unsat) { - STORM_LOG_TRACE("Trace formula became unsatisfiable after step " << (stepCounter - 1) << "."); + STORM_LOG_TRACE("Trace formula became unsatisfiable after step " << stepCounter << "."); break; } + + ++stepCounter; } // Now encode the trace as an SMT problem. @@ -666,14 +663,14 @@ namespace storm { std::vector interpolants; std::vector prefix; - for (uint64_t step = 0; step + 1 < stepCounter; ++step) { + for (uint64_t step = 0; step < stepCounter; ++step) { prefix.push_back(step); storm::expressions::Expression interpolant = interpolatingSolver.getInterpolant(prefix).substitute(variableSubstitution).changeManager(abstractionInformation.getExpressionManager()); if (!interpolant.isTrue() && !interpolant.isFalse()) { STORM_LOG_DEBUG("Derived new predicate (based on interpolation): " << interpolant); interpolants.push_back(interpolant); } else { - STORM_LOG_TRACE("Found interpolant is '" << interpolant << "'."); + STORM_LOG_ASSERT(false, "The found interpolant is '" << interpolant << "', which shouldn't happen."); } } return boost::make_optional(RefinementPredicates(RefinementPredicates::Source::Interpolation, interpolants)); @@ -843,6 +840,7 @@ namespace storm { bool considerDeviation = (pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::NearestMaximalDeviation || pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) && lowerValues && upperValues; bool foundPivotState = false; ValueType pivotStateDeviation = storm::utility::zero(); + auto const& player2Grouping = transitionMatrix.getRowGroupIndices(); while (!dijkstraQueue.empty()) { auto distanceStatePair = *dijkstraQueue.begin(); @@ -875,8 +873,7 @@ 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) { @@ -905,7 +902,8 @@ namespace storm { if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { uint64_t minPlayer2Successor = minStrategyPair.getPlayer1Strategy().getChoice(currentState); uint64_t minPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minPlayer2Successor); - + STORM_LOG_ASSERT(player2Grouping[minPlayer2Successor] <= minPlayer2Choice && minPlayer2Choice < player2Grouping[minPlayer2Successor + 1], "Illegal choice for player 2."); + for (auto const& entry : transitionMatrix.getRow(minPlayer2Choice)) { uint64_t player1Successor = entry.getColumn(); if (!relevantStates.get(player1Successor)) { @@ -925,7 +923,8 @@ namespace storm { if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { uint64_t maxPlayer2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); uint64_t maxPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxPlayer2Successor); - + STORM_LOG_ASSERT(player2Grouping[maxPlayer2Successor] <= maxPlayer2Choice && maxPlayer2Choice < player2Grouping[maxPlayer2Successor + 1], "Illegal choice for player 2."); + for (auto const& entry : transitionMatrix.getRow(maxPlayer2Choice)) { uint64_t player1Successor = entry.getColumn(); if (!relevantStates.get(player1Successor)) { @@ -936,7 +935,7 @@ namespace storm { if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) { distances[player1Successor] = alternateDistance; if (generatePredecessors) { - result.predecessors[player1Successor] = std::make_pair(currentState, maxPlayer2Successor); + result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[maxPlayer2Successor]); } dijkstraQueue.emplace(alternateDistance, player1Successor); } @@ -977,7 +976,8 @@ namespace storm { storm::dd::Bdd maxPlayer2Strategy = game.getManager().getBddZero(); if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(pivotState)) { uint64_t player2State = minStrategyPair.getPlayer1Strategy().getChoice(pivotState); - minPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[transitionMatrix.getRowGroupIndices()[player2State]], abstractionInformation.getPlayer1VariableCount()); + STORM_LOG_ASSERT(player1Grouping[pivotState] <= player2State && player2State < player1Grouping[pivotState + 1], "Illegal choice for player 1."); + minPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[player2State], abstractionInformation.getPlayer1VariableCount()); if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) { uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State); @@ -990,7 +990,8 @@ namespace storm { } if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(pivotState)) { uint64_t player2State = maxStrategyPair.getPlayer1Strategy().getChoice(pivotState); - maxPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[transitionMatrix.getRowGroupIndices()[player2State]], abstractionInformation.getPlayer1VariableCount()); + STORM_LOG_ASSERT(player1Grouping[pivotState] <= player2State && player2State < player1Grouping[pivotState + 1], "Illegal choice for player 1."); + maxPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[player2State], abstractionInformation.getPlayer1VariableCount()); if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) { uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State); @@ -1001,6 +1002,11 @@ namespace storm { maxPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size()); } } +// symbolicPivotState.template toAdd().exportToDot("pivot.dot"); +// minPlayer1Strategy.template toAdd().exportToDot("minpl1.dot"); +// minPlayer2Strategy.template toAdd().exportToDot("minpl2.dot"); +// maxPlayer1Strategy.template toAdd().exportToDot("maxpl1.dot"); +// maxPlayer2Strategy.template toAdd().exportToDot("maxpl2.dot"); boost::optional predicates; if (useInterpolation) { predicates = derivePredicatesFromInterpolation(game, pivotStateResult, odd); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 35d838d55..eeaffd6c3 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -689,6 +689,14 @@ namespace storm { player1Groups[player1State + 1] = player2State; } + // Lift the player 1 labeling from rows to row groups (player 2 states). + for (uint64_t player1State = 0; player1State < player1Groups.size() - 1; ++player1State) { + for (uint64_t player2State = player1Groups[player1State]; player2State < player1Groups[player1State + 1]; ++player2State) { + player1Labeling[player2State] = player1Labeling[player2RowGrouping[player2State]]; + } + } + player1Labeling.resize(player2RowGrouping.size() - 1); + // Create explicit representations of important state sets. storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd); storm::storage::BitVector constraintStates = constraintStatesBdd.toVector(odd);