From b9688346cce06ecb912bed02cae1d291a584ac4f Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 14 Dec 2016 16:27:22 +0100 Subject: [PATCH] command decomposition working. fixed some bugs, possibly introduced more, currently debugging --- .../abstraction/AbstractionInformation.cpp | 4 +- .../abstraction/AbstractionInformation.h | 3 +- src/storm/abstraction/MenuGameRefiner.cpp | 14 ++ src/storm/abstraction/jani/EdgeAbstractor.cpp | 4 +- .../jani/JaniMenuGameAbstractor.cpp | 2 +- .../abstraction/prism/CommandAbstractor.cpp | 200 +++++++++++++++--- .../abstraction/prism/CommandAbstractor.h | 6 +- .../abstraction/prism/ModuleAbstractor.cpp | 4 +- .../abstraction/prism/ModuleAbstractor.h | 4 +- .../prism/PrismMenuGameAbstractor.cpp | 5 +- .../abstraction/GameBasedMdpModelChecker.cpp | 8 +- .../settings/modules/AbstractionSettings.cpp | 6 + .../settings/modules/AbstractionSettings.h | 8 + 13 files changed, 219 insertions(+), 49 deletions(-) diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 30c55500a..2fc5446ea 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -209,8 +209,8 @@ namespace storm { } template - storm::dd::Bdd AbstractionInformation::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const { - return encodeChoice(index, 0, end, player2VariableBdds); + storm::dd::Bdd AbstractionInformation::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const { + return encodeChoice(index, start, end, player2VariableBdds); } template diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index 4cca4b329..b0336afe5 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -214,10 +214,11 @@ namespace storm { * Encodes the given index using the indicated player 2 variables. * * @param index The index to encode. + * @param start The index of the first variable of the range that is used to encode the index. * @param end The index of the variable past the end of the range that is used to encode the index. * @return The index encoded as a BDD. */ - storm::dd::Bdd encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const; + storm::dd::Bdd encodePlayer2Choice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const; /*! * Decodes the player 2 choice in the given valuation. diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index aa262e4e0..f0d02ea81 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -379,6 +379,14 @@ namespace storm { bool player1ChoicesDifferent = !(pivotState && minPlayer1Strategy).exclusiveOr(pivotState && maxPlayer1Strategy).isZero(); + pivotState.template toAdd().exportToDot("pivot.dot"); + + minPlayer1Strategy.template toAdd().exportToDot("minpl1.dot"); + maxPlayer1Strategy.template toAdd().exportToDot("maxpl1.dot"); + + (pivotState && minPlayer1Strategy).template toAdd().exportToDot("minpivot.dot"); + (pivotState && maxPlayer1Strategy).template toAdd().exportToDot("maxpivot.dot"); + boost::optional predicates; // Derive predicates from lower choice. @@ -386,6 +394,9 @@ namespace storm { storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); + lowerChoice1.template toAdd().exportToDot("lower1.dot"); + lowerChoice2.template toAdd().exportToDot("lower2.dot"); + bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); if (lowerChoicesDifferent) { STORM_LOG_TRACE("Deriving predicate based on lower choice."); @@ -400,6 +411,9 @@ namespace storm { storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); storm::dd::Bdd upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); + + upperChoice1.template toAdd().exportToDot("upper1.dot"); + upperChoice2.template toAdd().exportToDot("upper2.dot"); bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); if (upperChoicesDifferent) { diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index fadaef4a2..ec1eae2ab 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -112,7 +112,7 @@ namespace storm { uint_fast64_t distributionIndex = 1; storm::dd::Bdd allDistributions = this->getAbstractionInformation().getDdManager().getBddZero(); for (auto const& distribution : sourceDistributionsPair.second) { - allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, numberOfVariablesNeeded); + allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, 0, numberOfVariablesNeeded); ++distributionIndex; STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty."); } @@ -375,7 +375,7 @@ namespace storm { result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false); // Add the edge encoding and the next free player 2 encoding. - result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(0, numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); + result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(0, 0,numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); return result; } diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 47f644159..845465a7e 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -165,7 +165,7 @@ namespace storm { // If there are deadlock states, we fix them now. storm::dd::Add deadlockTransitions = abstractionInformation.getDdManager().template getAddZero(); if (!deadlockStates.isZero()) { - deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); + deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, 0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); } // Compute bottom states and the appropriate transitions if necessary. diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index 7198b2f2b..89829f41b 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -23,7 +23,7 @@ namespace storm { namespace abstraction { namespace prism { template - CommandAbstractor::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allowInvalidSuccessors) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), allowInvalidSuccessors(allowInvalidSuccessors), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory) { + CommandAbstractor::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allowInvalidSuccessors, bool useDecomposition) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), allowInvalidSuccessors(allowInvalidSuccessors), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -92,7 +92,7 @@ namespace storm { allRelevantBlocks.insert(rhsVariableBlocks.begin(), rhsVariableBlocks.end()); } } - STORM_LOG_TRACE("Found " << allRelevantBlocks.size() << " relevant block."); + STORM_LOG_TRACE("Found " << allRelevantBlocks.size() << " relevant block(s)."); // Create a block partition. std::vector> relevantBlockPartition; @@ -174,61 +174,187 @@ namespace storm { STORM_LOG_TRACE("Relevant block partition size is one, falling back to regular computation."); recomputeCachedBdd(); } else { - // otherwise, enumerate the abstract guard so we do this only once - std::set relatedGuardPredicates = localExpressionInformation.getRelatedExpressions(command.get().getGuardExpression().getVariables()); - std::vector guardDecisionVariables; - std::vector> guardVariablesAndPredicates; - for (auto const& element : relevantPredicatesAndVariables.first) { - if (relatedGuardPredicates.find(element.second) != relatedGuardPredicates.end()) { - guardDecisionVariables.push_back(element.first); - guardVariablesAndPredicates.push_back(element); + std::set variablesContainedInGuard = command.get().getGuardExpression().getVariables(); + + // Check whether we need to enumerate the guard. This is the case if the blocks related by the guard + // are not contained within a single block of our decomposition. + bool enumerateAbstractGuard = true; + std::set guardBlocks = localExpressionInformation.getBlockIndicesOfVariables(variablesContainedInGuard); + for (auto const& block : relevantBlockPartition) { + bool allContained = true; + for (auto const& guardBlock : guardBlocks) { + if (block.find(guardBlock) == block.end()) { + allContained = false; + break; + } + } + if (allContained) { + enumerateAbstractGuard = false; } } + uint64_t numberOfSolutions = 0; - abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero(); - smtSolver->allSat(decisionVariables, [this,&guardVariablesAndPredicates,&numberOfSolutions] (storm::solver::SmtSolver::ModelReference const& model) { - abstractGuard |= getSourceStateBdd(model, guardVariablesAndPredicates); - ++numberOfSolutions; - return true; - }); - STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " for abstract guard."); + + if (enumerateAbstractGuard) { + // otherwise, enumerate the abstract guard so we do this only once + std::set relatedGuardPredicates = localExpressionInformation.getRelatedExpressions(variablesContainedInGuard); + std::vector guardDecisionVariables; + std::vector> guardVariablesAndPredicates; + for (auto const& element : relevantPredicatesAndVariables.first) { + if (relatedGuardPredicates.find(element.second) != relatedGuardPredicates.end()) { + guardDecisionVariables.push_back(element.first); + guardVariablesAndPredicates.push_back(element); + } + } + abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero(); + smtSolver->allSat(guardDecisionVariables, [this,&guardVariablesAndPredicates,&numberOfSolutions] (storm::solver::SmtSolver::ModelReference const& model) { + abstractGuard |= getSourceStateBdd(model, guardVariablesAndPredicates); + ++numberOfSolutions; + return true; + }); + STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " for abstract guard."); + + // now that we have the abstract guard, we can add it as an assertion to the solver before enumerating + // the other solutions. + + // Create a new backtracking point before adding the guard. + smtSolver->push(); + + // Create the guard constraint. + std::pair, std::unordered_map> result = abstractGuard.toExpression(this->getAbstractionInformation().getExpressionManager()); + + // Then add it to the solver. + for (auto const& expression : result.first) { + smtSolver->add(expression); + } + + // Finally associate the level variables with the predicates. + for (auto const& indexVariablePair : result.second) { + smtSolver->add(storm::expressions::iff(indexVariablePair.second, this->getAbstractionInformation().getPredicateForDdVariableIndex(indexVariablePair.first))); + } + } // then enumerate the solutions for each of the blocks of the decomposition + uint64_t usedNondeterminismVariables = 0; + uint64_t blockCounter = 0; + std::vector> blockBdds; for (auto const& block : relevantBlockPartition) { std::set relevantPredicates; for (auto const& innerBlock : block) { relevantPredicates.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end()); } - std::vector decisionVariables; - std::vector>> variablesAndPredicates; + std::vector transitionDecisionVariables; + std::vector> sourceVariablesAndPredicates; + for (auto const& element : relevantPredicatesAndVariables.first) { + if (relevantPredicates.find(element.second) != relevantPredicates.end()) { + transitionDecisionVariables.push_back(element.first); + sourceVariablesAndPredicates.push_back(element); + } + } + + std::vector>> destinationVariablesAndPredicates; for (uint64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { - variablesAndPredicates.emplace_back(); - for (auto const& element : relevantPredicatesAndVariables.second[updateIndex]) { - if (relevantPredicates.find(element.second) != relevantPredicates.end()) { - decisionVariables.push_back(element.first); - variablesAndPredicates.back().push_back(element); + destinationVariablesAndPredicates.emplace_back(); + for (auto const& assignment : command.get().getUpdate(updateIndex).getAssignments()) { + uint64_t assignmentVariableBlockIndex = localExpressionInformation.getBlockIndexOfVariable(assignment.getVariable()); + std::set const& assignmentVariableBlock = localExpressionInformation.getExpressionBlock(assignmentVariableBlockIndex); + if (block.find(assignmentVariableBlockIndex) != block.end()) { + for (auto const& element : relevantPredicatesAndVariables.second[updateIndex]) { + if (assignmentVariableBlock.find(element.second) != assignmentVariableBlock.end()) { + destinationVariablesAndPredicates.back().push_back(element); + transitionDecisionVariables.push_back(element.first); + } + } } } } std::unordered_map, std::vector>> sourceToDistributionsMap; numberOfSolutions = 0; - smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&numberOfSolutions] (storm::solver::SmtSolver::ModelReference const& model) { - sourceToDistributionsMap[getSourceStateBdd(model, relevantPredicatesAndVariables.first)].push_back(getDistributionBdd(model, relevantPredicatesAndVariables.second)); + smtSolver->allSat(transitionDecisionVariables, [&sourceToDistributionsMap,this,&numberOfSolutions,&sourceVariablesAndPredicates,&destinationVariablesAndPredicates] (storm::solver::SmtSolver::ModelReference const& model) { + sourceToDistributionsMap[getSourceStateBdd(model, sourceVariablesAndPredicates)].push_back(getDistributionBdd(model, destinationVariablesAndPredicates)); ++numberOfSolutions; return true; }); + STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions for block " << blockCounter << "."); + numberOfSolutions = 0; + + // Now we search for the maximal number of choices of player 2 to determine how many DD variables we + // need to encode the nondeterminism. + uint_fast64_t maximalNumberOfChoices = 0; + for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { + maximalNumberOfChoices = std::max(maximalNumberOfChoices, static_cast(sourceDistributionsPair.second.size())); + } + + // 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 + 1))); + + // Finally, build overall result. + storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero(); + + uint_fast64_t sourceStateIndex = 0; + for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { + STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty."); + STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty."); + // We start with the distribution index of 1, becase 0 is reserved for a potential bottom choice. + uint_fast64_t distributionIndex = 1; + storm::dd::Bdd allDistributions = this->getAbstractionInformation().getDdManager().getBddZero(); + for (auto const& distribution : sourceDistributionsPair.second) { + allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, usedNondeterminismVariables, usedNondeterminismVariables + numberOfVariablesNeeded); + ++distributionIndex; + STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty."); + } + resultBdd |= sourceDistributionsPair.first && allDistributions; + ++sourceStateIndex; + STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty."); + } + usedNondeterminismVariables += numberOfVariablesNeeded; + + blockBdds.push_back(resultBdd); + ++blockCounter; } + smtSolver->pop(); + // multiply the results + storm::dd::Bdd resultBdd = getAbstractionInformation().getDdManager().getBddOne(); + for (auto const& blockBdd : blockBdds) { + resultBdd &= blockBdd; + } - // multiply with the abstract guard + // if we did not explicitly enumerate the guard, we can construct it from the result BDD. + if (!enumerateAbstractGuard) { + std::set allVariables(getAbstractionInformation().getSuccessorVariables()); + auto player2Variables = getAbstractionInformation().getPlayer2VariableSet(usedNondeterminismVariables); + allVariables.insert(player2Variables.begin(), player2Variables.end()); + auto auxVariables = getAbstractionInformation().getAuxVariableSet(0, getAbstractionInformation().getAuxVariableCount()); + allVariables.insert(auxVariables.begin(), auxVariables.end()); + + std::set variablesToAbstract; + std::set_intersection(allVariables.begin(), allVariables.end(), resultBdd.getContainedMetaVariables().begin(), resultBdd.getContainedMetaVariables().end(), std::inserter(variablesToAbstract, variablesToAbstract.begin())); + + abstractGuard = resultBdd.existsAbstract(variablesToAbstract); + } else { + // Multiply the abstract guard as it can contain predicates that are not mentioned in the blocks. + resultBdd &= abstractGuard; + } // multiply with missing identities + resultBdd &= computeMissingIdentities(); // cache and return result - + resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()); + + // Cache the result. + cachedDd = GameBddResult(resultBdd, usedNondeterminismVariables); + + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions in " << std::chrono::duration_cast(end - start).count() << "ms."); + forceRecomputation = false; + + resultBdd.template toAdd().exportToDot("cmd_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); } } @@ -262,24 +388,22 @@ namespace storm { if (!skipBottomStates) { abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero(); } - uint_fast64_t sourceStateIndex = 0; for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { if (!skipBottomStates) { abstractGuard |= sourceDistributionsPair.first; } - + STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty."); STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty."); // We start with the distribution index of 1, becase 0 is reserved for a potential bottom choice. uint_fast64_t distributionIndex = 1; storm::dd::Bdd allDistributions = this->getAbstractionInformation().getDdManager().getBddZero(); for (auto const& distribution : sourceDistributionsPair.second) { - allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, numberOfVariablesNeeded); + allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, 0, numberOfVariablesNeeded); ++distributionIndex; STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty."); } resultBdd |= sourceDistributionsPair.first && allDistributions; - ++sourceStateIndex; STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty."); } @@ -501,11 +625,17 @@ namespace storm { template GameBddResult CommandAbstractor::abstract() { if (forceRecomputation) { - this->recomputeCachedBdd(); + if (useDecomposition) { + this->recomputeCachedBddUsingDecomposition(); + } else { + this->recomputeCachedBdd(); + } } else { cachedDd.bdd &= computeMissingGlobalIdentities(); } + STORM_LOG_TRACE("Command produces " << cachedDd.bdd.getNonZeroCount() << " transitions."); + return cachedDd; } @@ -520,6 +650,8 @@ namespace storm { return result; } +// abstractGuard.template toAdd().exportToDot("abstractguard_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + // Use the state abstractor to compute the set of abstract states that has this command enabled but // still has a transition to a bottom state. bottomStateAbstractor.constrain(reachableStates && abstractGuard); @@ -537,7 +669,7 @@ namespace storm { result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false); // Add the command encoding and the next free player 2 encoding. - result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(0, numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); + result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(0, 0, numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); return result; } diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index 9046fd053..21494e2b2 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -55,8 +55,9 @@ namespace storm { * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param allowInvalidSuccessors A flag indicating whether it is allowed to enumerate invalid successors. + * @param useDecomposition A flag indicating whether to use the decomposition during abstraction. */ - CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allowInvalidSuccessors); + CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allowInvalidSuccessors, bool useDecomposition); /*! * Refines the abstract command with the given predicates. @@ -237,6 +238,9 @@ namespace storm { // considered as source predicates. bool allowInvalidSuccessors; + // A flag indicating whether to use the decomposition when abstracting. + bool useDecomposition; + // A flag indicating whether the guard of the command was added as a predicate. If this is true, there // is no need to compute bottom states. bool skipBottomStates; diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index e825eee48..d9cf92093 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -23,7 +23,7 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { + ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { bool allowInvalidSuccessorsInCommands = false; if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::None || invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) { @@ -32,7 +32,7 @@ namespace storm { // For each concrete command, we create an abstract counterpart. for (auto const& command : module.getCommands()) { - commands.emplace_back(command, abstractionInformation, smtSolverFactory, allowInvalidSuccessorsInCommands); + commands.emplace_back(command, abstractionInformation, smtSolverFactory, allowInvalidSuccessorsInCommands, useDecomposition); } } diff --git a/src/storm/abstraction/prism/ModuleAbstractor.h b/src/storm/abstraction/prism/ModuleAbstractor.h index 357d9682d..5982ec361 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.h +++ b/src/storm/abstraction/prism/ModuleAbstractor.h @@ -36,8 +36,10 @@ namespace storm { * @param module The concrete module for which to build the abstraction. * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. + * @param invalidBlockDetectionStrategy The strategy to use for detecting invalid blocks. + * @param useDecomposition A flag that governs whether to use the decomposition in the abstraction. */ - ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy); + ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy, bool useDecomposition); ModuleAbstractor(ModuleAbstractor const&) = default; ModuleAbstractor& operator=(ModuleAbstractor const&) = default; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 8eab6d22d..f49c104c0 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -62,8 +62,9 @@ namespace storm { abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); // For each module of the concrete program, we create an abstract counterpart. + bool useDecomposition = storm::settings::getModule().isUseDecompositionSet(); for (auto const& module : program.getModules()) { - this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, invalidBlockDetectionStrategy); + this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, invalidBlockDetectionStrategy, useDecomposition); } // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. @@ -167,7 +168,7 @@ namespace storm { // If there are deadlock states, we fix them now. storm::dd::Add deadlockTransitions = abstractionInformation.getDdManager().template getAddZero(); if (!deadlockStates.isZero()) { - deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); + deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, 0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); } // Compute bottom states and the appropriate transitions if necessary. diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 9e37e5dca..45534e453 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -52,6 +52,8 @@ namespace storm { } else { preprocessedModel = originalProgram; } + + STORM_LOG_TRACE("Game-based model checker got program " << preprocessedModel.asPrismProgram()); } else { storm::jani::Model const& originalModel = model.asJaniModel(); STORM_LOG_THROW(originalModel.getModelType() == storm::jani::ModelType::DTMC || originalModel.getModelType() == storm::jani::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); @@ -330,7 +332,7 @@ namespace storm { } // #ifdef LOCAL_DEBUG - // abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); + // abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); // #endif // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). @@ -354,14 +356,14 @@ namespace storm { bool qualitativeRefinement = false; if (initialMaybeStates.isZero()) { // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. - STORM_LOG_TRACE("No initial state is a 'maybe' state. Refining abstraction based on qualitative check."); + STORM_LOG_TRACE("No initial state is a 'maybe' state."); result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); if (result) { printStatistics(*abstractor, game); return result; } else { - STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states."); + STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check."); auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now(); // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index dc70b13ec..9654c5692 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -23,6 +23,7 @@ namespace storm { const std::string AbstractionSettings::reuseQualitativeResultsOptionName = "reuse-qualitative"; const std::string AbstractionSettings::reuseQuantitativeResultsOptionName = "reuse-quantitative"; const std::string AbstractionSettings::reuseAllResultsOptionName = "reuse-all"; + const std::string AbstractionSettings::useDecompositionOptionName = "decomposition"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build()); @@ -44,6 +45,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, reuseQualitativeResultsOptionName, true, "Sets whether to reuse qualitative results.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, reuseQuantitativeResultsOptionName, true, "Sets whether to reuse quantitative results.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, reuseAllResultsOptionName, true, "Sets whether to reuse all results.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, useDecompositionOptionName, true, "Sets whether to apply decomposition during the abstraction.").build()); } bool AbstractionSettings::isAddAllGuardsSet() const { @@ -109,6 +111,10 @@ namespace storm { bool AbstractionSettings::isReuseAllResultsSet() const { return this->getOption(reuseAllResultsOptionName).getHasOptionBeenSet(); } + + bool AbstractionSettings::isUseDecompositionSet() const { + return this->getOption(useDecompositionOptionName).getHasOptionBeenSet(); + } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index d00faa692..8d7a35b2c 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -108,6 +108,13 @@ namespace storm { */ bool isReuseAllResultsSet() const; + /*! + * Retrieves whether the option to use the decomposition was set. + * + * @return True iff the option was set. + */ + bool isUseDecompositionSet() const; + const static std::string moduleName; private: @@ -124,6 +131,7 @@ namespace storm { const static std::string reuseQualitativeResultsOptionName; const static std::string reuseQuantitativeResultsOptionName; const static std::string reuseAllResultsOptionName; + const static std::string useDecompositionOptionName; }; }