diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp deleted file mode 100644 index 1f63fcd64..000000000 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp +++ /dev/null @@ -1,576 +0,0 @@ -#include "storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h" - -#include "storm/models/symbolic/Dtmc.h" -#include "storm/models/symbolic/Mdp.h" -#include "storm/models/symbolic/StochasticTwoPlayerGame.h" -#include "storm/models/symbolic/StandardRewardModel.h" - -#include "storm/modelchecker/results/CheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/QuantitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" -#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" -#include "storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h" - -#include "storm/logic/FragmentSpecification.h" - -#include "storm/storage/dd/Bdd.h" -#include "storm/storage/dd/BisimulationDecomposition.h" - -#include "storm/abstraction/QualitativeMdpResultMinMax.h" -#include "storm/abstraction/QualitativeGameResultMinMax.h" -#include "storm/abstraction/QuantitativeGameResult.h" - -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/AbstractionSettings.h" - -#include "storm/solver/SymbolicGameSolver.h" - -#include "storm/utility/macros.h" -#include "storm/exceptions/NotSupportedException.h" -#include "storm/exceptions/InvalidPropertyException.h" -#include "storm/exceptions/NotImplementedException.h" -#include "storm/exceptions/InvalidTypeException.h" - -namespace storm { - namespace modelchecker { - - template - PartialBisimulationMdpModelChecker::PartialBisimulationMdpModelChecker(ModelType const& model) : AbstractModelChecker(), model(model) { - // Intentionally left empty. - } - - template - bool PartialBisimulationMdpModelChecker::canHandle(CheckTask const& checkTask) const { - storm::logic::Formula const& formula = checkTask.getFormula(); - storm::logic::FragmentSpecification fragment = storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true); - return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); - } - - template - std::unique_ptr PartialBisimulationMdpModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { - return computeValuesAbstractionRefinement(checkTask.substituteFormula(checkTask.getFormula())); - } - - template - std::unique_ptr PartialBisimulationMdpModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { - return computeValuesAbstractionRefinement(checkTask.substituteFormula(checkTask.getFormula())); - } - - template - std::unique_ptr PartialBisimulationMdpModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { - STORM_LOG_THROW(rewardMeasureType == storm::logic::RewardMeasureType::Expectation, storm::exceptions::InvalidPropertyException, "Can only compute reward expectations."); - return computeValuesAbstractionRefinement(checkTask.template substituteFormula(checkTask.getFormula())); - } - - template - std::unique_ptr PartialBisimulationMdpModelChecker::computeValuesAbstractionRefinement(CheckTask const& checkTask) { - STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); - - // Create the appropriate preservation information. - storm::dd::bisimulation::PreservationInformation preservationInformation(model, {checkTask.getFormula().asSharedPointer()}); - if (checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward) { - if (!checkTask.isRewardModelSet() || model.hasUniqueRewardModel()) { - preservationInformation.addRewardModel(model.getUniqueRewardModelName()); - } else if (checkTask.isRewardModelSet()) { - preservationInformation.addRewardModel(checkTask.getRewardModel()); - } - } - - // Create a bisimulation object that is used to obtain (partial) quotients. - storm::dd::BisimulationDecomposition bisimulation(this->model, storm::storage::BisimulationType::Strong, preservationInformation); - - auto start = std::chrono::high_resolution_clock::now(); - - uint64_t iterations = 0; - std::unique_ptr result; - while (!result) { - bool fullQuotient = bisimulation.getReachedFixedPoint(); - std::shared_ptr> quotient = bisimulation.getQuotient(); - STORM_LOG_TRACE("Model in iteration " << (iterations + 1) << " has " << quotient->getNumberOfStates() << " states and " << quotient->getNumberOfTransitions() << " transitions."); - - if (fullQuotient) { - STORM_LOG_TRACE("Reached final quotient."); - quotient->printModelInformationToStream(std::cout); - result = computeResultFullQuotient(*quotient, checkTask); - } else { - // Obtain lower and upper bounds from the partial quotient. - std::pair, std::unique_ptr> bounds = computeBoundsPartialQuotient(*quotient, checkTask); - - bool converged = false; - if (!bounds.first && !bounds.second) { - STORM_LOG_TRACE("Did not compute any bounds, skipping convergence check."); - } else { - // If either of the two bounds does not exist, the answer can be derived from the existing bounds. - if (bounds.first == nullptr || bounds.second == nullptr) { - STORM_LOG_ASSERT(bounds.first || bounds.second, "Expected at least one bound."); - STORM_LOG_TRACE("Obtained result on partial quotient."); - quotient->printModelInformationToStream(std::cout); - if (bounds.first) { - return std::move(bounds.first); - } else { - return std::move(bounds.second); - } - } - - // Check whether the bounds are sufficiently close. - converged = checkBoundsSufficientlyClose(bounds); - if (converged) { - result = getAverageOfBounds(bounds); - } - } - - if (!converged) { - STORM_LOG_TRACE("Performing bisimulation step."); - bisimulation.compute(10); - } - } - - ++iterations; - } - - auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Completed abstraction-refinement in " << std::chrono::duration_cast(end - start).count() << "ms."); - - return result; - } - - template - void PartialBisimulationMdpModelChecker::printBoundsInformation(std::pair, std::unique_ptr> const& bounds) { - STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); - storm::modelchecker::SymbolicQuantitativeCheckResult const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult(); - STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); - storm::modelchecker::SymbolicQuantitativeCheckResult const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult(); - - // If there is exactly one value that we stored, we print the current bounds as an interval. - if (lowerBounds.getStates().getNonZeroCount() == 1 && upperBounds.getStates().getNonZeroCount() == 1) { - STORM_LOG_TRACE("Obtained bounds [" << lowerBounds.getValueVector().getMax() << ", " << upperBounds.getValueVector().getMax() << "] on actual result."); - } else { - storm::dd::Add diffs = upperBounds.getValueVector() - lowerBounds.getValueVector(); - storm::dd::Bdd maxDiffRepresentative = diffs.maxAbstractRepresentative(diffs.getContainedMetaVariables()); - - std::pair bounds; - bounds.first = (lowerBounds.getValueVector() * maxDiffRepresentative.template toAdd()).getMax(); - bounds.second = (upperBounds.getValueVector() * maxDiffRepresentative.template toAdd()).getMax(); - - STORM_LOG_TRACE("Largest interval over initial is [" << bounds.first << ", " << bounds.second << "], difference " << (bounds.second - bounds.first) << "."); - } - } - - template - bool PartialBisimulationMdpModelChecker::checkBoundsSufficientlyClose(std::pair, std::unique_ptr> const& bounds) { - STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); - storm::modelchecker::SymbolicQuantitativeCheckResult const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult(); - STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); - storm::modelchecker::SymbolicQuantitativeCheckResult const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult(); - - return lowerBounds.getValueVector().equalModuloPrecision(upperBounds.getValueVector(), storm::settings::getModule().getPrecision(), false); - } - - template - std::unique_ptr PartialBisimulationMdpModelChecker::getAverageOfBounds(std::pair, std::unique_ptr> const& bounds) { - STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); - storm::modelchecker::SymbolicQuantitativeCheckResult const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult(); - STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); - storm::modelchecker::SymbolicQuantitativeCheckResult const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult(); - - return std::make_unique>(lowerBounds.getReachableStates(), lowerBounds.getStates(), (lowerBounds.getValueVector() + upperBounds.getValueVector()) / lowerBounds.getValueVector().getDdManager().getConstant(storm::utility::convertNumber(std::string("2.0")))); - } - - template - typename PartialBisimulationMdpModelChecker::ValueType PartialBisimulationMdpModelChecker::getExtremalBound(storm::OptimizationDirection dir, QuantitativeCheckResult const& result) { - if (dir == storm::OptimizationDirection::Minimize) { - return result.getMin(); - } else { - return result.getMax(); - } - } - - template - bool PartialBisimulationMdpModelChecker::checkForResult(storm::models::Model const& quotient, bool lowerBounds, QuantitativeCheckResult const& result, CheckTask const& checkTask) { - storm::logic::ComparisonType comparisonType = checkTask.getBoundComparisonType(); - ValueType threshold = checkTask.getBoundThreshold(); - - if (lowerBounds) { - if (storm::logic::isLowerBound(comparisonType)) { - ValueType minimalLowerBound = getExtremalBound(storm::OptimizationDirection::Minimize, result); - return (storm::logic::isStrict(comparisonType) && minimalLowerBound > threshold) || (!storm::logic::isStrict(comparisonType) && minimalLowerBound >= threshold); - } else { - ValueType maximalLowerBound = getExtremalBound(storm::OptimizationDirection::Maximize, result); - return (storm::logic::isStrict(comparisonType) && maximalLowerBound >= threshold) || (!storm::logic::isStrict(comparisonType) && maximalLowerBound > threshold); - } - } else { - if (storm::logic::isLowerBound(comparisonType)) { - ValueType minimalUpperBound = getExtremalBound(storm::OptimizationDirection::Minimize, result); - return (storm::logic::isStrict(comparisonType) && minimalUpperBound <= threshold) || (!storm::logic::isStrict(comparisonType) && minimalUpperBound < threshold); - } else { - ValueType maximalUpperBound = getExtremalBound(storm::OptimizationDirection::Maximize, result); - return (storm::logic::isStrict(comparisonType) && maximalUpperBound < threshold) || (!storm::logic::isStrict(comparisonType) && maximalUpperBound <= threshold); - } - } - } - - template - std::unique_ptr PartialBisimulationMdpModelChecker::computeBoundsPartialQuotient(SymbolicMdpPrctlModelChecker>& checker, storm::models::symbolic::Mdp const& quotient, storm::OptimizationDirection const& dir, CheckTask& checkTask) { - - bool rewards = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; - - std::unique_ptr result; - checkTask.setOptimizationDirection(dir); - if (rewards) { - result = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, checkTask); - } else { - result = checker.computeProbabilities(checkTask); - } - STORM_LOG_ASSERT(result, "Expected result."); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotient.getReachableStates(), quotient.getInitialStates())); - return result; - } - - template - template - std::pair::DdType>, storm::dd::Bdd::DdType>> PartialBisimulationMdpModelChecker::getConstraintAndTargetStates(QuotientModelType const& quotient, CheckTask const& checkTask) { - std::pair, storm::dd::Bdd> result; - - SymbolicPropositionalModelChecker checker(quotient); - if (checkTask.getFormula().isUntilFormula()) { - std::unique_ptr subresult = checker.check(checkTask.getFormula().asUntilFormula().getLeftSubformula()); - result.first = subresult->asSymbolicQualitativeCheckResult().getTruthValuesVector(); - subresult = checker.check(checkTask.getFormula().asUntilFormula().getRightSubformula()); - result.second = subresult->asSymbolicQualitativeCheckResult().getTruthValuesVector(); - } else if (checkTask.getFormula().isEventuallyFormula()) { - storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula().asEventuallyFormula(); - result.first = quotient.getReachableStates(); - std::unique_ptr subresult = checker.check(eventuallyFormula.getSubformula()); - result.second = subresult->asSymbolicQualitativeCheckResult().getTruthValuesVector(); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The given formula is not supported by this model checker."); - } - - return result; - } - - template - storm::abstraction::QualitativeMdpResultMinMax::DdType> PartialBisimulationMdpModelChecker::computeQualitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { - - STORM_LOG_DEBUG("Computing qualitative solution for quotient MDP."); - storm::abstraction::QualitativeMdpResultMinMax result; - - auto start = std::chrono::high_resolution_clock::now(); - bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; - storm::dd::Bdd transitionMatrixBdd = quotient.getTransitionMatrix().notZero(); - if (isRewardFormula) { - auto prob1 = storm::utility::graph::performProb1E(quotient, transitionMatrixBdd, constraintStates, targetStates, storm::utility::graph::performProbGreater0E(quotient, transitionMatrixBdd, constraintStates, targetStates)); - result.prob1Min = storm::abstraction::QualitativeMdpResult(prob1); - prob1 = storm::utility::graph::performProb1A(quotient, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(quotient, transitionMatrixBdd, constraintStates, targetStates)); - result.prob1Max = storm::abstraction::QualitativeMdpResult(prob1); - } else { - auto prob01 = storm::utility::graph::performProb01Min(quotient, transitionMatrixBdd, constraintStates, targetStates); - result.prob0Min = storm::abstraction::QualitativeMdpResult(prob01.first); - result.prob1Min = storm::abstraction::QualitativeMdpResult(prob01.second); - prob01 = storm::utility::graph::performProb01Max(quotient, transitionMatrixBdd, constraintStates, targetStates); - result.prob0Max = storm::abstraction::QualitativeMdpResult(prob01.first); - result.prob1Max = storm::abstraction::QualitativeMdpResult(prob01.second); - } - auto end = std::chrono::high_resolution_clock::now(); - - auto timeInMilliseconds = std::chrono::duration_cast(end - start).count(); - STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms."); - - return result; - } - - template - storm::abstraction::QualitativeGameResultMinMax::DdType> PartialBisimulationMdpModelChecker::computeQualitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::OptimizationDirection optimizationDirectionInModel) { - - STORM_LOG_DEBUG("Computing qualitative solution for quotient game."); - storm::abstraction::QualitativeGameResultMinMax result; - - auto start = std::chrono::high_resolution_clock::now(); - bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; - storm::dd::Bdd transitionMatrixBdd = quotient.getTransitionMatrix().notZero(); - if (isRewardFormula) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rewards are currently not supported for quotient stochastic games."); - } else { - result.prob0Min = storm::utility::graph::performProb0(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Minimize, optimizationDirectionInModel); - result.prob1Min = storm::utility::graph::performProb1(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Minimize, optimizationDirectionInModel); - result.prob0Max = storm::utility::graph::performProb0(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Maximize, optimizationDirectionInModel); - result.prob1Max = storm::utility::graph::performProb1(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Maximize, optimizationDirectionInModel); - } - auto end = std::chrono::high_resolution_clock::now(); - - auto timeInMilliseconds = std::chrono::duration_cast(end - start).count(); - STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms."); - - return result; - } - - template - std::unique_ptr PartialBisimulationMdpModelChecker::checkForResult(storm::models::symbolic::Model const& quotient, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask) { - std::unique_ptr result; - - bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; - if (isRewardFormula) { - // In the reachability reward case, we can give an answer if all initial states of the system are infinity - // states in the min result. - if ((quotient.getInitialStates() && !qualitativeResults.getProb1Min().getStates()) == quotient.getInitialStates()) { - result = std::make_unique>(quotient.getReachableStates(), quotient.getInitialStates(), quotient.getInitialStates().ite(quotient.getManager().getConstant(storm::utility::infinity()), quotient.getManager().template getAddZero())); - } - } else { - // In the reachability probability case, we can give the answer if all initial states are prob1 states - // in the min result or if all initial states are prob0 in the max case. - // Furthermore, we can give the answer if there are initial states with probability > 0 in the min case - // and the probability bound was 0 or if there are initial states with probability < 1 in the max case - // and the probability bound was 1. - if ((quotient.getInitialStates() && qualitativeResults.getProb1Min().getStates()) == quotient.getInitialStates()) { - result = std::make_unique>(quotient.getReachableStates(), quotient.getInitialStates(), quotient.getManager().template getAddOne()); - } else if ((quotient.getInitialStates() && qualitativeResults.getProb0Max().getStates()) == quotient.getInitialStates()) { - result = std::make_unique>(quotient.getReachableStates(), quotient.getInitialStates(), quotient.getManager().template getAddZero()); - } else if (checkTask.isBoundSet() && checkTask.getBoundThreshold() == storm::utility::zero() && (quotient.getInitialStates() && qualitativeResults.getProb0Min().getStates()) != quotient.getInitialStates()) { - result = std::make_unique>(quotient.getReachableStates(), quotient.getInitialStates(), (quotient.getInitialStates() && qualitativeResults.getProb0Min().getStates()).ite(quotient.getManager().template getConstant(0.5), quotient.getManager().template getAddZero())); - } else if (checkTask.isBoundSet() && checkTask.getBoundThreshold() == storm::utility::one() && (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates()) != quotient.getInitialStates()) { - result = std::make_unique>(quotient.getReachableStates(), quotient.getInitialStates(), (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates()).ite(quotient.getManager().template getConstant(0.5), quotient.getManager().template getAddZero()) + qualitativeResults.getProb1Max().getStates().template toAdd()); - } - } - - return result; - } - - template - bool PartialBisimulationMdpModelChecker::skipQuantitativeSolution(storm::models::symbolic::Model const& quotient, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask) { - - bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; - if (isRewardFormula) { - if ((quotient.getInitialStates() && qualitativeResults.getProb1Min().getStates()) != (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates())) { - return true; - } - } else { - if ((quotient.getInitialStates() && qualitativeResults.getProb0Min().getStates()) != (quotient.getInitialStates() && qualitativeResults.getProb0Max().getStates())) { - return true; - } else if ((quotient.getInitialStates() && qualitativeResults.getProb1Min().getStates()) != (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates())) { - return true; - } - } - return false; - } - - template - std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeQuantitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults) { - - std::pair, std::unique_ptr> result; - - bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; - if (isRewardFormula) { - storm::dd::Bdd maybeMin = qualitativeResults.getProb1Min().getStates() && quotient.getReachableStates(); - result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Minimize, quotient, quotient.getTransitionMatrix(), quotient.getTransitionMatrix().notZero(), checkTask.isRewardModelSet() ? quotient.getRewardModel(checkTask.getRewardModel()) : quotient.getRewardModel(""), maybeMin, targetStates, !qualitativeResults.getProb1Min().getStates() && quotient.getReachableStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), quotient.getManager().template getAddZero()); - - storm::dd::Bdd maybeMax = qualitativeResults.getProb1Max().getStates() && quotient.getReachableStates(); - result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Maximize, quotient, quotient.getTransitionMatrix(), quotient.getTransitionMatrix().notZero(), checkTask.isRewardModelSet() ? quotient.getRewardModel(checkTask.getRewardModel()) : quotient.getRewardModel(""), maybeMin, targetStates, !qualitativeResults.getProb1Max().getStates() && quotient.getReachableStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), quotient.getManager().template getAddZero())); - } else { - storm::dd::Bdd maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && quotient.getReachableStates(); - result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Minimize, quotient, quotient.getTransitionMatrix(), maybeMin, qualitativeResults.getProb1Min().getStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), quotient.getManager().template getAddZero()); - - storm::dd::Bdd maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && quotient.getReachableStates(); - result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Maximize, quotient, quotient.getTransitionMatrix(), maybeMax, qualitativeResults.getProb1Max().getStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), quotient.getManager().template getAddZero())); - } - - return result; - } - - template - std::unique_ptr computeReachabilityProbabilitiesHelper(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& prob1States) { - - STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << "."); - - // Compute the ingredients of the equation system. - storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); - storm::dd::Add submatrix = maybeStatesAdd * quotient.getTransitionMatrix(); - storm::dd::Add prob1StatesAsColumn = prob1States.template toAdd().swapVariables(quotient.getRowColumnMetaVariablePairs()); - storm::dd::Add subvector = submatrix * prob1StatesAsColumn; - subvector = subvector.sumAbstract(quotient.getColumnVariables()); - - // Cut away all columns targeting non-maybe states. - submatrix *= maybeStatesAdd.swapVariables(quotient.getRowColumnMetaVariablePairs()); - - // Initialize the starting vector. - storm::dd::Add startVector = quotient.getManager().template getAddZero(); - - // Create the solver and solve the equation system. - storm::solver::SymbolicGameSolverFactory solverFactory; - std::unique_ptr> solver = solverFactory.create(submatrix, maybeStates, quotient.getIllegalPlayer1Mask(), quotient.getIllegalPlayer2Mask(), quotient.getRowVariables(), quotient.getColumnVariables(), quotient.getRowColumnMetaVariablePairs(), quotient.getPlayer1Variables(), quotient.getPlayer2Variables()); - auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector); - - return std::make_unique>(quotient.getReachableStates(), prob1States.template toAdd() + values); - } - - template - std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults) { - - std::pair, std::unique_ptr> result; - - bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; - if (isRewardFormula) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Computing rewards for stochastic games is currently unsupported."); - } else { - storm::dd::Bdd maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && quotient.getReachableStates(); - result.first = computeReachabilityProbabilitiesHelper(quotient, storm::OptimizationDirection::Minimize, checkTask.getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Min().getStates()); - - storm::dd::Bdd maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && quotient.getReachableStates(); - result.second = computeReachabilityProbabilitiesHelper(quotient, storm::OptimizationDirection::Maximize, checkTask.getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Max().getStates()); - } - - return result; - } - - template - std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeBoundsPartialQuotient(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask) { - std::pair, std::unique_ptr> result; - - // We go through two phases. In phase (1) we are solving the qualitative part and in phase (2) the quantitative part. - - // Preparation: determine the constraint states and the target states of the reachability objective. - std::pair, storm::dd::Bdd> constraintTargetStates = getConstraintAndTargetStates(quotient, checkTask); - - // Phase (1): solve qualitatively. - storm::abstraction::QualitativeMdpResultMinMax qualitativeResults = computeQualitativeResult(quotient, checkTask, constraintTargetStates.first, constraintTargetStates.second); - - // Check whether the answer can be given after the qualitative solution. - result.first = checkForResult(quotient, qualitativeResults, checkTask); - if (result.first) { - return result; - } - - // Check whether we should skip the quantitative solution (for example if there are initial states for which - // the value is already known to be different at this point. - bool doSkipQuantitativeSolution = skipQuantitativeSolution(quotient, qualitativeResults, checkTask); - STORM_LOG_TRACE("" << (doSkipQuantitativeSolution ? "Skipping" : "Not skipping") << " quantitative solution."); - - // Phase (2): solve quantitatively. - if (!doSkipQuantitativeSolution) { - result = computeQuantitativeResult(quotient, checkTask, constraintTargetStates.first, constraintTargetStates.second, qualitativeResults); - - storm::modelchecker::SymbolicQualitativeCheckResult initialStateFilter(quotient.getReachableStates(), quotient.getInitialStates()); - result.first->filter(initialStateFilter); - result.second->filter(initialStateFilter); - printBoundsInformation(result); - - // Check whether the answer can be given after the quantitative solution. - if (checkForResult(quotient, true, result.first->asQuantitativeCheckResult(), checkTask)) { - result.second = nullptr; - } - if (checkForResult(quotient, false, result.second->asQuantitativeCheckResult(), checkTask)) { - result.first = nullptr; - } - } - return result; - } - - template - std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask) { - std::pair, std::unique_ptr> result; - - // We go through two phases. In phase (1) we are solving the qualitative part and in phase (2) the quantitative part. - - // Preparation: determine the constraint states and the target states of the reachability objective. - std::pair, storm::dd::Bdd> constraintTargetStates = getConstraintAndTargetStates(quotient, checkTask); - - // Phase (1): solve qualitatively. - storm::abstraction::QualitativeGameResultMinMax qualitativeResults = computeQualitativeResult(quotient, checkTask, constraintTargetStates.first, constraintTargetStates.second, checkTask.getOptimizationDirection()); - - // Check whether the answer can be given after the qualitative solution. - result.first = checkForResult(quotient, qualitativeResults, checkTask); - if (result.first) { - return result; - } - - // Check whether we should skip the quantitative solution (for example if there are initial states for which - // the value is already known to be different at this point. - bool doSkipQuantitativeSolution = skipQuantitativeSolution(quotient, qualitativeResults, checkTask); - STORM_LOG_TRACE("" << (doSkipQuantitativeSolution ? "Skipping" : "Not skipping") << " quantitative solution."); - - // Phase (2): solve quantitatively. - if (!doSkipQuantitativeSolution) { - result = computeQuantitativeResult(quotient, checkTask, constraintTargetStates.first, constraintTargetStates.second, qualitativeResults); - - storm::modelchecker::SymbolicQualitativeCheckResult initialStateFilter(quotient.getReachableStates(), quotient.getInitialStates()); - result.first->filter(initialStateFilter); - result.second->filter(initialStateFilter); - printBoundsInformation(result); - - // Check whether the answer can be given after the quantitative solution. - if (checkForResult(quotient, true, result.first->asQuantitativeCheckResult(), checkTask)) { - result.second = nullptr; - } else if (checkForResult(quotient, false, result.second->asQuantitativeCheckResult(), checkTask)) { - result.first = nullptr; - } - } - return result; - } - - template - std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeBoundsPartialQuotient(storm::models::Model const& quotient, CheckTask const& checkTask) { - - // Sanity checks. - STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient."); - storm::models::ModelType modelType = quotient.getType(); - STORM_LOG_THROW(modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Only MDPs and stochastic games are supported as partial quotients."); - - if (modelType == storm::models::ModelType::Mdp) { - return computeBoundsPartialQuotient(static_cast const&>(quotient), checkTask); - } else { - return computeBoundsPartialQuotient(static_cast const&>(quotient), checkTask); - } - } - - template - std::unique_ptr PartialBisimulationMdpModelChecker::computeResultFullQuotient(storm::models::symbolic::Dtmc const& quotient, CheckTask const& checkTask) { - bool rewards = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; - - SymbolicDtmcPrctlModelChecker> checker(quotient); - std::unique_ptr result; - if (rewards) { - result = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, checkTask); - } else { - result = checker.computeProbabilities(checkTask); - } - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotient.getReachableStates(), quotient.getInitialStates())); - return result; - } - - template - std::unique_ptr PartialBisimulationMdpModelChecker::computeResultFullQuotient(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask) { - bool rewards = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; - - SymbolicMdpPrctlModelChecker> checker(quotient); - std::unique_ptr result; - if (rewards) { - result = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, checkTask); - } else { - result = checker.computeProbabilities(checkTask); - } - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotient.getReachableStates(), quotient.getInitialStates())); - return result; - } - - template - std::unique_ptr PartialBisimulationMdpModelChecker::computeResultFullQuotient(storm::models::Model const& quotient, CheckTask const& checkTask) { - - // Sanity checks. - STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient."); - storm::models::ModelType modelType = quotient.getType(); - STORM_LOG_THROW(modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp, storm::exceptions::NotSupportedException, "Only DTMCs and MDPs supported as full quotients."); - - if (modelType == storm::models::ModelType::Dtmc) { - return computeResultFullQuotient(static_cast const&>(quotient), checkTask); - } else { - return computeResultFullQuotient(static_cast const&>(quotient), checkTask); - } - } - - template class PartialBisimulationMdpModelChecker>; - template class PartialBisimulationMdpModelChecker>; - template class PartialBisimulationMdpModelChecker>; - template class PartialBisimulationMdpModelChecker>; - } -} diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h deleted file mode 100644 index eb129c711..000000000 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h +++ /dev/null @@ -1,112 +0,0 @@ -#pragma once - -#include "storm/modelchecker/AbstractModelChecker.h" - -#include "storm/storage/dd/DdType.h" - -#include "storm/solver/OptimizationDirection.h" - -namespace storm { - namespace dd { - template - class Bdd; - } - - namespace models { - template - class Model; - - namespace symbolic { - template - class Model; - - template - class Dtmc; - - template - class Mdp; - - template - class StochasticTwoPlayerGame; - } - } - - namespace abstraction { - template - class SymbolicQualitativeResultMinMax; - - template - class QualitativeMdpResultMinMax; - - template - class QualitativeGameResultMinMax; - } - - namespace modelchecker { - template - class SymbolicMdpPrctlModelChecker; - - template - class QuantitativeCheckResult; - - template - class PartialBisimulationMdpModelChecker : public AbstractModelChecker { - public: - typedef typename ModelType::ValueType ValueType; - static const storm::dd::DdType DdType = ModelType::DdType; - - /*! - * Constructs a model checker for the given model. - */ - explicit PartialBisimulationMdpModelChecker(ModelType const& model); - - /// Overridden methods from super class. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - - private: - std::unique_ptr computeValuesAbstractionRefinement(CheckTask const& checkTask); - - // Methods to check for convergence and postprocessing the result. - bool checkBoundsSufficientlyClose(std::pair, std::unique_ptr> const& bounds); - std::unique_ptr getAverageOfBounds(std::pair, std::unique_ptr> const& bounds); - void printBoundsInformation(std::pair, std::unique_ptr> const& bounds); - - // Methods related to the qualitative solution. - storm::abstraction::QualitativeMdpResultMinMax computeQualitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); - storm::abstraction::QualitativeGameResultMinMax computeQualitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::OptimizationDirection optimizationDirectionInModel); - std::unique_ptr checkForResult(storm::models::symbolic::Model const& quotient, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask); - bool skipQuantitativeSolution(storm::models::symbolic::Model const& quotient, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask); - - // Methods related to the quantitative solution. - std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults); - std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults); - - // Retrieves the constraint and target states of the quotient wrt. to the formula in the check task. - template - std::pair, storm::dd::Bdd> getConstraintAndTargetStates(QuotientModelType const& quotient, CheckTask const& checkTask); - - // Retrieves the extremal bound (wrt. to the optimization direction) of the quantitative check result. - ValueType getExtremalBound(storm::OptimizationDirection dir, QuantitativeCheckResult const& result); - - // Checks whether the quantitative result is sufficient for answering the query. - bool checkForResult(storm::models::Model const& quotient, bool lowerBounds, QuantitativeCheckResult const& result, CheckTask const& checkTask); - - // Methods to compute bounds on the partial quotient. - std::unique_ptr computeBoundsPartialQuotient(SymbolicMdpPrctlModelChecker>& checker, storm::models::symbolic::Mdp const& quotient, storm::OptimizationDirection const& dir, CheckTask& checkTask); - std::pair, std::unique_ptr> computeBoundsPartialQuotient(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask); - std::pair, std::unique_ptr> computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask); - std::pair, std::unique_ptr> computeBoundsPartialQuotient(storm::models::Model const& quotient, CheckTask const& checkTask); - - // Methods to solve the query on the full quotient. - std::unique_ptr computeResultFullQuotient(storm::models::symbolic::Dtmc const& quotient, CheckTask const& checkTask); - std::unique_ptr computeResultFullQuotient(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask); - std::unique_ptr computeResultFullQuotient(storm::models::Model const& quotient, CheckTask const& checkTask); - - // The non-abstracted model. - ModelType const& model; - }; - } -}