diff --git a/src/storm/abstraction/ExpressionTranslator.cpp b/src/storm/abstraction/ExpressionTranslator.cpp index 76dd8a2a3..8bf792278 100644 --- a/src/storm/abstraction/ExpressionTranslator.cpp +++ b/src/storm/abstraction/ExpressionTranslator.cpp @@ -118,7 +118,7 @@ namespace storm { // At this point, none of the predicates was found to be equivalent, but there is no need to split as the subexpressions are not valid predicates. - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator (" << expression << ")."); } return boost::any(); } diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index aad16cc2d..b570bf50c 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -63,14 +63,17 @@ namespace storm { } template - MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule().isUseInterpolationSet()), splitAll(false), splitPredicates(false), addedAllGuardsFlag(false), pivotSelectionHeuristic(storm::settings::getModule().getPivotSelectionHeuristic()), splitter(), equivalenceChecker(std::move(smtSolver)) { + MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule().isUseInterpolationSet()), splitAll(false), splitPredicates(false), rankPredicates(false), addedAllGuardsFlag(false), pivotSelectionHeuristic(), splitter(), equivalenceChecker(std::move(smtSolver)) { - equivalenceChecker.addConstraints(abstractor.getAbstractionInformation().getConstraints()); + auto const& abstractionSettings = storm::settings::getModule(); + pivotSelectionHeuristic = abstractionSettings.getPivotSelectionHeuristic(); AbstractionSettings::SplitMode splitMode = storm::settings::getModule().getSplitMode(); splitAll = splitMode == AbstractionSettings::SplitMode::All; splitPredicates = splitMode == AbstractionSettings::SplitMode::NonGuard; + rankPredicates = abstractionSettings.isRankRefinementPredicatesSet(); + equivalenceChecker.addConstraints(abstractor.getAbstractionInformation().getConstraints()); if (storm::settings::getModule().isAddAllGuardsSet()) { std::vector guards; @@ -82,7 +85,7 @@ namespace storm { } } performRefinement(createGlobalRefinement(preprocessPredicates(guards, RefinementPredicates::Source::InitialGuard))); - + addedAllGuardsFlag = true; } } @@ -298,6 +301,9 @@ namespace storm { for (uint64_t predicateIndex = 0; predicateIndex < lower.size(); ++predicateIndex) { if (lower[predicateIndex] != upper[predicateIndex]) { possibleRefinementPredicates.push_back(abstractionInformation.getPredicateByIndex(predicateIndex).substitute(variableUpdates).simplify()); + if (!rankPredicates) { + break; + } } } ++orderedUpdateIndex; @@ -307,49 +313,54 @@ namespace storm { STORM_LOG_ASSERT(!possibleRefinementPredicates.empty(), "Expected refinement predicates."); - // Since we can choose any of the deviation predicates to perform the split, we go through the remaining - // updates and build all deviation predicates. We can then check whether any of the possible refinement - // predicates also eliminates another deviation. - std::vector otherRefinementPredicates; - for (; orderedUpdateIndex < updateIndicesAndMasses.size(); ++orderedUpdateIndex) { - storm::storage::BitVector const& lower = lowerChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first; - storm::storage::BitVector const& upper = upperChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first; - - bool deviates = lower != upper; - if (deviates) { - std::map newVariableUpdates = abstractor.get().getVariableUpdates(player1Index, updateIndicesAndMasses[orderedUpdateIndex].first); - for (uint64_t predicateIndex = 0; predicateIndex < lower.size(); ++predicateIndex) { - if (lower[predicateIndex] != upper[predicateIndex]) { - otherRefinementPredicates.push_back(abstractionInformation.getPredicateByIndex(predicateIndex).substitute(newVariableUpdates).simplify()); + if (rankPredicates) { + // Since we can choose any of the deviation predicates to perform the split, we go through the remaining + // updates and build all deviation predicates. We can then check whether any of the possible refinement + // predicates also eliminates another deviation. + std::vector otherRefinementPredicates; + for (; orderedUpdateIndex < updateIndicesAndMasses.size(); ++orderedUpdateIndex) { + storm::storage::BitVector const& lower = lowerChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first; + storm::storage::BitVector const& upper = upperChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first; + + bool deviates = lower != upper; + if (deviates) { + std::map newVariableUpdates = abstractor.get().getVariableUpdates(player1Index, updateIndicesAndMasses[orderedUpdateIndex].first); + for (uint64_t predicateIndex = 0; predicateIndex < lower.size(); ++predicateIndex) { + if (lower[predicateIndex] != upper[predicateIndex]) { + otherRefinementPredicates.push_back(abstractionInformation.getPredicateByIndex(predicateIndex).substitute(newVariableUpdates).simplify()); + } } } } - } - - // Finally, go through the refinement predicates and see how many deviations they cover. - std::vector refinementPredicateIndexToCount(possibleRefinementPredicates.size(), 0); - for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) { - refinementPredicateIndexToCount[index] = 1; - } - for (auto const& otherPredicate : otherRefinementPredicates) { + + // Finally, go through the refinement predicates and see how many deviations they cover. + std::vector refinementPredicateIndexToCount(possibleRefinementPredicates.size(), 0); for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) { - if (equivalenceChecker.areEquivalentModuloNegation(otherPredicate, possibleRefinementPredicates[index])) { - ++refinementPredicateIndexToCount[index]; + refinementPredicateIndexToCount[index] = 1; + } + for (auto const& otherPredicate : otherRefinementPredicates) { + for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) { + if (equivalenceChecker.areEquivalentModuloNegation(otherPredicate, possibleRefinementPredicates[index])) { + ++refinementPredicateIndexToCount[index]; + } } } - } - - // Find predicate that covers the most deviations. - uint64_t chosenPredicateIndex = 0; - for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) { - if (refinementPredicateIndexToCount[index] > refinementPredicateIndexToCount[chosenPredicateIndex]) { - chosenPredicateIndex = index; + + // Find predicate that covers the most deviations. + uint64_t chosenPredicateIndex = 0; + for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) { + if (refinementPredicateIndexToCount[index] > refinementPredicateIndexToCount[chosenPredicateIndex]) { + chosenPredicateIndex = index; + } } + newPredicate = possibleRefinementPredicates[chosenPredicateIndex]; + STORM_LOG_DEBUG("Derived new predicate (based on weakest-precondition): " << newPredicate << ", (equivalent to " << (refinementPredicateIndexToCount[chosenPredicateIndex] - 1) << " other refinement predicates)."); + } else { + newPredicate = possibleRefinementPredicates.front(); + STORM_LOG_DEBUG("Derived new predicate (based on weakest-precondition): " << newPredicate << "."); } - newPredicate = possibleRefinementPredicates[chosenPredicateIndex]; STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation."); - STORM_LOG_DEBUG("Derived new predicate (based on weakest-precondition): " << newPredicate << ", (equivalent to " << (refinementPredicateIndexToCount[chosenPredicateIndex] - 1) << " other refinement predicates)"); } return RefinementPredicates(fromGuard ? RefinementPredicates::Source::Guard : RefinementPredicates::Source::WeakestPrecondition, {newPredicate}); @@ -633,6 +644,9 @@ namespace storm { template boost::optional derivePredicatesFromInterpolation(storm::expressions::ExpressionManager& interpolationManager, AbstractionInformation const& abstractionInformation, std::vector> const& trace, std::map const& variableSubstitution) { + + auto start = std::chrono::high_resolution_clock::now(); + boost::optional predicates; // Create solver and interpolation groups. storm::solver::MathsatSmtSolver interpolatingSolver(interpolationManager, storm::solver::MathsatSmtSolver::Options(true, false, true)); @@ -671,16 +685,15 @@ namespace storm { STORM_LOG_DEBUG("Derived new predicate (based on interpolation at step " << step << " out of " << stepCounter << "): " << interpolant); interpolants.push_back(interpolant); } -// else { -// STORM_LOG_ASSERT(step == 0false, "The found interpolant (based on interpolation at step " << step << " out of " << stepCounter << ") is '" << interpolant << "', which shouldn't happen."); -// } } - return boost::make_optional(RefinementPredicates(RefinementPredicates::Source::Interpolation, interpolants)); + predicates = boost::make_optional(RefinementPredicates(RefinementPredicates::Source::Interpolation, interpolants)); } else { STORM_LOG_TRACE("Trace formula is satisfiable, not using interpolation."); } - - return boost::none; + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Deriving predicates using interpolation from witness of size " << trace.size() << " took " << std::chrono::duration_cast(end - start).count() << "ms."); + + return predicates; } template @@ -843,6 +856,8 @@ namespace storm { bool foundPivotState = false; ValueType pivotStateDeviation = storm::utility::zero(); auto const& player2Grouping = transitionMatrix.getRowGroupIndices(); + + uint64_t pivotStates = 0; while (!dijkstraQueue.empty()) { auto distanceStatePair = *dijkstraQueue.begin(); @@ -878,6 +893,7 @@ namespace storm { } // If it is indeed a pivot state, we can abort the search here. if (isPivotState) { + if (considerDeviation && foundPivotState) { ValueType deviationOfCurrentState = (*upperValues)[currentState] - (*lowerValues)[currentState]; if (deviationOfCurrentState > pivotStateDeviation) { @@ -913,7 +929,7 @@ namespace storm { } ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one(); - if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) { + if (probabilityDistances ? alternateDistance > distances[player1Successor] : alternateDistance < distances[player1Successor]) { distances[player1Successor] = alternateDistance; if (generatePredecessors) { result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[minPlayer2Successor]); @@ -934,7 +950,7 @@ namespace storm { } ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one(); - if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) { + if (probabilityDistances ? alternateDistance > distances[player1Successor] : !probabilityDistances && alternateDistance < distances[player1Successor]) { distances[player1Successor] = alternateDistance; if (generatePredecessors) { result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[maxPlayer2Successor]); @@ -945,6 +961,12 @@ namespace storm { } } + std::cout << "found " << pivotStates << " pivots" << std::endl; + + if (foundPivotState) { + return result; + } + // If we arrived at this point, we have explored all relevant states, but none of them was a pivot state, // which can happen when trying to refine using the qualitative result only. return boost::none; @@ -1004,6 +1026,7 @@ namespace storm { maxPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size()); } } + auto end = std::chrono::high_resolution_clock::now(); boost::optional predicates; if (useInterpolation) { @@ -1012,6 +1035,7 @@ namespace storm { if (!predicates) { predicates = derivePredicatesFromPivotState(game, symbolicPivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); } + end = std::chrono::high_resolution_clock::now(); STORM_LOG_THROW(static_cast(predicates), storm::exceptions::InvalidStateException, "Predicates needed to continue."); std::vector preparedPredicates = preprocessPredicates(predicates.get().getPredicates(), predicates.get().getSource()); @@ -1027,11 +1051,7 @@ namespace storm { boost::optional> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, player1Labeling, initialStates, relevantStates, targetStates, minStrategyPair, maxStrategyPair, &quantitativeResult.getMin().getValues(), &quantitativeResult.getMax().getValues()); - // If there was no pivot state, continue the search. - if (!optionalPivotStateResult) { - STORM_LOG_TRACE("Did not find pivot state in qualitative fragment."); - return false; - } + STORM_LOG_THROW(optionalPivotStateResult, storm::exceptions::InvalidStateException, "Did not find pivot state to proceed."); // Otherwise, we can refine. auto const& pivotStateResult = optionalPivotStateResult.get(); @@ -1121,6 +1141,12 @@ namespace storm { return true; } + struct VariableSetHash { + std::size_t operator()(std::set const& set) const { + return set.size(); + } + }; + template std::vector MenuGameRefiner::preprocessPredicates(std::vector const& predicates, RefinementPredicates::Source const& source) const { bool split = source == RefinementPredicates::Source::WeakestPrecondition && splitPredicates; @@ -1128,37 +1154,80 @@ namespace storm { split |= splitAll; if (split) { + auto start = std::chrono::high_resolution_clock::now(); AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); std::vector cleanedAtoms; + std::unordered_map, std::vector, VariableSetHash> predicateClasses; + for (auto const& predicate : predicates) { - // Split the predicates. std::vector atoms = splitter.split(predicate); - // Check which of the atoms are redundant in the sense that they are equivalent to a predicate we already have. + // Put the atoms into the right class. for (auto const& atom : atoms) { - // Check whether the newly found atom is equivalent to an atom we already have in the predicate - // set or in the set that is to be added. - bool addAtom = true; - for (auto const& oldPredicate : abstractionInformation.getPredicates()) { - if (equivalenceChecker.areEquivalent(atom, oldPredicate) || equivalenceChecker.areEquivalent(atom, !oldPredicate)) { - addAtom = false; + std::set vars = atom.getVariables(); + predicateClasses[vars].push_back(atom); + } + } + + // Now clean the classes in the sense that redundant predicates are cleaned. + for (auto& predicateClass : predicateClasses) { + std::vector cleanedAtomsOfClass; + + for (auto const& predicate : predicateClass.second) { + bool addPredicate = true; + for (auto const& atom : cleanedAtomsOfClass) { + if (predicate.areSame(atom)) { + addPredicate = false; break; } - } - for (auto const& addedAtom : cleanedAtoms) { - if (equivalenceChecker.areEquivalent(addedAtom, atom) || equivalenceChecker.areEquivalent(addedAtom, !atom)) { - addAtom = false; + + if (addPredicate && equivalenceChecker.areEquivalentModuloNegation(predicate, atom)) { + addPredicate = false; break; } } - - if (addAtom) { - cleanedAtoms.push_back(atom); + if (addPredicate) { + cleanedAtomsOfClass.push_back(predicate); } } + + predicateClass.second = std::move(cleanedAtomsOfClass); + } + + std::unordered_map, std::vector, VariableSetHash> oldPredicateClasses; + for (auto const& oldPredicate : abstractionInformation.getPredicates()) { + std::set vars = oldPredicate.getVariables(); + + oldPredicateClasses[vars].push_back(oldPredicate); + } + + for (auto const& predicateClass : predicateClasses) { + auto oldPredicateClassIt = oldPredicateClasses.find(predicateClass.first); + if (oldPredicateClassIt != oldPredicateClasses.end()) { + for (auto const& newAtom : predicateClass.second) { + for (auto const& oldPredicate : oldPredicateClassIt->second) { + bool addAtom = true; + if (newAtom.areSame(oldPredicate)) { + addAtom = false; + break; + } + if (equivalenceChecker.areEquivalentModuloNegation(newAtom, oldPredicate)) { + addAtom = false; + break; + } + if (addAtom) { + cleanedAtoms.push_back(newAtom); + } + } + } + } else { + cleanedAtoms.insert(cleanedAtoms.end(), predicateClass.second.begin(), predicateClass.second.end()); + } } + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Preprocessing predicates took " << std::chrono::duration_cast(end - start).count() << "ms."); return cleanedAtoms; } else { diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index a38ec0bf0..1db5ed8df 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -78,7 +78,7 @@ namespace storm { ExplicitPivotStateResult() = default; uint64_t pivotState; - + /// The distance with which the state in question is reached. ValueType distance; @@ -177,6 +177,9 @@ namespace storm { /// A flag indicating whether predicates derived from weakest preconditions shall be split before using them for refinement. bool splitPredicates; + /// A flag indicating whether predicates are to be ranked. + bool rankPredicates; + /// A flag indicating whether all guards have been used to refine the abstraction. bool addedAllGuardsFlag; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 718207120..e7bfe8522 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -81,7 +81,7 @@ namespace storm { STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool."); predicateIndices.push_back(abstractionInformation.getOrAddPredicate(predicate)); } - + // Refine all abstract modules. for (auto& module : modules) { module.refine(predicateIndices); @@ -171,27 +171,29 @@ namespace storm { storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); - + + // Cut transition relation to the reachable states for backward search. + transitionRelation &= reachableStates; + relevantStatesWatch.start(); if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) { - // Cut transition relation to the reachable states for backward search. - transitionRelation &= reachableStates; - + // Get the target state BDD. 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. 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 || reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + // Cut the transition relation to the 'extended backward reachable states', so we have the appropriate self- // loops of (now) deadlock states. transitionRelation &= reachableStates; - - // Include all successors of reachable states, because the backward search otherwise potentially - // cuts probability 0 choices of these states. - reachableStates |= reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + relevantStatesWatch.stop(); - + STORM_LOG_TRACE("Restricting to relevant states took " << relevantStatesWatch.getTimeInMilliseconds() << "ms."); } @@ -212,7 +214,7 @@ namespace storm { bool hasBottomStates = !bottomStateResult.states.isZero(); // Construct the transition matrix by cutting away the transitions of unreachable states. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd(); + storm::dd::Add transitionMatrix = (game.bdd && reachableStates && reachableStates.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs())).template toAdd(); transitionMatrix *= commandUpdateProbabilitiesAdd; transitionMatrix += deadlockTransitions; diff --git a/src/storm/adapters/GmmxxAdapter.cpp b/src/storm/adapters/GmmxxAdapter.cpp index 4210a00ee..ee5873eea 100644 --- a/src/storm/adapters/GmmxxAdapter.cpp +++ b/src/storm/adapters/GmmxxAdapter.cpp @@ -13,7 +13,7 @@ namespace storm { template std::unique_ptr> GmmxxAdapter::toGmmxxSparseMatrix(storm::storage::SparseMatrix const& matrix) { uint_fast64_t realNonZeros = matrix.getEntryCount(); - STORM_LOG_DEBUG("Converting " << matrix.getRowCount() << "x" << matrix.getColumnCount() << " matrix with " << realNonZeros << " non-zeros to gmm++ format."); + STORM_LOG_TRACE("Converting " << matrix.getRowCount() << "x" << matrix.getColumnCount() << " matrix with " << realNonZeros << " non-zeros to gmm++ format."); // Prepare the resulting matrix. std::unique_ptr> result(new gmm::csr_matrix(matrix.getRowCount(), matrix.getColumnCount())); @@ -37,7 +37,7 @@ namespace storm { std::swap(result->ir, columns); std::swap(result->pr, values); - STORM_LOG_DEBUG("Done converting matrix to gmm++ format."); + STORM_LOG_TRACE("Done converting matrix to gmm++ format."); return result; } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index bd77c5cd5..a1900236c 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -54,6 +54,7 @@ namespace storm { using storm::abstraction::ExplicitQuantitativeResult; using storm::abstraction::ExplicitQuantitativeResultMinMax; using storm::abstraction::ExplicitGameStrategyPair; + using detail::PreviousExplicitResult; template GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()) { @@ -62,13 +63,16 @@ namespace storm { storm::prism::Program const& originalProgram = model.asPrismProgram(); STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); + auto flattenStart = std::chrono::high_resolution_clock::now(); // Flatten the modules if there is more than one. if (originalProgram.getNumberOfModules() > 1) { preprocessedModel = originalProgram.flattenModules(this->smtSolverFactory); } else { preprocessedModel = originalProgram; } - + auto flattenEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Flattened model in " << std::chrono::duration_cast(flattenEnd - flattenStart).count() << "ms."); + STORM_LOG_TRACE("Game-based model checker got program " << preprocessedModel.asPrismProgram()); } else { storm::jani::Model const& originalModel = model.asJaniModel(); @@ -391,22 +395,31 @@ namespace storm { } template - ExplicitQuantitativeResult computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& strategyPair, ExplicitQuantitativeResult const* startingQuantitativeResult = nullptr, ExplicitGameStrategyPair const* startingStrategyPair = nullptr) { + ExplicitQuantitativeResult computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& strategyPair, storm::dd::Odd const& odd, ExplicitQuantitativeResult const* startingQuantitativeResult = nullptr, ExplicitGameStrategyPair const* startingStrategyPair = nullptr, boost::optional> const& previousResult = boost::none) { bool player2Min = player2Direction == storm::OptimizationDirection::Minimize; auto const& player1Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer1States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer1States(); auto const& player2Prob0States = player2Min ? qualitativeResult.getProb0Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb0Max().asExplicitQualitativeGameResult().getPlayer2States(); auto const& player2Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer2States(); - // If there are no maybe states, we construct the quantitative result from the qualitative result alone. + ExplicitQuantitativeResult result(maybeStates.size()); + storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one()); + + // If there are no maybe states, there is nothing we need to solve. if (maybeStates.empty()) { - ExplicitQuantitativeResult result(maybeStates.size()); - storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one()); return result; } + + // If there is a previous result, unpack the previous values with respect to the new ODD. + if (previousResult) { + previousResult.get().odd.oldToNewIndex(odd, [&previousResult,&result,player2Min] (uint64_t oldOffset, uint64_t newOffset) { + result.getValues()[newOffset] = player2Min ? previousResult.get().values.getMin().getValues()[oldOffset] : previousResult.get().values.getMax().getValues()[oldOffset]; + }); + } // Otherwise, we need to solve a (sub)game. - + STORM_LOG_TRACE("Solving " << maybeStates.getNumberOfSetBits()<< " maybe states."); + // Create the game by selecting all maybe player 2 states (non-prob0/1) of all maybe player 1 states. std::vector subPlayer1Groups(maybeStates.getNumberOfSetBits() + 1); uint64_t position = 0; @@ -440,6 +453,10 @@ namespace storm { if (startingQuantitativeResult) { storm::utility::vector::selectVectorValues(values, maybeStates, startingQuantitativeResult->getValues()); } + if (previousResult) { + STORM_LOG_ASSERT(!startingQuantitativeResult, "Cannot take two different hints."); + storm::utility::vector::selectVectorValues(values, maybeStates, result.getValues()); + } // Prepare scheduler storage. std::vector player1Scheduler(subPlayer1Groups.size() - 1); @@ -473,9 +490,7 @@ namespace storm { // Solve actual game and track schedulers. gameSolver->solveGame(env, player1Direction, player2Direction, values, b, &player1Scheduler, &player2Scheduler); - // Create combined result for all states. - ExplicitQuantitativeResult result(maybeStates.size()); - storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one()); + // Set values according to quantitative result (qualitative result has already been taken care of). storm::utility::vector::setVectorValues(result.getValues(), maybeStates, values); // Obtain strategies from solver and fuse them with the pre-existing strategy pair for the qualitative result. @@ -526,19 +541,19 @@ namespace storm { } abstractor->addTerminalStates(targetStateExpression); abstractor->setTargetStates(targetStateExpression); + // Create a refiner that can be used to refine the abstraction when needed. storm::abstraction::MenuGameRefiner refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager())); refiner.refine(initialPredicates); - + storm::dd::Bdd globalConstraintStates = abstractor->getStates(constraintExpression); storm::dd::Bdd globalTargetStates = abstractor->getStates(targetStateExpression); // Enter the main-loop of abstraction refinement. boost::optional> previousSymbolicQualitativeResult = boost::none; boost::optional> previousSymbolicMinQuantitativeResult = boost::none; - boost::optional previousExplicitQualitativeResult = boost::none; - // boost::optional> previousExplicitMinQuantitativeResult = boost::none; + boost::optional> previousExplicitResult = boost::none; for (uint_fast64_t iterations = 0; iterations < maximalNumberOfAbstractions; ++iterations) { auto iterationStart = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Starting iteration " << iterations << "."); @@ -568,7 +583,7 @@ namespace storm { if (solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Dd) { result = performSymbolicAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousSymbolicQualitativeResult, previousSymbolicMinQuantitativeResult); } else { - result = performExplicitAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousExplicitQualitativeResult); + result = performExplicitAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousExplicitResult); } if (result) { @@ -684,7 +699,7 @@ namespace storm { } template - std::unique_ptr GameBasedMdpModelChecker::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStatesBdd, storm::dd::Bdd const& constraintStatesBdd, storm::dd::Bdd const& targetStatesBdd, storm::abstraction::MenuGameRefiner const& refiner, boost::optional& previousQualitativeResult) { + std::unique_ptr GameBasedMdpModelChecker::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStatesBdd, storm::dd::Bdd const& constraintStatesBdd, storm::dd::Bdd const& targetStatesBdd, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousResult) { STORM_LOG_TRACE("Using sparse solving."); // (0) Start by transforming the necessary symbolic elements to explicit ones. @@ -749,7 +764,7 @@ namespace storm { // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). auto qualitativeStart = std::chrono::high_resolution_clock::now(); - ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, minStrategyPair, maxStrategyPair); + ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousResult, odd, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, minStrategyPair, maxStrategyPair); std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); if (result) { return result; @@ -782,22 +797,23 @@ namespace storm { return std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); } + ExplicitQuantitativeResultMinMax quantitativeResult; + // (4) if we arrived at this point and no refinement was made, we need to compute the quantitative solution. if (!qualitativeRefinement) { // At this point, we know that we cannot answer the query without further numeric computation. STORM_LOG_TRACE("Starting numerical solution step."); - ExplicitQuantitativeResultMinMax quantitativeResult; - + // (7) Solve the min values and check whether we can give the answer already. auto quantitativeStart = std::chrono::high_resolution_clock::now(); - quantitativeResult.setMin(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair)); + quantitativeResult.setMin(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair, odd, nullptr, nullptr, this->reuseQuantitativeResults ? previousResult : boost::none)); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.getMin().getRange(initialStates)); if (result) { return result; } // (8) Solve the max values and check whether we can give the answer already. - quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, &quantitativeResult.getMin(), &minStrategyPair)); + quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, odd, &quantitativeResult.getMin(), &minStrategyPair)); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.getMax().getRange(initialStates)); if (result) { return result; @@ -821,6 +837,33 @@ namespace storm { refiner.refine(game, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair); auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms."); + + if (this->reuseQuantitativeResults) { + PreviousExplicitResult nextPreviousResult; + nextPreviousResult.values = std::move(quantitativeResult); + 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."); + } } return nullptr; @@ -885,64 +928,17 @@ namespace storm { } template - ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker::computeProb01States(boost::optional const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair) { + ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker::computeProb01States(boost::optional> const& previousResult, storm::dd::Odd const& odd, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair) { ExplicitQualitativeGameResultMinMax result; - -// if (reuseQualitativeResults) { -// // Depending on the player 1 direction, we choose a different order of operations. -// if (player1Direction == storm::OptimizationDirection::Minimize) { -// // (1) min/min: compute prob0 using the game functions -// result.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); -// -// // (2) min/min: compute prob1 using the MDP functions -// storm::dd::Bdd candidates = game.getReachableStates() && !result.prob0Min.player1States; -// storm::dd::Bdd prob1MinMinMdp = storm::utility::graph::performProb1A(game, transitionMatrixBdd, previousQualitativeResult ? previousQualitativeResult.get().prob1Min.player1States : targetStates, candidates); -// -// // (3) min/min: compute prob1 using the game functions -// result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MinMinMdp)); -// -// // (4) min/max: compute prob 0 using the game functions -// result.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); -// -// // (5) min/max: compute prob 1 using the game functions -// // We know that only previous prob1 states can now be prob 1 states again, because the upper bound -// // values can only decrease over iterations. -// boost::optional> prob1Candidates; -// if (previousQualitativeResult) { -// prob1Candidates = previousQualitativeResult.get().prob1Max.player1States; -// } -// result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, prob1Candidates); -// } else { -// // (1) max/max: compute prob0 using the game functions -// result.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); -// -// // (2) max/max: compute prob1 using the MDP functions, reuse prob1 states of last iteration to constrain the candidate states. -// storm::dd::Bdd candidates = game.getReachableStates() && !result.prob0Max.player1States; -// if (previousQualitativeResult) { -// candidates &= previousQualitativeResult.get().prob1Max.player1States; -// } -// storm::dd::Bdd prob1MaxMaxMdp = storm::utility::graph::performProb1E(game, transitionMatrixBdd, constraintStates, targetStates, candidates); -// -// // (3) max/max: compute prob1 using the game functions, reuse prob1 states from the MDP precomputation -// result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, boost::make_optional(prob1MaxMaxMdp)); -// -// // (4) max/min: compute prob0 using the game functions -// result.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); -// -// // (5) max/min: compute prob1 using the game functions, use prob1 from max/max as the candidate set -// result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MaxMaxMdp)); -// } -// } else { - result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair.getPlayer1Strategy(), &minStrategyPair.getPlayer2Strategy()); - result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair.getPlayer1Strategy(), &minStrategyPair.getPlayer2Strategy()); - result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair.getPlayer1Strategy(), &maxStrategyPair.getPlayer2Strategy()); - result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair.getPlayer1Strategy(), &maxStrategyPair.getPlayer2Strategy()); -// } - - STORM_LOG_TRACE("Qualitative precomputation completed."); - STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNumberOfSetBits()<< " 'no', " << result.prob1Min.player1States.getNumberOfSetBits() << " 'yes'."); - STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNumberOfSetBits() << " 'no', " << result.prob1Max.player1States.getNumberOfSetBits() << " 'yes'."); + + result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair); + result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair); + result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair); + result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair); + + STORM_LOG_DEBUG("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNumberOfSetBits()<< " 'no', " << result.prob1Min.player1States.getNumberOfSetBits() << " 'yes'."); + STORM_LOG_DEBUG("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNumberOfSetBits() << " 'no', " << result.prob1Max.player1States.getNumberOfSetBits() << " 'yes'."); return result; } @@ -1003,9 +999,8 @@ namespace storm { result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); } - STORM_LOG_TRACE("Qualitative precomputation completed."); - STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNonZeroCount() << " 'no', " << result.prob1Min.player1States.getNonZeroCount() << " 'yes'."); - STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNonZeroCount() << " 'no', " << result.prob1Max.player1States.getNonZeroCount() << " 'yes'."); + STORM_LOG_DEBUG("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNonZeroCount() << " 'no', " << result.prob1Min.player1States.getNonZeroCount() << " 'yes'."); + STORM_LOG_DEBUG("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNonZeroCount() << " 'no', " << result.prob1Max.player1States.getNonZeroCount() << " 'yes'."); STORM_LOG_ASSERT(checkQualitativeStrategies(result, targetStates), "Qualitative strategies appear to be broken."); return result; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index b54a510c8..0319e48c5 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -6,11 +6,13 @@ #include "storm/storage/prism/Program.h" #include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/Odd.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/abstraction/SymbolicQualitativeGameResult.h" #include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h" +#include "storm/abstraction/ExplicitQuantitativeResult.h" #include "storm/logic/Bound.h" @@ -40,9 +42,6 @@ namespace storm { class ExplicitQualitativeGameResult; class ExplicitQualitativeGameResultMinMax; - template - class ExplicitQuantitativeResult; - template class ExplicitQuantitativeResultMinMax; @@ -56,6 +55,18 @@ namespace storm { using storm::abstraction::SymbolicQualitativeGameResultMinMax; using storm::abstraction::ExplicitQualitativeGameResult; using storm::abstraction::ExplicitQualitativeGameResultMinMax; + using storm::abstraction::ExplicitQuantitativeResult; + using storm::abstraction::ExplicitQuantitativeResultMinMax; + + namespace detail { + template + struct PreviousExplicitResult { + ExplicitQuantitativeResultMinMax values; + std::vector minPlayer1Labels; + std::vector maxPlayer1Labels; + storm::dd::Odd odd; + }; + } template class GameBasedMdpModelChecker : public AbstractModelChecker { @@ -75,7 +86,7 @@ namespace storm { virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityProbabilities(Environment const& env, CheckTask const& checkTask) override; - + private: /*! * Performs the core part of the abstraction-refinement loop. @@ -83,7 +94,7 @@ namespace storm { std::unique_ptr performGameBasedAbstractionRefinement(Environment const& env, CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); std::unique_ptr performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult); - std::unique_ptr performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional& previousQualitativeResult); + std::unique_ptr performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousResult); /*! * Retrieves the initial predicates for the abstraction. @@ -101,7 +112,7 @@ namespace storm { */ SymbolicQualitativeGameResultMinMax computeProb01States(boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); - ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair); + ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional> const& previousResult, storm::dd::Odd const& odd, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair); void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game) const; diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 341571ef6..8a7f92468 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -24,6 +24,7 @@ namespace storm { const std::string AbstractionSettings::restrictToRelevantStatesOptionName = "relevant"; const std::string AbstractionSettings::solveModeOptionName = "solve"; const std::string AbstractionSettings::maximalAbstractionOptionName = "maxabs"; + const std::string AbstractionSettings::rankRefinementPredicatesOptionName = "rankpred"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { std::vector methods = {"games", "bisimulation", "bisim"}; @@ -80,6 +81,11 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) .setDefaultValueString("off").build()) .build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, rankRefinementPredicatesOptionName, true, "Sets whether to rank the refinement predicates if there are multiple.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) + .setDefaultValueString("off").build()) + .build()); } AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const { @@ -166,6 +172,10 @@ namespace storm { return this->getOption(maximalAbstractionOptionName).getArgumentByName("count").getValueAsUnsignedInteger(); } + bool AbstractionSettings::isRankRefinementPredicatesSet() const { + return this->getOption(rankRefinementPredicatesOptionName).getArgumentByName("value").getValueAsString() == "on"; + } + } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 90a7ea668..7fe212fbd 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -116,6 +116,13 @@ namespace storm { */ uint_fast64_t getMaximalAbstractionCount() const; + /* + * Determines whether refinement predicates are to be ranked. + * + * @return True iff the refinement predicates are to be ranked. + */ + bool isRankRefinementPredicatesSet() const; + const static std::string moduleName; private: @@ -130,6 +137,7 @@ namespace storm { const static std::string restrictToRelevantStatesOptionName; const static std::string solveModeOptionName; const static std::string maximalAbstractionOptionName; + const static std::string rankRefinementPredicatesOptionName; }; } diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 3f0f25828..e27fae045 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -970,6 +970,7 @@ namespace storm { // Copy over selected entries. rowGroupCount = 0; index_type rowCount = 0; + subEntries = 0; for (auto index : rowGroupConstraint) { if (!this->hasTrivialRowGrouping()) { matrixBuilder.newRowGroup(rowCount); @@ -985,6 +986,7 @@ namespace storm { matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero()); insertedDiagonalElement = true; } + ++subEntries; matrixBuilder.addNextValue(rowCount, columnBitsSetBeforeIndex[it->getColumn()], it->getValue()); } } diff --git a/src/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index 0a0712b2b..ff3a1a3ef 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -90,6 +90,33 @@ namespace storm { expandValuesToVectorRec(oldOffset + oldOdd.getElseOffset(), oldOdd.getThenSuccessor(), oldValues, newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), newValues); } } + + void Odd::oldToNewIndex(storm::dd::Odd const& newOdd, std::function const& callback) const { + STORM_LOG_ASSERT(this->getHeight() < newOdd.getHeight(), "Expected increase in height."); + oldToNewIndexRec(0, *this, 0, newOdd, callback); + } + + void Odd::oldToNewIndexRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::function const& callback) { + if (oldOdd.getTotalOffset() == 0 || newOdd.getTotalOffset() == 0) { + return; + } + + if (oldOdd.isTerminalNode()) { + if (oldOdd.getThenOffset() != 0) { + if (newOdd.isTerminalNode()) { + if (newOdd.getThenOffset() != 0) { + callback(oldOffset, newOffset); + } + } else { + oldToNewIndexRec(oldOffset, oldOdd, newOffset, newOdd.getElseSuccessor(), callback); + oldToNewIndexRec(oldOffset, oldOdd, newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), callback); + } + } + } else { + oldToNewIndexRec(oldOffset, oldOdd.getElseSuccessor(), newOffset, newOdd.getElseSuccessor(), callback); + oldToNewIndexRec(oldOffset + oldOdd.getElseOffset(), oldOdd.getThenSuccessor(), newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), callback); + } + } void Odd::exportToDot(std::string const& filename) const { std::ofstream dotFile; diff --git a/src/storm/storage/dd/Odd.h b/src/storm/storage/dd/Odd.h index d62bf1844..ac23142f4 100644 --- a/src/storm/storage/dd/Odd.h +++ b/src/storm/storage/dd/Odd.h @@ -5,6 +5,7 @@ #include #include #include +#include namespace storm { namespace storage { @@ -116,6 +117,16 @@ namespace storm { template void expandExplicitVector(storm::dd::Odd const& newOdd, std::vector const& oldValues, std::vector& newValues) const; + /*! + * Translates the indices of the old ODD to that of the new ODD by calling the callback for each old-new + * offset pair. Note that for each old offset, there may be multiple new offsets. The new ODD is expected + * to extend the old ODD by adding layers *at the bottom*. + * + * @param newOdd The new ODD to use. + * @param callback The callback function. + */ + void oldToNewIndex(storm::dd::Odd const& newOdd, std::function const& callback) const; + /*! * Exports the ODD in the dot format to the given file. * @@ -155,6 +166,8 @@ namespace storm { template static void expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector& newValues); + static void oldToNewIndexRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::function const& callback); + // The then- and else-nodes. std::shared_ptr elseNode; std::shared_ptr thenNode; diff --git a/src/storm/storage/expressions/EquivalenceChecker.cpp b/src/storm/storage/expressions/EquivalenceChecker.cpp index c00d4fae6..5d1ffad56 100644 --- a/src/storm/storage/expressions/EquivalenceChecker.cpp +++ b/src/storm/storage/expressions/EquivalenceChecker.cpp @@ -21,14 +21,26 @@ namespace storm { bool EquivalenceChecker::areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second) { this->smtSolver->push(); - this->smtSolver->add((first && !second) || (!first && second)); + this->smtSolver->add(!storm::expressions::iff(first, second)); bool equivalent = smtSolver->check() == storm::solver::SmtSolver::CheckResult::Unsat; this->smtSolver->pop(); return equivalent; } bool EquivalenceChecker::areEquivalentModuloNegation(storm::expressions::Expression const& first, storm::expressions::Expression const& second) { - return this->areEquivalent(first, second) || this->areEquivalent(first, !second); + this->smtSolver->push(); + this->smtSolver->add(!storm::expressions::iff(first, second)); + bool equivalent = smtSolver->check() == storm::solver::SmtSolver::CheckResult::Unsat; + if (equivalent) { + this->smtSolver->pop(); + return true; + } + this->smtSolver->pop(); + this->smtSolver->push(); + this->smtSolver->add(!storm::expressions::iff(first, !second)); + equivalent = smtSolver->check() == storm::solver::SmtSolver::CheckResult::Unsat; + this->smtSolver->pop(); + return equivalent; } } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 6e4c185ea..4844abb83 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -9,7 +9,7 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/DdManager.h" -#include "storm/abstraction/ExplicitGameStrategy.h" +#include "storm/abstraction/ExplicitGameStrategyPair.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/models/symbolic/DeterministicModel.h" @@ -1085,7 +1085,7 @@ namespace storm { } template - ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy) { + ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair) { ExplicitGameProb01Result result(psiStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount())); @@ -1163,7 +1163,7 @@ namespace storm { result.player2States.complement(); // Generate player 1 strategy if required. - if (player1Strategy) { + if (strategyPair) { for (auto player1State : result.player1States) { if (player1Direction == storm::OptimizationDirection::Minimize) { // At least one player 2 successor is a state with probability 0, find it. @@ -1176,16 +1176,16 @@ namespace storm { } } STORM_LOG_ASSERT(foundProb0Successor, "Expected at least one state 2 successor with probability 0."); - player1Strategy->setChoice(player1State, player2State); + strategyPair->getPlayer1Strategy().setChoice(player1State, player2State); } else { // Since all player 2 successors are states with probability 0, just pick any. - player1Strategy->setChoice(player1State, player1Groups[player1State]); + strategyPair->getPlayer1Strategy().setChoice(player1State, player1Groups[player1State]); } } } // Generate player 2 strategy if required. - if (player2Strategy) { + if (strategyPair) { for (auto player2State : result.player2States) { if (player2Direction == storm::OptimizationDirection::Minimize) { // At least one distribution only has successors with probability 0, find it. @@ -1207,10 +1207,10 @@ namespace storm { } STORM_LOG_ASSERT(foundProb0SuccessorDistribution, "Expected at least one distribution with only successors with probability 0."); - player2Strategy->setChoice(player2State, row); + strategyPair->getPlayer2Strategy().setChoice(player2State, row); } else { // Since all player 1 successors are states with probability 0, just pick any. - player2Strategy->setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State]); + strategyPair->getPlayer2Strategy().setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State]); } } } @@ -1286,7 +1286,7 @@ namespace storm { } template - ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy, boost::optional const& player1Candidates) { + ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates) { // During the execution, the two state sets in the result hold the potential player 1/2 states. ExplicitGameProb01Result result; @@ -1349,8 +1349,8 @@ namespace storm { if (addPlayer2State) { player2Solution.set(player2Predecessor); - if (produceStrategiesInIteration && player2Strategy) { - player2Strategy->setChoice(player2Predecessor, validChoice); + if (produceStrategiesInIteration) { + strategyPair->getPlayer2Strategy().setChoice(player2Predecessor, validChoice); } // Check whether the addition of the player 2 state changes the state of the (single) @@ -1377,8 +1377,8 @@ namespace storm { if (addPlayer1State) { player1Solution.set(player1Predecessor); - if (produceStrategiesInIteration && player1Strategy) { - player1Strategy->setChoice(player1Predecessor, validChoice); + if (produceStrategiesInIteration) { + strategyPair->getPlayer1Strategy().setChoice(player1Predecessor, validChoice); } stack.emplace_back(player1Predecessor); @@ -1395,7 +1395,7 @@ namespace storm { // If we were asked to produce strategies, we propagate that by triggering another iteration. // We only do this if at least one strategy will be produced. - produceStrategiesInIteration = !produceStrategiesInIteration && (player1Strategy || player2Strategy); + produceStrategiesInIteration = !produceStrategiesInIteration && strategyPair; } else { result.player1States = player1Solution; result.player2States = player2Solution; @@ -1680,9 +1680,9 @@ namespace storm { template std::pair performProb01Min(storm::models::sparse::NondeterministicModel> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); #endif - template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy); + template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair); - template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy, boost::optional const& player1Candidates); + template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates); template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index e99fd0ba6..3793b42d8 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -50,7 +50,7 @@ namespace storm { } namespace abstraction { - class ExplicitGameStrategy; + class ExplicitGameStrategyPair; } namespace utility { @@ -651,13 +651,11 @@ namespace storm { * @param psiStates The psi states of the model. * @param player1Direction The optimization direction of player 1. * @param player2Direction The optimization direction of player 2. - * @param player1Strategy If not null, a player 1 strategy is synthesized and the corresponding choices - * are written to this strategy. - * @param player2Strategy If not null, a player 2 strategy is synthesized and the corresponding choices + * @param strategyPair If not null, player 1 and t2 strategies are synthesized and the corresponding choices * are written to this strategy. */ template - ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy = nullptr, storm::abstraction::ExplicitGameStrategy* player2Strategy = nullptr); + ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair = nullptr); /*! * Computes the set of states that have probability 1 given the strategies of the two players. @@ -670,14 +668,12 @@ namespace storm { * @param psiStates The psi states of the model. * @param player1Direction The optimization direction of player 1. * @param player2Direction The optimization direction of player 2. - * @param player1Strategy If not null, a player 1 strategy is synthesized and the corresponding choices - * are written to this strategy. - * @param player2Strategy If not null, a player 2 strategy is synthesized and the corresponding choices + * @param strategyPair If not null, player 1 and t2 strategies are synthesized and the corresponding choices * are written to this strategy. * @param player1Candidates If given, this set constrains the candidates of player 1 states that are considered. */ template - ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy = nullptr, storm::abstraction::ExplicitGameStrategy* player2Strategy = nullptr, boost::optional const& player1Candidates = boost::none); + ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair = nullptr, boost::optional const& player1Candidates = boost::none); /*! * Performs a topological sort of the states of the system according to the given transitions.