From ba3ec0da275e98642b7be456df57c39ffe141b16 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 31 May 2018 20:39:15 +0200 Subject: [PATCH] lifted all new stuff to JANI menu game abstractor --- .../ExplicitQuantitativeResult.cpp | 5 + .../abstraction/ExplicitQuantitativeResult.h | 3 +- .../abstraction/jani/AutomatonAbstractor.cpp | 6 +- .../abstraction/jani/AutomatonAbstractor.h | 2 +- src/storm/abstraction/jani/EdgeAbstractor.cpp | 471 +++++++++--------- src/storm/abstraction/jani/EdgeAbstractor.h | 26 +- .../jani/JaniMenuGameAbstractor.cpp | 45 +- .../abstraction/jani/JaniMenuGameAbstractor.h | 2 +- .../abstraction/prism/CommandAbstractor.cpp | 23 +- .../abstraction/prism/CommandAbstractor.h | 8 - .../abstraction/prism/ModuleAbstractor.cpp | 10 +- .../prism/PrismMenuGameAbstractor.cpp | 12 +- .../abstraction/GameBasedMdpModelChecker.cpp | 44 +- .../abstraction/GameBasedMdpModelChecker.h | 10 +- 14 files changed, 318 insertions(+), 349 deletions(-) diff --git a/src/storm/abstraction/ExplicitQuantitativeResult.cpp b/src/storm/abstraction/ExplicitQuantitativeResult.cpp index 4b996483d..b15db88bb 100644 --- a/src/storm/abstraction/ExplicitQuantitativeResult.cpp +++ b/src/storm/abstraction/ExplicitQuantitativeResult.cpp @@ -13,6 +13,11 @@ namespace storm { // Intentionally left empty. } + template + ExplicitQuantitativeResult::ExplicitQuantitativeResult(std::vector&& values) : values(std::move(values)) { + // Intentionally left empty. + } + template std::vector const& ExplicitQuantitativeResult::getValues() const { return values; diff --git a/src/storm/abstraction/ExplicitQuantitativeResult.h b/src/storm/abstraction/ExplicitQuantitativeResult.h index 7604655d8..449feb09e 100644 --- a/src/storm/abstraction/ExplicitQuantitativeResult.h +++ b/src/storm/abstraction/ExplicitQuantitativeResult.h @@ -15,7 +15,8 @@ namespace storm { public: ExplicitQuantitativeResult() = default; ExplicitQuantitativeResult(uint64_t numberOfStates); - + ExplicitQuantitativeResult(std::vector&& values); + std::vector const& getValues() const; std::vector& getValues(); void setValue(uint64_t state, ValueType const& value); diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index b14b4db7b..3063c5b1b 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -1,8 +1,8 @@ #include "storm/abstraction/jani/AutomatonAbstractor.h" #include "storm/abstraction/BottomStateResult.h" -#include "storm/abstraction/GameBddResult.h" #include "storm/abstraction/AbstractionInformation.h" +#include "storm/abstraction/GameBddResult.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" @@ -24,12 +24,12 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - AutomatonAbstractor::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) { + AutomatonAbstractor::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) { // For each concrete command, we create an abstract counterpart. uint64_t edgeId = 0; for (auto const& edge : automaton.getEdges()) { - edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, useDecomposition); + edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, useDecomposition, debug); ++edgeId; } diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.h b/src/storm/abstraction/jani/AutomatonAbstractor.h index 9e800b756..3053de3c4 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.h +++ b/src/storm/abstraction/jani/AutomatonAbstractor.h @@ -35,7 +35,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param useDecomposition A flag indicating whether to use the decomposition during abstraction. */ - AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); + AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug); AutomatonAbstractor(AutomatonAbstractor const&) = default; AutomatonAbstractor& operator=(AutomatonAbstractor const&) = default; diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index c0592df3c..f60d99ece 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -23,7 +23,7 @@ namespace storm { namespace abstraction { namespace jani { template - EdgeAbstractor::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory) { + EdgeAbstractor::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory), debug(debug) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(edge.getNumberOfDestinations()); @@ -179,7 +179,6 @@ namespace storm { } relevantBlockPartition[representativeBlock].insert(relevantBlockPartition[assignmentVariableBlock].begin(), relevantBlockPartition[assignmentVariableBlock].end()); relevantBlockPartition[assignmentVariableBlock].clear(); - } } } @@ -188,200 +187,231 @@ namespace storm { // Now remove all blocks that are empty and obtain the partition. std::vector> cleanedRelevantBlockPartition; - for (auto& element : relevantBlockPartition) { - if (!element.empty()) { - cleanedRelevantBlockPartition.emplace_back(std::move(element)); + for (auto& outerBlock : relevantBlockPartition) { + if (!outerBlock.empty()) { + cleanedRelevantBlockPartition.emplace_back(); + + for (auto const& innerBlock : outerBlock) { + if (!localExpressionInformation.getExpressionBlock(innerBlock).empty()) { + cleanedRelevantBlockPartition.back().insert(innerBlock); + } + } + + if (cleanedRelevantBlockPartition.back().empty()) { + cleanedRelevantBlockPartition.pop_back(); + } } } relevantBlockPartition = std::move(cleanedRelevantBlockPartition); - // if the decomposition has size 1, use the plain technique from before - if (relevantBlockPartition.size() == 1) { - STORM_LOG_TRACE("Relevant block partition size is one, falling back to regular computation."); - recomputeCachedBddWithoutDecomposition(); - } else { - std::set variablesContainedInGuard = edge.get().getGuard().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); + STORM_LOG_TRACE("Decomposition into " << relevantBlockPartition.size() << " blocks."); + if (this->debug) { + uint64_t blockIndex = 0; 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; - - 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); - } + STORM_LOG_TRACE("Predicates of block " << blockIndex << ":"); + std::set blockPredicateIndices; + for (auto const& innerBlock : block) { + blockPredicateIndices.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end()); } - 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); + for (auto const& predicateIndex : blockPredicateIndices) { + STORM_LOG_TRACE(abstractionInformation.get().getPredicateByIndex(predicateIndex)); } - // 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))); + ++blockIndex; + } + } + + std::set variablesContainedInGuard = edge.get().getGuard().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; } } - - // 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()); + if (allContained) { + enumerateAbstractGuard = false; + } + } + + uint64_t numberOfSolutions = 0; + uint64_t numberOfTotalSolutions = 0; + + // If we need to enumerate the guard, do it only once now. + if (enumerateAbstractGuard) { + 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); } - - 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); - } + } + 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 << " solutions 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()); + } + + if (relevantPredicates.empty()) { + STORM_LOG_TRACE("Block does not contain relevant predicates, skipping it."); + continue; + } + + 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 destinationIndex = 0; destinationIndex < edge.get().getNumberOfDestinations(); ++destinationIndex) { - destinationVariablesAndPredicates.emplace_back(); - for (auto const& assignment : edge.get().getDestination(destinationIndex).getOrderedAssignments().getAllAssignments()) { - uint64_t assignmentVariableBlockIndex = localExpressionInformation.getBlockIndexOfVariable(assignment.getExpressionVariable()); + } + + std::vector>> destinationVariablesAndPredicates; + for (uint64_t destinationIndex = 0; destinationIndex < edge.get().getNumberOfDestinations(); ++destinationIndex) { + destinationVariablesAndPredicates.emplace_back(); + for (auto const& assignment : edge.get().getDestination(destinationIndex).getOrderedAssignments().getAllAssignments()) { + uint64_t assignmentVariableBlockIndex = localExpressionInformation.getBlockIndexOfVariable(assignment.getVariable().getExpressionVariable()); + + if (block.find(assignmentVariableBlockIndex) != block.end()) { std::set const& assignmentVariableBlock = localExpressionInformation.getExpressionBlock(assignmentVariableBlockIndex); - if (block.find(assignmentVariableBlockIndex) != block.end()) { - for (auto const& element : relevantPredicatesAndVariables.second[destinationIndex]) { - if (assignmentVariableBlock.find(element.second) != assignmentVariableBlock.end()) { - destinationVariablesAndPredicates.back().push_back(element); - transitionDecisionVariables.push_back(element.first); - } + for (auto const& element : relevantPredicatesAndVariables.second[destinationIndex]) { + 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(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; } - if (enumerateAbstractGuard) { - smtSolver->pop(); - } + std::unordered_map, std::vector>> sourceToDistributionsMap; + numberOfSolutions = 0; + 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 << "."); + numberOfTotalSolutions += numberOfSolutions; - // multiply the results - storm::dd::Bdd resultBdd = getAbstractionInformation().getDdManager().getBddOne(); - for (auto const& blockBdd : blockBdds) { - resultBdd &= blockBdd; + // 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())); } - // if we did not explicitly enumerate the guard, we can construct it from the result BDD. - if (!enumerateAbstractGuard) { - std::set allVariables(this->getAbstractionInformation().getSuccessorVariables()); - auto player2Variables = this->getAbstractionInformation().getPlayer2VariableSet(usedNondeterminismVariables); - allVariables.insert(player2Variables.begin(), player2Variables.end()); - auto auxVariables = this->getAbstractionInformation().getAuxVariableSet(0, this->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())); + // 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)))); + + // Finally, build overall result. + storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero(); + + 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."); - abstractGuard = resultBdd.existsAbstract(variablesToAbstract); - } else { - // Multiply the abstract guard as it can contain predicates that are not mentioned in the blocks. - resultBdd &= abstractGuard; + // We start with the distribution index of 1, because 0 is reserved for a potential bottom choice. + uint_fast64_t distributionIndex = blockCounter == 0 ? 1 : 0; + 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; + STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty."); } + usedNondeterminismVariables += numberOfVariablesNeeded; - // multiply with missing identities - resultBdd &= computeMissingIdentities(); - - // cache and return result - resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()); + blockBdds.push_back(resultBdd); + ++blockCounter; + } + + if (enumerateAbstractGuard) { + smtSolver->pop(); + } + + // multiply the results + storm::dd::Bdd resultBdd = getAbstractionInformation().getDdManager().getBddOne(); + uint64_t blockIndex = 0; + for (auto const& blockBdd : blockBdds) { + resultBdd &= blockBdd; + ++blockIndex; + } + + // 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()); - // Cache the result. - cachedDd = GameBddResult(resultBdd, usedNondeterminismVariables); + std::set variablesToAbstract; + std::set_intersection(allVariables.begin(), allVariables.end(), resultBdd.getContainedMetaVariables().begin(), resultBdd.getContainedMetaVariables().end(), std::inserter(variablesToAbstract, variablesToAbstract.begin())); - 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; + 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 &= computeMissingDestinationIdentities(); + + // cache and return result + resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()); + + // Cache the result. + cachedDd = GameBddResult(resultBdd, usedNondeterminismVariables); + + auto end = std::chrono::high_resolution_clock::now(); + + STORM_LOG_TRACE("Enumerated " << numberOfTotalSolutions << " solutions in " << std::chrono::duration_cast(end - start).count() << "ms."); + forceRecomputation = false; } template @@ -414,7 +444,6 @@ namespace storm { if (!skipBottomStates) { abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero(); } - uint_fast64_t sourceStateIndex = 0; for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { if (!skipBottomStates) { abstractGuard |= sourceDistributionsPair.first; @@ -431,11 +460,10 @@ namespace storm { 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."); } - resultBdd &= computeMissingIdentities(); + resultBdd &= computeMissingDestinationIdentities(); resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()); STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions."); @@ -461,14 +489,8 @@ namespace storm { storm::expressions::Variable const& assignedVariable = assignment.getExpressionVariable(); 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. - assignedVariables.insert(assignedVariable); } - auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables); - result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end()); - return result; } @@ -535,7 +557,8 @@ namespace storm { template storm::dd::Bdd EdgeAbstractor::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector> const& variablePredicates) const { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); - for (auto const& variableIndexPair : variablePredicates) { + for (auto variableIndexPairIt = variablePredicates.rbegin(), variableIndexPairIte = variablePredicates.rend(); variableIndexPairIt != variableIndexPairIte; ++variableIndexPairIt) { + auto const& variableIndexPair = *variableIndexPairIt; if (model.getBooleanValue(variableIndexPair.first)) { result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); } else { @@ -555,7 +578,8 @@ namespace storm { storm::dd::Bdd updateBdd = this->getAbstractionInformation().getDdManager().getBddOne(); // Translate block variables for this update into a successor block. - for (auto const& variableIndexPair : variablePredicates[destinationIndex]) { + for (auto variableIndexPairIt = variablePredicates[destinationIndex].rbegin(), variableIndexPairIte = variablePredicates[destinationIndex].rend(); variableIndexPairIt != variableIndexPairIte; ++variableIndexPairIt) { + auto const& variableIndexPair = *variableIndexPairIt; if (model.getBooleanValue(variableIndexPair.first)) { updateBdd &= this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } else { @@ -572,99 +596,75 @@ namespace storm { } template - storm::dd::Bdd EdgeAbstractor::computeMissingIdentities() const { - storm::dd::Bdd identities = computeMissingGlobalIdentities(); - identities &= computeMissingUpdateIdentities(); - return identities; - } - - template - storm::dd::Bdd EdgeAbstractor::computeMissingUpdateIdentities() const { + storm::dd::Bdd EdgeAbstractor::computeMissingDestinationIdentities() const { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); - for (uint_fast64_t updateIndex = 0; updateIndex < edge.get().getNumberOfDestinations(); ++updateIndex) { + for (uint_fast64_t destinationIndex = 0; destinationIndex < edge.get().getNumberOfDestinations(); ++destinationIndex) { // Compute the identities that are missing for this update. - auto updateRelevantIt = relevantPredicatesAndVariables.second[updateIndex].begin(); - auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end(); + auto updateRelevantIt = relevantPredicatesAndVariables.second[destinationIndex].rbegin(); + auto updateRelevantIte = relevantPredicatesAndVariables.second[destinationIndex].rend(); 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) { - updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second); + for (uint_fast64_t predicateIndex = this->getAbstractionInformation().getNumberOfPredicates() - 1;; --predicateIndex) { + if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) { + updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); } else { ++updateRelevantIt; } + + if (predicateIndex == 0) { + break; + } } - result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); + result |= updateIdentity && this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } return result; } - template - storm::dd::Bdd EdgeAbstractor::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) { - result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); - } else { - ++relevantIt; - } - } - - return result; - } - template GameBddResult EdgeAbstractor::abstract() { if (forceRecomputation) { this->recomputeCachedBdd(); } else { - cachedDd.bdd &= computeMissingGlobalIdentities(); + cachedDd.bdd &= computeMissingDestinationIdentities(); } + STORM_LOG_TRACE("Edge produces " << cachedDd.bdd.getNonZeroCount() << " transitions."); + return cachedDd; } template BottomStateResult EdgeAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables, boost::optional> const& locationVariables) { - // Compute the reachable states that have this edge enabled. - storm::dd::Bdd reachableStatesWithEdge; - if (locationVariables) { - reachableStatesWithEdge = (reachableStates && abstractGuard && this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex())).existsAbstract(this->getAbstractionInformation().getSourceLocationVariables()); - } else { - reachableStatesWithEdge = (reachableStates && abstractGuard).existsAbstract(this->getAbstractionInformation().getSourceLocationVariables()); - } - - STORM_LOG_TRACE("Computing bottom state transitions of edge with guard " << edge.get().getGuard()); + STORM_LOG_TRACE("Computing bottom state transitions of edge with index " << edgeId << "."); BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); - // If the guard of this edge is a predicate, there are not bottom states/transitions. + // If the guard of this command is a predicate, there are not bottom states/transitions. if (skipBottomStates) { STORM_LOG_TRACE("Skipping bottom state computation for this edge."); return result; } - // Use the state abstractor to compute the set of abstract states that has this edge enabled but still - // has a transition to a bottom state. + storm::dd::Bdd reachableStatesWithEdge = reachableStates && abstractGuard; + // needed? +// if (locationVariables) { +// reachableStatesWithEdge = (reachableStates && abstractGuard && this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex())).existsAbstract(this->getAbstractionInformation().getSourceLocationVariables()); +// } else { +// reachableStatesWithEdge = (reachableStates && abstractGuard).existsAbstract(this->getAbstractionInformation().getSourceLocationVariables()); +// } + + + // 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(reachableStatesWithEdge); if (locationVariables) { result.states = bottomStateAbstractor.getAbstractStates() && reachableStatesWithEdge && this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex()); } else { result.states = bottomStateAbstractor.getAbstractStates() && reachableStatesWithEdge; } - + // If the result is empty one time, we can skip the bottom state computation from now on. if (result.states.isZero()) { skipBottomStates = true; @@ -673,14 +673,11 @@ namespace storm { // Now equip all these states with an actual transition to a bottom state. result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities() && this->getAbstractionInformation().getBottomStateBdd(false, false); - // Mark the states as bottom states and add source location information. + // Mark the states as bottom states. result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false); - // Add the edge encoding. - result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(0, 0,numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); - - // Add the location identity to the transitions. - result.transitions &= this->getAbstractionInformation().getAllLocationIdentities(); + // Add the command encoding and the next free player 2 encoding. + 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/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h index 7ba7445a5..3c8c1d21b 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.h +++ b/src/storm/abstraction/jani/EdgeAbstractor.h @@ -58,7 +58,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param useDecomposition A flag indicating whether to use an edge decomposition during abstraction. */ - EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); + EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug); /*! * Refines the abstract edge with the given predicates. @@ -187,21 +187,14 @@ namespace storm { * Recomputes the cached BDD using the decomposition. */ void recomputeCachedBddWithDecomposition(); - - /*! - * Computes the missing state identities. - * - * @return A BDD that represents the all missing state identities. - */ - storm::dd::Bdd computeMissingIdentities() const; /*! - * Computes the missing state identities for the updates. + * Computes the missing state identities for the destinations. * * @return A BDD that represents the state identities for predicates that are irrelevant for the * successor states. */ - storm::dd::Bdd computeMissingUpdateIdentities() const; + storm::dd::Bdd computeMissingDestinationIdentities() const; /*! * Retrieves the abstraction information object. @@ -216,15 +209,7 @@ namespace storm { * @return The abstraction information object. */ 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; - + // An SMT responsible for this abstract command. std::unique_ptr smtSolver; @@ -275,6 +260,9 @@ namespace storm { // A state-set abstractor used to determine the bottom states if not all guards were added. StateSetAbstractor bottomStateAbstractor; + + // A flag that indicates whether or not debug mode is enabled. + bool debug; }; } } diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index be4e33d8e..886bcbdcc 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -51,26 +51,28 @@ namespace storm { validBlockAbstractor.constrain(range); } - uint_fast64_t totalNumberOfCommands = 0; - uint_fast64_t maximalUpdateCount = 0; + uint_fast64_t totalNumberOfEdges = 0; + uint_fast64_t maximalDestinationCount = 0; std::vector allGuards; for (auto const& automaton : model.getAutomata()) { for (auto const& edge : automaton.getEdges()) { - maximalUpdateCount = std::max(maximalUpdateCount, static_cast(edge.getNumberOfDestinations())); + maximalDestinationCount = std::max(maximalDestinationCount, static_cast(edge.getNumberOfDestinations())); } - totalNumberOfCommands += automaton.getNumberOfEdges(); + totalNumberOfEdges += automaton.getNumberOfEdges(); } // NOTE: currently we assume that 64 player 2 variables suffice, which corresponds to 2^64 possible // choices. If for some reason this should not be enough, we could grow this vector dynamically, but // odds are that it's impossible to treat such models in any event. - abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 64, static_cast(std::ceil(std::log2(maximalUpdateCount)))); + abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfEdges))), 64, static_cast(std::ceil(std::log2(maximalDestinationCount)))); // For each module of the concrete program, we create an abstract counterpart. - bool useDecomposition = storm::settings::getModule().isUseDecompositionSet(); + auto const& settings = storm::settings::getModule(); + bool useDecomposition = settings.isUseDecompositionSet(); + bool debug = settings.isDebugSet(); for (auto const& automaton : model.getAutomata()) { - automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, useDecomposition); + automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, useDecomposition, debug); } // Retrieve global BDDs/ADDs so we can multiply them in the abstraction process. @@ -105,7 +107,7 @@ namespace storm { MenuGame JaniMenuGameAbstractor::abstract() { if (refinementPerformed) { currentGame = buildGame(); - refinementPerformed = true; + refinementPerformed = false; } return *currentGame; } @@ -153,7 +155,7 @@ namespace storm { template std::unique_ptr> JaniMenuGameAbstractor::buildGame() { - // As long as there is only one module, we only build its game representation. + // As long as there is only one automaton, we only build its game representation. GameBddResult game = automata.front().abstract(); // Add the locations to the transitions. @@ -161,10 +163,12 @@ namespace storm { // Construct a set of all unnecessary variables, so we can abstract from it. std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); + std::set successorAndAuxVariables(abstractionInformation.getSuccessorVariables()); auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); + successorAndAuxVariables.insert(auxVariables.begin(), auxVariables.end()); storm::utility::Stopwatch relevantStatesWatch(true); storm::dd::Bdd nonTerminalStates = this->abstractionInformation.getDdManager().getBddOne(); @@ -179,12 +183,15 @@ namespace storm { } relevantStatesWatch.stop(); + storm::dd::Bdd validBlocks = validBlockAbstractor.getValidBlocks(); + + // Compute the choices with only valid successors so we can restrict the game to these. + auto choicesWithOnlyValidSuccessors = !game.bdd.andExists(!validBlocks.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs()), successorAndAuxVariables) && game.bdd.existsAbstract(successorAndAuxVariables); + // Do a reachability analysis on the raw transition relation. - storm::dd::Bdd transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract); - storm::dd::Bdd initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates(); - if (!model.get().hasTrivialInitialStatesExpression()) { - initialStates &= validBlockAbstractor.getValidBlocks(); - } + storm::dd::Bdd extendedTransitionRelation = validBlocks && nonTerminalStates && game.bdd && choicesWithOnlyValidSuccessors; + storm::dd::Bdd transitionRelation = extendedTransitionRelation.existsAbstract(variablesToAbstract); + storm::dd::Bdd initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates() && validBlocks; initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); @@ -194,20 +201,19 @@ namespace storm { storm::dd::Bdd targetStates = reachableStates && this->getStates(this->getTargetStateExpression()); // In the presence of target states, we keep only states that can reach the target states. - auto newReachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates; - reachableStates = newReachableStates; + reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates; // Include all successors of reachable states, because the backward search otherwise potentially // cuts probability 0 choices of these states. reachableStates |= (reachableStates && !targetStates).relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); - relevantStatesWatch.stop(); // Restrict transition relation to relevant fragment for computation of deadlock states. transitionRelation &= reachableStates && reachableStates.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs()); + relevantStatesWatch.stop(); STORM_LOG_TRACE("Restricting to relevant states took " << relevantStatesWatch.getTimeInMilliseconds() << "ms."); } - + // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states, // as the bottom states are not contained in the reachable states. storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables()); @@ -227,8 +233,7 @@ namespace storm { // Construct the transition matrix by cutting away the transitions of unreachable states. // Note that we also restrict the successor states of transitions, because there might be successors // that are not in the set of relevant states we restrict to. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates && reachableStates.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs())).template toAdd(); - + storm::dd::Add transitionMatrix = (extendedTransitionRelation && reachableStates && reachableStates.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs())).template toAdd(); transitionMatrix *= edgeDecoratorAdd; transitionMatrix += deadlockTransitions; diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index 916dbd7d6..80c625072 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -117,7 +117,7 @@ namespace storm { * @param highlightStates A BDD characterizing states that will be highlighted. * @param filter A filter that is applied to select which part of the game to export. */ - void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override; + virtual void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override; virtual uint64_t getNumberOfPredicates() const override; diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index 4a22b976f..39d95845b 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -283,7 +283,7 @@ namespace storm { } } - // then enumerate the solutions for each of the blocks of the decomposition + // Then enumerate the solutions for each of the blocks of the decomposition uint64_t usedNondeterminismVariables = 0; uint64_t blockCounter = 0; std::vector> blockBdds; @@ -349,7 +349,6 @@ namespace storm { // 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."); @@ -363,7 +362,6 @@ namespace storm { 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; @@ -402,7 +400,7 @@ namespace storm { } // multiply with missing identities - resultBdd &= computeMissingIdentities(); + resultBdd &= computeMissingUpdateIdentities(); // cache and return result resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()); @@ -465,7 +463,7 @@ namespace storm { STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty."); } - resultBdd &= computeMissingIdentities(); + resultBdd &= computeMissingUpdateIdentities(); 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."); @@ -491,14 +489,8 @@ namespace storm { storm::expressions::Variable const& assignedVariable = assignment.getVariable(); 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. -// assignedVariables.insert(assignedVariable); } -// auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables); -// result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end()); - return result; } @@ -507,7 +499,7 @@ namespace storm { std::pair, std::vector>> result; // To start with, all predicates related to the guard are relevant source predicates. - result.first = localExpressionInformation.getRelatedExpressions(command.get().getGuardExpression().getVariables()); + result.first = localExpressionInformation.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables()); // Then, we add the predicates that become relevant, because of some update. for (auto const& update : command.get().getUpdates()) { @@ -596,7 +588,6 @@ namespace storm { } updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); - result |= updateBdd; } @@ -604,11 +595,6 @@ namespace storm { return result; } - template - storm::dd::Bdd CommandAbstractor::computeMissingIdentities() const { - return computeMissingUpdateIdentities(); - } - template storm::dd::Bdd CommandAbstractor::computeMissingUpdateIdentities() const { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); @@ -619,7 +605,6 @@ namespace storm { auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].rend(); storm::dd::Bdd updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne(); - for (uint_fast64_t predicateIndex = this->getAbstractionInformation().getNumberOfPredicates() - 1;; --predicateIndex) { if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) { updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index e6d7c7238..9cc48b3b2 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -213,14 +213,6 @@ 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; - // An SMT responsible for this abstract command. std::unique_ptr smtSolver; diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index d1574e23b..bafb43717 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -1,7 +1,7 @@ #include "storm/abstraction/prism/ModuleAbstractor.h" -#include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/BottomStateResult.h" +#include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/GameBddResult.h" #include "storm/storage/dd/DdManager.h" @@ -26,10 +26,8 @@ namespace storm { ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { // For each concrete command, we create an abstract counterpart. - uint64_t counter = 0; for (auto const& command : module.getCommands()) { commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition, debug); - ++counter; } } @@ -37,8 +35,7 @@ namespace storm { void ModuleAbstractor::refine(std::vector const& predicates) { for (uint_fast64_t index = 0; index < commands.size(); ++index) { STORM_LOG_TRACE("Refining command with index " << index << "."); - CommandAbstractor& command = commands[index]; - command.refine(predicates); + commands[index].refine(predicates); } } @@ -85,8 +82,7 @@ namespace storm { BottomStateResult ModuleAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); - for (uint64_t index = 0; index < commands.size(); ++index) { - auto& command = commands[index]; + for (auto& command : commands) { BottomStateResult commandBottomStateResult = command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables); result.states |= commandBottomStateResult.states; result.transitions |= commandBottomStateResult.transitions; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 88d75b50f..60ab41e92 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -33,8 +33,7 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, - std::shared_ptr const& smtSolverFactory) + PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory) : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager(), program.getAllExpressionVariables(), smtSolverFactory->create(program.getManager())), modules(), initialStateAbstractor(abstractionInformation, {program.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false) { // For now, we assume that there is a single module. If the program has more than one module, it needs @@ -179,7 +178,6 @@ namespace storm { storm::dd::Bdd validBlocks = validBlockAbstractor.getValidBlocks(); // Compute the choices with only valid successors so we can restrict the game to these. - auto choicesWithOnlyValidSuccessors = !game.bdd.andExists(!validBlocks.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs()), successorAndAuxVariables) && game.bdd.existsAbstract(successorAndAuxVariables); // Do a reachability analysis on the raw transition relation. @@ -226,7 +224,7 @@ namespace storm { // Construct the transition matrix by cutting away the transitions of unreachable states. // Note that we also restrict the successor states of transitions, because there might be successors - // that are not in the relevant we restrict to. + // that are not in the set of relevant states we restrict to. storm::dd::Add transitionMatrix = (extendedTransitionRelation && reachableStates && reachableStates.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs())).template toAdd(); transitionMatrix *= commandUpdateProbabilitiesAdd; transitionMatrix += deadlockTransitions; @@ -242,9 +240,7 @@ namespace storm { reachableStates |= bottomStateResult.states; } - std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables); - - std::set allNondeterminismVariables = usedPlayer2Variables; + std::set allNondeterminismVariables = player2Variables; allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); std::set allSourceVariables(abstractionInformation.getSourceVariables()); @@ -252,7 +248,7 @@ namespace storm { std::set allSuccessorVariables(abstractionInformation.getSuccessorVariables()); allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false)); - return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), player2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); } template diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index f08785a6d..f06c91853 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -418,9 +418,10 @@ namespace storm { // If there is a previous result, unpack the previous values with respect to the new ODD. if (previousResult) { + STORM_LOG_ASSERT(player2Min, "Can only reuse previous values when minimizing."); previousResult.get().odd.oldToNewIndex(odd, [&previousResult,&result,player2Min,player1Prob1States] (uint64_t oldOffset, uint64_t newOffset) { - if (!player2Min && !player1Prob1States.get(newOffset)) { - result.getValues()[newOffset] = player2Min ? previousResult.get().values.getMin().getValues()[oldOffset] : previousResult.get().values.getMax().getValues()[oldOffset]; + if (!player1Prob1States.get(newOffset)) { + result.getValues()[newOffset] = player2Min ? previousResult.get().values.getValues()[oldOffset] : previousResult.get().values.getValues()[oldOffset]; } }); } @@ -1019,7 +1020,11 @@ namespace storm { STORM_LOG_INFO("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check."); // Post-process strategies for better refinements. + storm::utility::Stopwatch strategyProcessingWatch(true); postProcessStrategies(player1Direction, minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, qualitativeResult, this->fixPlayer1Strategy, this->fixPlayer2Strategy, this->debug); + strategyProcessingWatch.stop(); + totalStrategyProcessingWatch.add(strategyProcessingWatch); + STORM_LOG_DEBUG("Postprocessed strategies in " << strategyProcessingWatch.getTimeInMilliseconds() << "ms."); // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. @@ -1040,6 +1045,11 @@ namespace storm { // (7) Solve the min values and check whether we can give the answer already. storm::utility::Stopwatch quantitativeWatch(true); quantitativeResult.setMin(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair, odd, nullptr, nullptr, this->reuseQuantitativeResults ? previousResult : boost::none)); + + // Dispose of previous result as we now reused it. + if (previousResult) { + previousResult.get().clear(); + } quantitativeWatch.stop(); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.getMin().getRange(initialStates)); if (result) { @@ -1065,7 +1075,12 @@ namespace storm { } // Post-process strategies for better refinements. + storm::utility::Stopwatch strategyProcessingWatch(true); postProcessStrategies(player1Direction, minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, quantitativeResult, this->fixPlayer1Strategy, this->fixPlayer2Strategy, this->debug); + strategyProcessingWatch.stop(); + totalStrategyProcessingWatch.add(strategyProcessingWatch); + STORM_LOG_DEBUG("Postprocessed strategies in " << strategyProcessingWatch.getTimeInMilliseconds() << "ms."); + // Make sure that all strategies are still valid strategies. STORM_LOG_ASSERT(minStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << minStrategyPair.getNumberOfUndefinedPlayer1States() << "."); @@ -1081,28 +1096,9 @@ namespace storm { if (this->reuseQuantitativeResults) { PreviousExplicitResult nextPreviousResult; - nextPreviousResult.values = std::move(quantitativeResult); + nextPreviousResult.values = std::move(quantitativeResult.getMin()); nextPreviousResult.odd = odd; - - // We transform the offset choices for the states to their labels, so we can more easily identify - // them in the next iteration. - nextPreviousResult.minPlayer1Labels.resize(odd.getTotalOffset()); - nextPreviousResult.maxPlayer1Labels.resize(odd.getTotalOffset()); - for (uint64_t player1State = 0; player1State < odd.getTotalOffset(); ++player1State) { - if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(player1State)) { - nextPreviousResult.minPlayer1Labels[player1State] = player1Labeling[minStrategyPair.getPlayer1Strategy().getChoice(player1State)]; - } else { - nextPreviousResult.minPlayer1Labels[player1State] = std::numeric_limits::max(); - } - if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(player1State)) { - nextPreviousResult.maxPlayer1Labels[player1State] = player1Labeling[maxStrategyPair.getPlayer1Strategy().getChoice(player1State)]; - } else { - nextPreviousResult.minPlayer1Labels[player1State] = std::numeric_limits::max(); - } - } - previousResult = std::move(nextPreviousResult); - STORM_LOG_TRACE("Prepared next previous result to reuse values."); } } @@ -1273,6 +1269,7 @@ namespace storm { uint64_t totalAbstractionTimeMillis = totalAbstractionWatch.getTimeInMilliseconds(); uint64_t totalTranslationTimeMillis = totalTranslationWatch.getTimeInMilliseconds(); + uint64_t totalStrategyProcessingTimeMillis = totalStrategyProcessingWatch.getTimeInMilliseconds(); uint64_t totalSolutionTimeMillis = totalSolutionWatch.getTimeInMilliseconds(); uint64_t totalRefinementTimeMillis = totalRefinementWatch.getTimeInMilliseconds(); uint64_t totalTimeMillis = totalWatch.getTimeInMilliseconds(); @@ -1281,6 +1278,9 @@ namespace storm { std::cout << " * abstraction: " << totalAbstractionTimeMillis << "ms (" << 100 * static_cast(totalAbstractionTimeMillis)/totalTimeMillis << "%)" << std::endl; if (this->solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Sparse) { std::cout << " * translation: " << totalTranslationTimeMillis << "ms (" << 100 * static_cast(totalTranslationTimeMillis)/totalTimeMillis << "%)" << std::endl; + if (fixPlayer1Strategy || fixPlayer2Strategy) { + std::cout << " * strategy processing: " << totalStrategyProcessingTimeMillis << "ms (" << 100 * static_cast(totalStrategyProcessingTimeMillis)/totalTimeMillis << "%)" << std::endl; + } } std::cout << " * solution: " << totalSolutionTimeMillis << "ms (" << 100 * static_cast(totalSolutionTimeMillis)/totalTimeMillis << "%)" << std::endl; std::cout << " * refinement: " << totalRefinementTimeMillis << "ms (" << 100 * static_cast(totalRefinementTimeMillis)/totalTimeMillis << "%)" << std::endl; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index 353be113a..d76eee4f2 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -62,10 +62,13 @@ namespace storm { namespace detail { template struct PreviousExplicitResult { - ExplicitQuantitativeResultMinMax values; - std::vector minPlayer1Labels; - std::vector maxPlayer1Labels; + ExplicitQuantitativeResult values; storm::dd::Odd odd; + + void clear() { + odd = storm::dd::Odd(); + values = ExplicitQuantitativeResult(); + } }; } @@ -164,6 +167,7 @@ namespace storm { storm::utility::Stopwatch totalSolutionWatch; storm::utility::Stopwatch totalRefinementWatch; storm::utility::Stopwatch totalTranslationWatch; + storm::utility::Stopwatch totalStrategyProcessingWatch; storm::utility::Stopwatch totalWatch; }; }