From e78057256074e67bf8af3f9aabab9939f7fbdbe9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 28 May 2018 21:38:17 +0200 Subject: [PATCH] changing command decomposition of game-based abstraction and further debugging --- src/storm/abstraction/MenuGameRefiner.cpp | 4 + .../abstraction/prism/CommandAbstractor.cpp | 108 ++++++------------ .../abstraction/prism/CommandAbstractor.h | 14 +-- .../prism/PrismMenuGameAbstractor.cpp | 11 +- .../abstraction/GameBasedMdpModelChecker.cpp | 2 - 5 files changed, 52 insertions(+), 87 deletions(-) diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 84ac8e7af..a9db0f620 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -279,6 +279,10 @@ namespace storm { // Decode both choices to explicit mappings. std::map> lowerChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping(lowerChoice); std::map> upperChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping(upperChoice); + + lowerChoice.template toAdd().exportToDot("lower.dot"); + upperChoice.template toAdd().exportToDot("upper.dot"); + STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ")."); // First, sort updates according to probability mass. diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index 929285943..84fe80137 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -98,7 +98,7 @@ namespace storm { template void CommandAbstractor::recomputeCachedBddWithDecomposition() { - STORM_LOG_TRACE("Recomputing BDD for command " << command.get() << " using the decomposition."); + STORM_LOG_TRACE("Recomputing BDD for command with index " << command.get().getGlobalIndex() << " (" << command.get() << ") using the decomposition."); auto start = std::chrono::high_resolution_clock::now(); // compute a decomposition of the command @@ -205,18 +205,16 @@ namespace storm { relevantBlockPartition = std::move(cleanedRelevantBlockPartition); STORM_LOG_TRACE("Decomposition into " << relevantBlockPartition.size() << " blocks."); - for (auto const& block : relevantBlockPartition) { - STORM_LOG_TRACE("New block of size " << block.size() << ":"); - - std::set blockPredicateIndices; - for (auto const& innerBlock : block) { - blockPredicateIndices.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end()); - } - - for (auto const& predicateIndex : blockPredicateIndices) { - STORM_LOG_TRACE(abstractionInformation.get().getPredicateByIndex(predicateIndex)); - } - } +// for (auto const& block : relevantBlockPartition) { +// std::set blockPredicateIndices; +// for (auto const& innerBlock : block) { +// blockPredicateIndices.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end()); +// } +// +// for (auto const& predicateIndex : blockPredicateIndices) { +// STORM_LOG_TRACE(abstractionInformation.get().getPredicateByIndex(predicateIndex)); +// } +// } std::set variablesContainedInGuard = command.get().getGuardExpression().getVariables(); @@ -240,8 +238,6 @@ namespace storm { uint64_t numberOfSolutions = 0; uint64_t numberOfTotalSolutions = 0; - std::cout << localExpressionInformation << std::endl; - // If we need to enumerate the guard, do it only once now. if (enumerateAbstractGuard) { std::set relatedGuardPredicates = localExpressionInformation.getRelatedExpressions(variablesContainedInGuard); @@ -260,8 +256,6 @@ namespace storm { return true; }); STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions for abstract guard."); - abstractGuard.template toAdd().exportToDot("abstractguard" + std::to_string(command.get().getGlobalIndex()) + ".dot"); - // Now that we have the abstract guard, we can add it as an assertion to the solver before enumerating // the other solutions. @@ -301,9 +295,7 @@ namespace storm { std::vector transitionDecisionVariables; std::vector> sourceVariablesAndPredicates; for (auto const& element : relevantPredicatesAndVariables.first) { - std::cout << "1-querying " << abstractionInformation.get().getPredicateByIndex(element.second) << std::endl; if (relevantPredicates.find(element.second) != relevantPredicates.end()) { - std::cout << "1-is relevant!" << std::endl; transitionDecisionVariables.push_back(element.first); sourceVariablesAndPredicates.push_back(element); } @@ -314,14 +306,11 @@ namespace storm { destinationVariablesAndPredicates.emplace_back(); for (auto const& assignment : command.get().getUpdate(updateIndex).getAssignments()) { uint64_t assignmentVariableBlockIndex = localExpressionInformation.getBlockIndexOfVariable(assignment.getVariable()); - std::cout << "assignment variable " << assignment.getVariable().getName() << " block index: " << assignmentVariableBlockIndex << std::endl; if (block.find(assignmentVariableBlockIndex) != block.end()) { std::set const& assignmentVariableBlock = localExpressionInformation.getExpressionBlock(assignmentVariableBlockIndex); for (auto const& element : relevantPredicatesAndVariables.second[updateIndex]) { - std::cout << "2-querying " << abstractionInformation.get().getPredicateByIndex(element.second) << std::endl; if (assignmentVariableBlock.find(element.second) != assignmentVariableBlock.end()) { - std::cout << "2-is relevant!" << std::endl; destinationVariablesAndPredicates.back().push_back(element); transitionDecisionVariables.push_back(element.first); } @@ -350,7 +339,6 @@ namespace storm { // We now compute how many variables we need to encode the choices. We add one to the maximal number of // choices to account for a possible transition to a bottom state. uint_fast64_t numberOfVariablesNeeded = static_cast(std::ceil(std::log2(maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0)))); - std::cout << "need " << numberOfVariablesNeeded << " variables for " << (maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0)) << " choices" << std::endl; // Finally, build overall result. storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero(); @@ -365,7 +353,6 @@ namespace storm { storm::dd::Bdd allDistributions = this->getAbstractionInformation().getDdManager().getBddZero(); for (auto const& distribution : sourceDistributionsPair.second) { allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, usedNondeterminismVariables, usedNondeterminismVariables + numberOfVariablesNeeded); - distribution.template toAdd().exportToDot("dist" + std::to_string(distributionIndex) + ".dot"); ++distributionIndex; STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty."); } @@ -375,9 +362,6 @@ namespace storm { } usedNondeterminismVariables += numberOfVariablesNeeded; -// resultBdd.template toAdd().exportToDot("result.dot"); -// exit(-1); - blockBdds.push_back(resultBdd); ++blockCounter; } @@ -390,7 +374,6 @@ namespace storm { storm::dd::Bdd resultBdd = getAbstractionInformation().getDdManager().getBddOne(); uint64_t blockIndex = 0; for (auto const& blockBdd : blockBdds) { - blockBdd.template toAdd().exportToDot("block" + std::to_string(command.get().getGlobalIndex()) + "_" + std::to_string(blockIndex) + ".dot"); resultBdd &= blockBdd; ++blockIndex; } @@ -412,16 +395,9 @@ namespace storm { resultBdd &= abstractGuard; } - resultBdd.template toAdd().exportToDot("decomp" + std::to_string(command.get().getGlobalIndex()) + ".dot"); - - auto identities = computeMissingIdentities(); - identities.template toAdd().exportToDot("idents" + std::to_string(command.get().getGlobalIndex()) + ".dot"); - // multiply with missing identities resultBdd &= computeMissingIdentities(); - resultBdd.template toAdd().exportToDot("decomp_idents" + std::to_string(command.get().getGlobalIndex()) + ".dot"); - // cache and return result resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()); @@ -483,8 +459,6 @@ namespace storm { STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty."); } - resultBdd.template toAdd().exportToDot("nodecomp" + std::to_string(command.get().getGlobalIndex()) + ".dot"); - resultBdd &= computeMissingIdentities(); resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()); STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions."); @@ -504,12 +478,12 @@ namespace storm { std::set assignedVariables; for (auto const& assignment : assignments) { // Also, variables appearing on the right-hand side of an assignment are relevant for source state. - auto const& rightHandSidePredicates = localExpressionInformation.getRelatedExpressions(assignment.getExpression().getVariables()); + auto const& rightHandSidePredicates = localExpressionInformation.getExpressionsUsingVariables(assignment.getExpression().getVariables()); result.first.insert(rightHandSidePredicates.begin(), rightHandSidePredicates.end()); // Variables that are being assigned are relevant for the successor state. storm::expressions::Variable const& assignedVariable = assignment.getVariable(); - auto const& leftHandSidePredicates = localExpressionInformation.getRelatedExpressions(assignedVariable); + auto const& leftHandSidePredicates = localExpressionInformation.getExpressionsUsingVariable(assignedVariable); result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end()); // // Keep track of all assigned variables, so we can find the related predicates later. @@ -624,9 +598,7 @@ namespace storm { template storm::dd::Bdd CommandAbstractor::computeMissingIdentities() const { - storm::dd::Bdd identities = computeMissingGlobalIdentities(); - identities &= computeMissingUpdateIdentities(); - return identities; + return computeMissingUpdateIdentities(); } template @@ -639,51 +611,45 @@ namespace storm { auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end(); storm::dd::Bdd updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne(); - auto sourceRelevantIt = relevantPredicatesAndVariables.first.begin(); - auto sourceRelevantIte = relevantPredicatesAndVariables.first.end(); - // Go through all relevant source predicates. This is guaranteed to be a superset of the set of - // relevant successor predicates for any update. - for (; sourceRelevantIt != sourceRelevantIte; ++sourceRelevantIt) { - // If the predicates do not match, there is a predicate missing, so we need to add its identity. - if (updateRelevantIt == updateRelevantIte || sourceRelevantIt->second != updateRelevantIt->second) { - std::cout << "adding update identity of predicate " << this->getAbstractionInformation().getPredicateByIndex(sourceRelevantIt->second) << " to update " << updateIndex << std::endl; - updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second); + for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { + if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) { + updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); } else { ++updateRelevantIt; } } - + result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } return result; } - template - storm::dd::Bdd CommandAbstractor::computeMissingGlobalIdentities() const { - storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); - - auto relevantIt = relevantPredicatesAndVariables.first.begin(); - auto relevantIte = relevantPredicatesAndVariables.first.end(); - - for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { - if (relevantIt == relevantIte || relevantIt->second != predicateIndex) { - std::cout << "adding global identity of predicate " << this->getAbstractionInformation().getPredicateByIndex(predicateIndex) << std::endl; - result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); - } else { - ++relevantIt; - } - } - - return result; - } +// template +// storm::dd::Bdd CommandAbstractor::computeMissingGlobalIdentities() const { +// storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); +// +// auto relevantIt = relevantPredicatesAndVariables.first.begin(); +// auto relevantIte = relevantPredicatesAndVariables.first.end(); +// +// for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { +// if (relevantIt == relevantIte || relevantIt->second != predicateIndex) { +// std::cout << "adding global identity of predicate " << this->getAbstractionInformation().getPredicateByIndex(predicateIndex) << std::endl; +// result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); +// } else { +// ++relevantIt; +// } +// } +// +// return result; +// } template GameBddResult CommandAbstractor::abstract() { if (forceRecomputation) { this->recomputeCachedBdd(); } else { - cachedDd.bdd &= computeMissingGlobalIdentities(); + cachedDd.bdd &= computeMissingUpdateIdentities(); } STORM_LOG_TRACE("Command produces " << cachedDd.bdd.getNonZeroCount() << " transitions."); diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index cb6146e73..9b911c8f5 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -213,13 +213,13 @@ namespace storm { */ AbstractionInformation& getAbstractionInformation(); - /*! - * Computes the globally missing state identities. - * - * @return A BDD that represents the global state identities for predicates that are irrelevant for the - * source and successor states. - */ - storm::dd::Bdd computeMissingGlobalIdentities() const; +// /*! +// * Computes the globally missing state identities. +// * +// * @return A BDD that represents the global state identities for predicates that are irrelevant for the +// * source and successor states. +// */ +// storm::dd::Bdd computeMissingGlobalIdentities() const; // An SMT responsible for this abstract command. std::unique_ptr smtSolver; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index d9cbdd46e..661aeca57 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -172,20 +172,17 @@ namespace storm { } relevantStatesWatch.stop(); + storm::dd::Bdd validBlocks = validBlockAbstractor.getValidBlocks(); + // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract); storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); if (program.get().hasInitialConstruct()) { - initialStates &= validBlockAbstractor.getValidBlocks(); + initialStates &= validBlocks; } initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); - - transitionRelation.template toAdd().exportToDot("transrel.dot"); - (initialStates && transitionRelation).template toAdd().exportToDot("transrelinit.dot"); - (transitionRelation && abstractionInformation.encodePlayer1Choice(6, this->getAbstractionInformation().getPlayer1VariableCount())).template toAdd().exportToDot("trans6.dot"); - - initialStates.template toAdd().exportToDot("initial.dot"); + reachableStates &= validBlocks; relevantStatesWatch.start(); if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) { diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index c79a423d3..588040ce9 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -573,8 +573,6 @@ namespace storm { targetStates |= game.getBottomStates(); } - exit(-1); - // #ifdef LOCAL_DEBUG // initialStates.template toAdd().exportToDot("init" + std::to_string(iteration) + ".dot"); // targetStates.template toAdd().exportToDot("target" + std::to_string(iteration) + ".dot");