diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index df26fa29b..2cd938941 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -20,6 +20,8 @@ #include "storm-config.h" #include "src/adapters/CarlAdapter.h" +//#define LOCAL_DEBUG + namespace storm { namespace abstraction { namespace prism { @@ -122,18 +124,28 @@ namespace storm { for (auto const& successorValuePair : lowerChoiceAsAdd) { uint_fast64_t updateIndex = abstractionInformation.decodeAux(successorValuePair.first, 0, currentGame->getProbabilisticBranchingVariables().size()); +#ifdef LOCAL_DEBUG std::cout << "update idx: " << updateIndex << std::endl; +#endif storm::storage::BitVector successor(abstractionInformation.getNumberOfPredicates()); for (uint_fast64_t index = 0; index < abstractionInformation.getOrderedSuccessorVariables().size(); ++index) { auto const& successorVariable = abstractionInformation.getOrderedSuccessorVariables()[index]; +#ifdef LOCAL_DEBUG std::cout << successorVariable.getName() << " has value"; +#endif if (successorValuePair.first.getBooleanValue(successorVariable)) { successor.set(index); +#ifdef LOCAL_DEBUG std::cout << " true"; +#endif } else { +#ifdef LOCAL_DEBUG std::cout << " false"; +#endif } +#ifdef LOCAL_DEBUG std::cout << std::endl; +#endif } result[updateIndex] = successor; @@ -147,12 +159,16 @@ namespace storm { storm::dd::Add player1ChoiceAsAdd = player1Choice.template toAdd(); auto pl1It = player1ChoiceAsAdd.begin(); uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); +#ifdef LOCAL_DEBUG std::cout << "command index " << commandIndex << std::endl; std::cout << program.get() << std::endl; +#endif storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand(); +#ifdef LOCAL_DEBUG player1Choice.template toAdd().exportToDot("pl1choice_ref.dot"); std::cout << concreteCommand << std::endl; +#endif // Check whether there are bottom states in the game and whether one of the choices actually picks the // bottom state as the successor. @@ -172,16 +188,23 @@ namespace storm { } else { STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); +#ifdef LOCAL_DEBUG lowerChoice.template toAdd().exportToDot("lowerchoice_ref.dot"); upperChoice.template toAdd().exportToDot("upperchoice_ref.dot"); +#endif // Decode both choices to explicit mappings. +#ifdef LOCAL_DEBUG std::cout << "lower" << std::endl; +#endif std::map lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice); +#ifdef LOCAL_DEBUG std::cout << "upper" << std::endl; +#endif std::map upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice); STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ")."); +#ifdef LOCAL_DEBUG std::cout << "lower" << std::endl; for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) { std::cout << entry.first << " -> " << entry.second << std::endl; @@ -190,6 +213,7 @@ namespace storm { for (auto const& entry : upperChoiceUpdateToSuccessorMapping) { std::cout << entry.first << " -> " << entry.second << std::endl; } +#endif // Now go through the mappings and find points of deviation. Currently, we take the first deviation. storm::expressions::Expression newPredicate; @@ -199,7 +223,9 @@ namespace storm { for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) { STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch."); uint_fast64_t updateIndex = lowerIt->first; +#ifdef LOCAL_DEBUG std::cout << "update idx " << updateIndex << std::endl; +#endif bool deviates = lowerIt->second != upperIt->second; if (deviates) { for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) { diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 61c5da10f..c8fd9e3bb 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -28,6 +28,8 @@ #include "src/modelchecker/results/CheckResult.h" +//#define LOCAL_DEBUG + namespace storm { namespace modelchecker { namespace detail { @@ -337,7 +339,7 @@ namespace storm { // // minResult.exportToDot("minresult.dot"); // maxResult.exportToDot("maxresult.dot"); - pivotState.template toAdd().exportToDot("pivot.dot"); +// pivotState.template toAdd().exportToDot("pivot.dot"); // pivotStateLower.exportToDot("pivot_lower.dot"); // pivotStateUpper.exportToDot("pivot_upper.dot"); // pivotStateIsMinProb0.template toAdd().exportToDot("pivot_is_minprob0.dot"); @@ -362,10 +364,12 @@ namespace storm { storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); // lowerChoice2.template toAdd().exportToDot("tmp_lower.dot"); // lowerChoice2 = lowerChoice2.existsAbstract(variablesToAbstract); - + +#ifdef LOCAL_DEBUG lowerChoice.template toAdd().exportToDot("ref_lower.dot"); lowerChoice1.template toAdd().exportToDot("ref_lower1.dot"); lowerChoice2.template toAdd().exportToDot("ref_lower2.dot"); +#endif bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); if (lowerChoicesDifferent) { @@ -475,16 +479,16 @@ namespace storm { targetStates |= game.getBottomStates(); } - abstractor.exportToDot("game" + std::to_string(iterations) + ".dot"); +#ifdef LOCAL_DEBUG + abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); +#endif prob01.min = computeProb01States(player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, game.getInitialStates(), prob01.min.first.getPlayer1States(), prob01.min.second.getPlayer1States()); if (result) { return result; } - /*if (iterations == 18) { - exit(-1); - }*/ + prob01.max = computeProb01States(player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, game.getInitialStates(), prob01.max.first.getPlayer1States(), prob01.max.second.getPlayer1States()); if (result) { @@ -608,10 +612,12 @@ namespace storm { //std::cout << "diff one? " << ((commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy)) << std::endl; STORM_LOG_ASSERT((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy) || (commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy), "The strategies fully coincide."); +#ifdef LOCAL_DEBUG abstractor.exportToDot("lowerlower" + std::to_string(iterations) + ".dot", targetStates, minMaybeStateResult.player1Strategy && minMaybeStateResult.player2Strategy); abstractor.exportToDot("upperupper" + std::to_string(iterations) + ".dot", targetStates, maxMaybeStateResult.player1Strategy && maxMaybeStateResult.player2Strategy); abstractor.exportToDot("common" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && minMaybeStateResult.player2Strategy && maxMaybeStateResult.player2Strategy); abstractor.exportToDot("both" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy)); +#endif refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd); } @@ -657,6 +663,5 @@ namespace storm { template class GameBasedMdpModelChecker>; template class GameBasedMdpModelChecker>; template class GameBasedMdpModelChecker>; - } }