From 330dfb96c7c0e4b5a1f4b7a0909da506aa9fabc0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 6 Nov 2017 16:40:29 +0100 Subject: [PATCH] more work on abstraction-refinement framework --- ...tractAbstractionRefinementModelChecker.cpp | 252 +++++++++++++++--- ...bstractAbstractionRefinementModelChecker.h | 36 ++- ...ationAbstractionRefinementModelChecker.cpp | 68 +++++ ...ulationAbstractionRefinementModelChecker.h | 57 ++++ .../PartialBisimulationMdpModelChecker.cpp | 10 +- .../prctl/SymbolicMdpPrctlModelChecker.cpp | 4 +- .../prctl/SymbolicMdpPrctlModelChecker.h | 4 +- .../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 114 ++++---- .../prctl/helper/SymbolicDtmcPrctlHelper.h | 10 +- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 16 +- .../prctl/helper/SymbolicMdpPrctlHelper.h | 16 +- src/storm/modelchecker/results/CheckResult.h | 2 + .../ExplicitParetoCurveCheckResult.cpp | 5 + .../results/ExplicitParetoCurveCheckResult.h | 3 +- .../ExplicitQualitativeCheckResult.cpp | 12 + .../results/ExplicitQualitativeCheckResult.h | 6 +- .../ExplicitQuantitativeCheckResult.cpp | 15 ++ .../results/ExplicitQuantitativeCheckResult.h | 6 +- .../results/HybridQuantitativeCheckResult.cpp | 5 + .../results/HybridQuantitativeCheckResult.h | 2 + .../results/ParetoCurveCheckResult.cpp | 1 - .../results/ParetoCurveCheckResult.h | 1 - .../results/QualitativeCheckResult.h | 1 + .../results/QuantitativeCheckResult.h | 5 +- .../SymbolicParetoCurveCheckResult.cpp | 5 + .../results/SymbolicParetoCurveCheckResult.h | 2 + .../SymbolicQualitativeCheckResult.cpp | 5 + .../results/SymbolicQualitativeCheckResult.h | 2 + .../SymbolicQuantitativeCheckResult.cpp | 5 + .../results/SymbolicQuantitativeCheckResult.h | 3 +- .../SymbolicMinMaxLinearEquationSolver.cpp | 14 +- .../SymbolicMinMaxLinearEquationSolver.h | 2 +- .../SymbolicMdpPrctlModelCheckerTest.cpp | 8 +- .../SymbolicBisimulationDecompositionTest.cpp | 12 +- 34 files changed, 559 insertions(+), 150 deletions(-) create mode 100644 src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp create mode 100644 src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp index 123a772cc..82461f576 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp @@ -13,8 +13,14 @@ #include "storm/modelchecker/CheckTask.h" #include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h" +#include "storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h" + +#include "storm/solver/SymbolicGameSolver.h" + #include "storm/abstraction/StateSet.h" #include "storm/abstraction/SymbolicStateSet.h" #include "storm/abstraction/QualitativeResultMinMax.h" @@ -119,10 +125,10 @@ namespace storm { STORM_LOG_TRACE("Model in iteration " << iterations << " has " << abstractModel->getNumberOfStates() << " states and " << abstractModel->getNumberOfTransitions() << " transitions (retrieved in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); // Obtain lower and upper bounds from the abstract model. - computeBounds(*abstractModel); + std::pair, std::unique_ptr> bounds = computeBounds(*abstractModel); // Try to derive the final result from the obtained bounds. - result = tryToObtainResultFromBounds(abstractModel, this->bounds); + result = tryToObtainResultFromBounds(*abstractModel, bounds); if (!result) { auto refinementStart = std::chrono::high_resolution_clock::now(); this->refineAbstractModel(); @@ -146,7 +152,7 @@ namespace storm { std::pair, std::unique_ptr> constraintAndTargetStates = getConstraintAndTargetStates(abstractModel); // Phase (1): solve qualitatively. - qualitativeResults = computeQualitativeResult(abstractModel, *constraintAndTargetStates.first, *constraintAndTargetStates.second); + lastQualitativeResults = computeQualitativeResult(abstractModel, *constraintAndTargetStates.first, *constraintAndTargetStates.second); // Check whether the answer can be given after the qualitative solution. result.first = checkForResultAfterQualitativeCheck(abstractModel); @@ -156,60 +162,238 @@ namespace storm { // 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(abstractModel, qualitativeResults, checkTask); + bool doSkipQuantitativeSolution = skipQuantitativeSolution(abstractModel, *lastQualitativeResults); STORM_LOG_TRACE("" << (doSkipQuantitativeSolution ? "Skipping" : "Not skipping") << " quantitative solution."); // Phase (2): solve quantitatively. if (!doSkipQuantitativeSolution) { - result = computeQuantitativeResult(abstractModel, 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(abstractModel, true, result.first->asQuantitativeCheckResult(), checkTask)) { -// result.second = nullptr; -// } -// if (checkForResult(abstractModel, false, result.second->asQuantitativeCheckResult(), checkTask)) { -// result.first = nullptr; -// } + lastBounds = computeQuantitativeResult(abstractModel, *constraintAndTargetStates.first, *constraintAndTargetStates.second, *lastQualitativeResults); + + result = std::make_pair(lastBounds.first->clone(), lastBounds.second->clone()); + filterInitialStates(abstractModel, result); + printBoundsInformation(result); + + // Check whether the answer can be given after the quantitative solution. + if (checkForResultAfterQuantitativeCheck(abstractModel, true, result.first->asQuantitativeCheckResult())) { + result.second = nullptr; + } + if (checkForResultAfterQuantitativeCheck(abstractModel, false, result.second->asQuantitativeCheckResult())) { + result.first = nullptr; + } } else { // In this case, we construct the full results from the qualitative results. + auto symbolicModel = abstractModel.template as>(); + std::unique_ptr lowerBounds = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates(), symbolicModel->getInitialStates().ite(lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates().template toAdd(), symbolicModel->getManager().template getAddZero())); + std::unique_ptr upperBounds = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates(), symbolicModel->getInitialStates().ite(lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates().template toAdd(), symbolicModel->getManager().template getAddZero())); + result = std::make_pair, std::unique_ptr>(std::move(lowerBounds), std::move(upperBounds)); } - // - fullResults = result; - return result; } template - bool AbstractAbstractionRefinementModelChecker::skipQuantitativeSolution(storm::models::Model const& abstractModel) { + bool AbstractAbstractionRefinementModelChecker::checkForResultAfterQuantitativeCheck(storm::models::Model const& abstractModel, bool lowerBounds, QuantitativeCheckResult const& result) { + storm::logic::ComparisonType comparisonType = checkTask->getBoundComparisonType(); + ValueType threshold = checkTask->getBoundThreshold(); + + if (lowerBounds) { + if (storm::logic::isLowerBound(comparisonType)) { + ValueType minimalLowerBound = result.getMin(); + return (storm::logic::isStrict(comparisonType) && minimalLowerBound > threshold) || (!storm::logic::isStrict(comparisonType) && minimalLowerBound >= threshold); + } else { + ValueType maximalLowerBound = result.getMax(); + return (storm::logic::isStrict(comparisonType) && maximalLowerBound >= threshold) || (!storm::logic::isStrict(comparisonType) && maximalLowerBound > threshold); + } + } else { + if (storm::logic::isLowerBound(comparisonType)) { + ValueType minimalUpperBound = result.getMin(); + return (storm::logic::isStrict(comparisonType) && minimalUpperBound <= threshold) || (!storm::logic::isStrict(comparisonType) && minimalUpperBound < threshold); + } else { + ValueType maximalUpperBound = result.getMax(); + return (storm::logic::isStrict(comparisonType) && maximalUpperBound < threshold) || (!storm::logic::isStrict(comparisonType) && maximalUpperBound <= threshold); + } + } + } + + template + void AbstractAbstractionRefinementModelChecker::printBoundsInformation(std::pair, std::unique_ptr>& bounds) { + STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult() && bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::NotSupportedException, "Expected symbolic bounds."); + + printBoundsInformation(bounds.first->asSymbolicQuantitativeCheckResult(), bounds.second->asSymbolicQuantitativeCheckResult()); + } + + template + void AbstractAbstractionRefinementModelChecker::printBoundsInformation(SymbolicQuantitativeCheckResult const& lowerBounds, SymbolicQuantitativeCheckResult const& upperBounds) { + + // 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 + void AbstractAbstractionRefinementModelChecker::filterInitialStates(storm::models::Model const& abstractModel, std::pair, std::unique_ptr>& bounds) { + STORM_LOG_THROW(abstractModel.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expected symbolic model."); + + filterInitialStates(*abstractModel.template as>(), bounds); + } + + template + void AbstractAbstractionRefinementModelChecker::filterInitialStates(storm::models::symbolic::Model const& abstractModel, std::pair, std::unique_ptr>& bounds) { + storm::modelchecker::SymbolicQualitativeCheckResult initialStateFilter(abstractModel.getReachableStates(), abstractModel.getInitialStates()); + bounds.first->filter(initialStateFilter); + bounds.second->filter(initialStateFilter); + } + + template + bool AbstractAbstractionRefinementModelChecker::skipQuantitativeSolution(storm::models::Model const& abstractModel, storm::abstraction::QualitativeResultMinMax const& qualitativeResults) { STORM_LOG_THROW(abstractModel.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expected symbolic model."); - return skipQuantitativeSolution(*abstractModel.template as>()); + return skipQuantitativeSolution(*abstractModel.template as>(), qualitativeResults.asSymbolicQualitativeResultMinMax()); } template - bool AbstractAbstractionRefinementModelChecker::skipQuantitativeSolution(storm::models::symbolic::Model const& abstractModel) { + bool AbstractAbstractionRefinementModelChecker::skipQuantitativeSolution(storm::models::symbolic::Model const& abstractModel, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults) { bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; if (isRewardFormula) { - if ((abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates()) != (abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates())) { + if ((abstractModel.getInitialStates() && qualitativeResults.getProb1Min().getStates()) != (abstractModel.getInitialStates() && qualitativeResults.getProb1Max().getStates())) { return true; } } else { - if ((abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb0Min().getStates()) != (abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb0Max().getStates())) { + if ((abstractModel.getInitialStates() && qualitativeResults.getProb0Min().getStates()) != (abstractModel.getInitialStates() && qualitativeResults.getProb0Max().getStates())) { return true; - } else if ((abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates()) != (abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates())) { + } else if ((abstractModel.getInitialStates() && qualitativeResults.getProb1Min().getStates()) != (abstractModel.getInitialStates() && qualitativeResults.getProb1Max().getStates())) { return true; } } return false; } + template + std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::computeQuantitativeResult(storm::models::Model const& abstractModel, storm::abstraction::StateSet const& constraintStates, storm::abstraction::StateSet const& targetStates, storm::abstraction::QualitativeResultMinMax const& qualitativeResults) { + STORM_LOG_ASSERT(abstractModel.isSymbolicModel(), "Expected symbolic abstract model."); + + return computeQuantitativeResult(*abstractModel.template as>(), constraintStates.asSymbolicStateSet(), targetStates.asSymbolicStateSet(), qualitativeResults.asSymbolicQualitativeResultMinMax()); + } + + template + std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::computeQuantitativeResult(storm::models::symbolic::Model const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults) { + + STORM_LOG_THROW(abstractModel.isOfType(storm::models::ModelType::Dtmc) || abstractModel.isOfType(storm::models::ModelType::Mdp) || abstractModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Abstract model type is not supported."); + + if (abstractModel.isOfType(storm::models::ModelType::Dtmc)) { + return computeQuantitativeResult(*abstractModel.template as>(), constraintStates, targetStates, qualitativeResults); + } else if (abstractModel.isOfType(storm::models::ModelType::Mdp)) { + return computeQuantitativeResult(*abstractModel.template as>(), constraintStates, targetStates, qualitativeResults); + } else { + return computeQuantitativeResult(*abstractModel.template as>(), constraintStates, targetStates, qualitativeResults); + } + } + + // FIXME: reuse previous result + template + std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::computeQuantitativeResult(storm::models::symbolic::Dtmc const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet 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 maybe = qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(); + storm::dd::Add values = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(abstractModel, abstractModel.getTransitionMatrix(), checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybe, targetStates.getStates(), !qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(), storm::solver::GeneralSymbolicLinearEquationSolverFactory(), abstractModel.getManager().template getAddZero()); + + result.first = std::make_unique>(abstractModel.getReachableStates(), values); + result.second = result.first->clone(); + } else { + storm::dd::Bdd maybe = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates(); + storm::dd::Add values = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeUntilProbabilities(abstractModel, abstractModel.getTransitionMatrix(), maybe, qualitativeResults.getProb1Min().getStates(), storm::solver::GeneralSymbolicLinearEquationSolverFactory(), abstractModel.getManager().template getAddZero()); + + result.first = std::make_unique>(abstractModel.getReachableStates(), values); + result.second = result.first->clone(); + } + + return result; + } + + // FIXME: reuse previous result + template + std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::computeQuantitativeResult(storm::models::symbolic::Mdp const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet 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() && abstractModel.getReachableStates(); + result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Minimize, abstractModel, abstractModel.getTransitionMatrix(), abstractModel.getTransitionMatrix().notZero(), checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybeMin, targetStates.getStates(), !qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), abstractModel.getManager().template getAddZero()); + + storm::dd::Bdd maybeMax = qualitativeResults.getProb1Max().getStates() && abstractModel.getReachableStates(); + result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Maximize, abstractModel, abstractModel.getTransitionMatrix(), abstractModel.getTransitionMatrix().notZero(), checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybeMin, targetStates.getStates(), !qualitativeResults.getProb1Max().getStates() && abstractModel.getReachableStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), abstractModel.getManager().template getAddZero())); + } else { + storm::dd::Bdd maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates(); + result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Minimize, abstractModel, abstractModel.getTransitionMatrix(), maybeMin, qualitativeResults.getProb1Min().getStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), abstractModel.getManager().template getAddZero()); + + storm::dd::Bdd maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && abstractModel.getReachableStates(); + result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Maximize, abstractModel, abstractModel.getTransitionMatrix(), maybeMax, qualitativeResults.getProb1Max().getStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), abstractModel.getManager().template getAddZero())); + } + + return result; + } + + // FIXME: reuse previous result + template + std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet 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, "Reward properties are not supported for abstract stochastic games."); + } else { + storm::dd::Bdd maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates(); + result.first = computeReachabilityProbabilitiesHelper(abstractModel, this->getAbstractionPlayer() == 1 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), this->getAbstractionPlayer() == 2 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Min().getStates(), abstractModel.getManager().template getAddZero()); + + storm::dd::Bdd maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && abstractModel.getReachableStates(); + result.second = computeReachabilityProbabilitiesHelper(abstractModel, this->getAbstractionPlayer() == 1 ? storm::OptimizationDirection::Maximize : checkTask->getOptimizationDirection(), this->getAbstractionPlayer() == 2 ? storm::OptimizationDirection::Maximize : checkTask->getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Max().getStates(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), abstractModel.getManager().template getAddZero())); + } + + return result; + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::computeReachabilityProbabilitiesHelper(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& prob1States, storm::dd::Add const& startValues) { + + 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 * abstractModel.getTransitionMatrix(); + storm::dd::Add prob1StatesAsColumn = prob1States.template toAdd().swapVariables(abstractModel.getRowColumnMetaVariablePairs()); + storm::dd::Add subvector = submatrix * prob1StatesAsColumn; + subvector = subvector.sumAbstract(abstractModel.getColumnVariables()); + + // Cut away all columns targeting non-maybe states. + submatrix *= maybeStatesAdd.swapVariables(abstractModel.getRowColumnMetaVariablePairs()); + + // Cut the starting vector to the maybe states of this query. + storm::dd::Add startVector = maybeStates.ite(startValues, abstractModel.getManager().template getAddZero()); + + // Create the solver and solve the equation system. + storm::solver::SymbolicGameSolverFactory solverFactory; + std::unique_ptr> solver = solverFactory.create(submatrix, maybeStates, abstractModel.getIllegalPlayer1Mask(), abstractModel.getIllegalPlayer2Mask(), abstractModel.getRowVariables(), abstractModel.getColumnVariables(), abstractModel.getRowColumnMetaVariablePairs(), abstractModel.getPlayer1Variables(), abstractModel.getPlayer2Variables()); + auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector); + + return std::make_unique>(abstractModel.getReachableStates(), prob1States.template toAdd() + values); + } + template std::unique_ptr AbstractAbstractionRefinementModelChecker::computeQualitativeResult(storm::models::Model const& abstractModel, storm::abstraction::StateSet const& constraintStates, storm::abstraction::StateSet const& targetStates) { STORM_LOG_ASSERT(abstractModel.isSymbolicModel(), "Expected symbolic abstract model."); @@ -264,17 +448,17 @@ namespace storm { storm::dd::Bdd transitionMatrixBdd = abstractModel.getTransitionMatrix().notZero(); if (this->getReuseQualitativeResults()) { if (isRewardFormula) { - auto states = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), qualitativeResults ? qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); + auto states = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); result->prob1Min = storm::abstraction::QualitativeMdpResult(states); states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, targetStates.getStates(), states); result->prob1Max = storm::abstraction::QualitativeMdpResult(states); } else { auto states = storm::utility::graph::performProb0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); result->prob0Max = storm::abstraction::QualitativeMdpResult(states); - states = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), qualitativeResults ? qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); + states = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); result->prob1Max = storm::abstraction::QualitativeMdpResult(states); - states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, qualitativeResults ? qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : targetStates.getStates(), states); + states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : targetStates.getStates(), states); result->prob1Min = storm::abstraction::QualitativeMdpResult(states); states = storm::utility::graph::performProb0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); @@ -360,7 +544,7 @@ namespace storm { // (2) min/min: compute prob1 using the MDP functions storm::dd::Bdd candidates = abstractModel.getReachableStates() && !result->getProb0Min().getStates(); - storm::dd::Bdd prob1MinMinMdp = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, qualitativeResults ? qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : targetStates.getStates(), candidates); + storm::dd::Bdd prob1MinMinMdp = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : targetStates.getStates(), candidates); // (3) min/min: compute prob1 using the game functions result->prob1Min = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, requiresSchedulers, requiresSchedulers, boost::make_optional(prob1MinMinMdp)); @@ -371,7 +555,7 @@ namespace storm { // (5) min/max, max/min: 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. - result->prob1Max = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers, qualitativeResults ? qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates() : boost::optional>()); + result->prob1Max = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers, lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates() : boost::optional>()); } else { // (1) max/max: compute prob0 using the game functions result->prob0Max = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, requiresSchedulers, requiresSchedulers); @@ -379,7 +563,7 @@ namespace storm { // (2) max/max: compute prob1 using the MDP functions, reuse prob1 states of last iteration to constrain the candidate states. storm::dd::Bdd candidates = abstractModel.getReachableStates() && !result->getProb0Max().getStates(); if (this->getReuseQualitativeResults()) { - candidates &= qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates(); + candidates &= lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates(); } storm::dd::Bdd prob1MaxMaxMdp = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), candidates); @@ -407,7 +591,7 @@ namespace storm { std::unique_ptr AbstractAbstractionRefinementModelChecker::checkForResultAfterQualitativeCheck(storm::models::symbolic::Model const& abstractModel) { std::unique_ptr result; - auto const& symbolicQualitativeResultMinMax = qualitativeResults->asSymbolicQualitativeResultMinMax(); + auto const& symbolicQualitativeResultMinMax = lastQualitativeResults->asSymbolicQualitativeResultMinMax(); bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; if (isRewardFormula) { diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h index 9d9f3a7ef..060687ce2 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h @@ -7,6 +7,9 @@ namespace storm { namespace dd { template class Bdd; + + template + class Add; } namespace models { @@ -53,6 +56,9 @@ namespace storm { template class QuantitativeCheckResult; + template + class SymbolicQuantitativeCheckResult; + template class AbstractAbstractionRefinementModelChecker : public AbstractModelChecker { public: @@ -64,7 +70,7 @@ namespace storm { */ explicit AbstractAbstractionRefinementModelChecker(); - ~AbstractAbstractionRefinementModelChecker(); + virtual ~AbstractAbstractionRefinementModelChecker(); /// Overridden methods from super class. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -90,7 +96,7 @@ namespace storm { /// Retrieves the state sets corresponding to the constraint and target states. virtual std::pair, std::unique_ptr> getConstraintAndTargetStates(storm::models::Model const& abstractModel) = 0; - /// Retrieves the index of the abstraction player. Must be in {0} for DTMCs, {1} for MDPs and in {1, 2} for games. + /// Retrieves the index of the abstraction player. Must be in {1} for DTMCs and MDPs and in {1, 2} for games. virtual uint64_t getAbstractionPlayer() const = 0; /// Retrieves whether schedulers need to be computed. @@ -105,8 +111,8 @@ namespace storm { /// Performs the actual abstraction refinement loop. std::unique_ptr performAbstractionRefinement(); - /// Computes lower and upper bounds on the abstract model and stores them in a member. - void computeBounds(storm::models::Model const& abstractModel); + /// Computes lower and upper bounds on the abstract model and returns the bounds for the initial states. + std::pair, std::unique_ptr> computeBounds(storm::models::Model const& abstractModel); /// Solves the current check task qualitatively, i.e. computes all states with probability 0/1. std::unique_ptr computeQualitativeResult(storm::models::Model const& abstractModel, storm::abstraction::StateSet const& constraintStates, storm::abstraction::StateSet const& targetStates); @@ -119,8 +125,19 @@ namespace storm { std::unique_ptr checkForResultAfterQualitativeCheck(storm::models::symbolic::Model const& abstractModel); // Methods related to the quantitative solution. - bool skipQuantitativeSolution(storm::models::Model const& abstractModel); - bool skipQuantitativeSolution(storm::models::symbolic::Model const& abstractModel); + bool skipQuantitativeSolution(storm::models::Model const& abstractModel, storm::abstraction::QualitativeResultMinMax const& qualitativeResults); + bool skipQuantitativeSolution(storm::models::symbolic::Model const& abstractModel, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults); + std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::Model const& abstractModel, storm::abstraction::StateSet const& constraintStates, storm::abstraction::StateSet const& targetStates, storm::abstraction::QualitativeResultMinMax const& qualitativeResults); + std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::Model const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults); + std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::Dtmc const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults); + std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::Mdp const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults); + std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults); + void filterInitialStates(storm::models::Model const& abstractModel, std::pair, std::unique_ptr>& bounds); + void filterInitialStates(storm::models::symbolic::Model const& abstractModel, std::pair, std::unique_ptr>& bounds); + void printBoundsInformation(std::pair, std::unique_ptr>& bounds); + void printBoundsInformation(SymbolicQuantitativeCheckResult const& lowerBounds, SymbolicQuantitativeCheckResult const& upperBounds); + bool checkForResultAfterQuantitativeCheck(storm::models::Model const& abstractModel, bool lowerBounds, QuantitativeCheckResult const& result); + std::unique_ptr computeReachabilityProbabilitiesHelper(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& prob1States, storm::dd::Add const& startValues); /// Tries to obtain the results from the bounds. If either of the two bounds is null, the result is assumed /// to be the non-null bound. If neither is null and the bounds are sufficiently close, the average of the @@ -151,10 +168,11 @@ namespace storm { bool reuseQuantitativeResults; /// The last qualitative results. - std::unique_ptr qualitativeResults; + std::unique_ptr lastQualitativeResults; - /// The last full result that was obtained. - std::pair, std::unique_ptr> bounds; + /// The last full results that were obtained. These results (if there are any) specify the lower and upper + /// bounds for all states in the model. + std::pair, std::unique_ptr> lastBounds; }; } } diff --git a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp new file mode 100644 index 000000000..e3f2c28ed --- /dev/null +++ b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp @@ -0,0 +1,68 @@ +#include "storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h" + +#include "storm/models/symbolic/Dtmc.h" +#include "storm/models/symbolic/Mdp.h" + +namespace storm { + namespace modelchecker { + + template + const std::string BisimulationAbstractionRefinementModelChecker::name = "bisimulation-based astraction refinement"; + + template + BisimulationAbstractionRefinementModelChecker::BisimulationAbstractionRefinementModelChecker(ModelType const& model) : model(model) { + // Intentionally left empty. + } + + template + BisimulationAbstractionRefinementModelChecker::~BisimulationAbstractionRefinementModelChecker() { + // Intentionally left empty. + } + +// template +// bool BisimulationAbstractionRefinementModelChecker::supportsReachabilityRewards() const { +// return true; +// } +// +// template +// std::string const& BisimulationAbstractionRefinementModelChecker::getName() const { +// return name; +// } +// +// template +// void BisimulationAbstractionRefinementModelChecker::initializeAbstractionRefinement() { +// +// } +// +// template +// std::shared_ptr::ValueType>> BisimulationAbstractionRefinementModelChecker::getAbstractModel() { +// +// } +// +// template +// std::pair, std::unique_ptr> BisimulationAbstractionRefinementModelChecker::getConstraintAndTargetStates(storm::models::Model const& abstractModel) { +// +// } +// +// template +// uint64_t BisimulationAbstractionRefinementModelChecker::getAbstractionPlayer() const { +// return 1; +// } +// +// template +// bool BisimulationAbstractionRefinementModelChecker::requiresSchedulerSynthesis() const { +// return false; +// } +// +// template +// void BisimulationAbstractionRefinementModelChecker::refineAbstractModel() { +// +// } + + template class BisimulationAbstractionRefinementModelChecker>; + template class BisimulationAbstractionRefinementModelChecker>; + template class BisimulationAbstractionRefinementModelChecker>; + template class BisimulationAbstractionRefinementModelChecker>; + + } +} diff --git a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h new file mode 100644 index 000000000..c46612dde --- /dev/null +++ b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h @@ -0,0 +1,57 @@ +#pragma once + +#include + +#include "storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h" + +namespace storm { + namespace models { + template + class Model; + } + + namespace dd { + template + class BisimulationDecomposition; + } + + namespace modelchecker { + + template + class BisimulationAbstractionRefinementModelChecker : public AbstractAbstractionRefinementModelChecker { + public: + typedef typename ModelType::ValueType ValueType; + static const storm::dd::DdType DdType = ModelType::DdType; + + /*! + * Constructs a model checker for the given model. + */ + explicit BisimulationAbstractionRefinementModelChecker(ModelType const& model); + + virtual ~BisimulationAbstractionRefinementModelChecker(); + + protected: +// virtual bool supportsReachabilityRewards() const override; +// virtual std::string const& getName() const override; +// virtual void initializeAbstractionRefinement() override; +// virtual std::shared_ptr> getAbstractModel() override; +// virtual std::pair, std::unique_ptr> getConstraintAndTargetStates(storm::models::Model const& abstractModel) override; +// virtual uint64_t getAbstractionPlayer() const override; +// virtual bool requiresSchedulerSynthesis() const override; +// virtual void refineAbstractModel() override; + + private: + ModelType const& model; + + /// The bisimulation object that maintains and refines the model. + std::unique_ptr> bisimulation; + + /// Maintains the last abstract model that was returned. + std::shared_ptr> lastAbstractModel; + + /// The name of the method. + const static std::string name; + }; + + } +} diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp index 4175a2ced..cb2e0c725 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp @@ -362,16 +362,16 @@ namespace storm { 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::SymbolicGeneralMinMaxLinearEquationSolverFactory(), quotient.getManager().template getAddZero()); + 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::SymbolicGeneralMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), quotient.getManager().template getAddZero())); + 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::SymbolicGeneralMinMaxLinearEquationSolverFactory(), quotient.getManager().template getAddZero()); + 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::SymbolicGeneralMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), quotient.getManager().template getAddZero())); + 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; @@ -392,7 +392,7 @@ namespace storm { // Cut away all columns targeting non-maybe states. submatrix *= maybeStatesAdd.swapVariables(quotient.getRowColumnMetaVariablePairs()); - // Cut the starting vector to the maybe states of this query. + // Initialize the starting vector. storm::dd::Add startVector = quotient.getManager().template getAddZero(); // Create the solver and solve the equation system. diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 4f7d0cf34..f442261ec 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -22,12 +22,12 @@ namespace storm { namespace modelchecker { template - SymbolicMdpPrctlModelChecker::SymbolicMdpPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + SymbolicMdpPrctlModelChecker::SymbolicMdpPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } template - SymbolicMdpPrctlModelChecker::SymbolicMdpPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory()) { + SymbolicMdpPrctlModelChecker::SymbolicMdpPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory()) { // Intentionally left empty. } diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index c45544d98..486763307 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -16,7 +16,7 @@ namespace storm { static const storm::dd::DdType DdType = ModelType::DdType; explicit SymbolicMdpPrctlModelChecker(ModelType const& model); - explicit SymbolicMdpPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); + explicit SymbolicMdpPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -31,7 +31,7 @@ namespace storm { private: // An object that is used for retrieving linear equation solvers. - std::unique_ptr> linearEquationSolverFactory; + std::unique_ptr> linearEquationSolverFactory; }; } // namespace modelchecker diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index 28c3f57db..19701eeef 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -19,7 +19,7 @@ namespace storm { namespace helper { template - storm::dd::Add SymbolicDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add SymbolicDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. STORM_LOG_TRACE("Found " << phiStates.getNonZeroCount() << " phi states and " << psiStates.getNonZeroCount() << " psi states."); @@ -35,39 +35,43 @@ namespace storm { } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { - // Create the matrix and the vector for the equation system. - storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); - - // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting - // non-maybe states in the matrix. - storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; - - // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all - // maybe states. - storm::dd::Add prob1StatesAsColumn = statesWithProbability01.second.template toAdd(); - prob1StatesAsColumn = prob1StatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs()); - storm::dd::Add subvector = submatrix * prob1StatesAsColumn; - subvector = subvector.sumAbstract(model.getColumnVariables()); - - // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed - // for solving the equation system (i.e. compute (I-A)). - submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); - if (linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem) { - submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; - } - - // Solve the equation system. - std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - solver->setBounds(storm::utility::zero(), storm::utility::one()); - storm::dd::Add result = solver->solveEquations(model.getManager().template getAddZero(), subvector); - - return statesWithProbability01.second.template toAdd() + result; + return computeUntilProbabilities(model, transitionMatrix, maybeStates, statesWithProbability01.second, linearEquationSolverFactory, startValues ? maybeStates.ite(startValues.get(), model.getManager().template getAddZero()) : model.getManager().template getAddZero()); } else { return statesWithProbability01.second.template toAdd(); } } } + template + storm::dd::Add SymbolicDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& statesWithProbability1, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { + // Create the matrix and the vector for the equation system. + storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); + + // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting + // non-maybe states in the matrix. + storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; + + // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all + // maybe states. + storm::dd::Add prob1StatesAsColumn = statesWithProbability1.template toAdd().swapVariables(model.getRowColumnMetaVariablePairs()); + storm::dd::Add subvector = submatrix * prob1StatesAsColumn; + subvector = subvector.sumAbstract(model.getColumnVariables()); + + // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed + // for solving the equation system (i.e. compute (I-A)). + submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); + if (linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem) { + submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; + } + + // Solve the equation system. + std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); + solver->setBounds(storm::utility::zero(), storm::utility::one()); + storm::dd::Add result = solver->solveEquations(model.getManager().template getAddZero(), subvector); + + return statesWithProbability1.template toAdd() + result; + } + template storm::dd::Add SymbolicDtmcPrctlHelper::computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { storm::dd::Add result = computeUntilProbabilities(model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); @@ -139,7 +143,7 @@ namespace storm { } template - storm::dd::Add SymbolicDtmcPrctlHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add SymbolicDtmcPrctlHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { // Only compute the result if there is at least one reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -158,35 +162,41 @@ namespace storm { } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { - // Create the matrix and the vector for the equation system. - storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); - - // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting - // non-maybe states in the matrix. - storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; - - // Then compute the state reward vector to use in the computation. - storm::dd::Add subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables()); - - // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed - // for solving the equation system (i.e. compute (I-A)). - submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); - if (linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem) { - submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; - } - - // Solve the equation system. - std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - solver->setLowerBound(storm::utility::zero()); - storm::dd::Add result = solver->solveEquations(model.getManager().template getAddZero(), subvector); - - return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result); + return computeReachabilityRewards(model, transitionMatrix, rewardModel, maybeStates, targetStates, infinityStates, linearEquationSolverFactory, startValues ? maybeStates.ite(startValues.get(), model.getManager().template getAddZero()) : model.getManager().template getAddZero()); } else { return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().getConstant(storm::utility::zero())); } } } + template + storm::dd::Add SymbolicDtmcPrctlHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& targetStates, storm::dd::Bdd const& infinityStates, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { + + // Create the matrix and the vector for the equation system. + storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); + + // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting + // non-maybe states in the matrix. + storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; + + // Then compute the state reward vector to use in the computation. + storm::dd::Add subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables()); + + // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed + // for solving the equation system (i.e. compute (I-A)). + submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); + if (linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem) { + submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; + } + + // Solve the equation system. + std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); + solver->setLowerBound(storm::utility::zero()); + storm::dd::Add result = solver->solveEquations(startValues ? startValues.get() : maybeStatesAdd.getDdManager().template getAddZero(), subvector); + + return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result); + } + template class SymbolicDtmcPrctlHelper; template class SymbolicDtmcPrctlHelper; diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h index 58b32b0dc..9deb84bec 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h @@ -21,15 +21,19 @@ namespace storm { static storm::dd::Add computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); - static storm::dd::Add computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); - + static storm::dd::Add computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); + + static storm::dd::Add computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& statesWithProbability1, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); + static storm::dd::Add computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); static storm::dd::Add computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); static storm::dd::Add computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); - static storm::dd::Add computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); + static storm::dd::Add computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); + + static storm::dd::Add computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& targetStates, storm::dd::Bdd const& infinityStates, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); }; } diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index ef6cb561b..2d0056f7e 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -37,7 +37,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& statesWithProbability1, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { + std::unique_ptr SymbolicMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& statesWithProbability1, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { // Create the matrix and the vector for the equation system. storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); @@ -83,7 +83,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { + std::unique_ptr SymbolicMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. std::pair, storm::dd::Bdd> statesWithProbability01; @@ -111,7 +111,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { std::unique_ptr result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); result->asQuantitativeCheckResult().oneMinus(); return result; @@ -129,7 +129,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 or 1 of satisfying the until-formula. storm::dd::Bdd statesWithProbabilityGreater0; @@ -167,7 +167,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -179,7 +179,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -194,7 +194,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& transitionMatrixBdd, RewardModelType const& rewardModel, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& targetStates, storm::dd::Bdd const& infinityStates, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { + std::unique_ptr SymbolicMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& transitionMatrixBdd, RewardModelType const& rewardModel, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& targetStates, storm::dd::Bdd const& infinityStates, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { // Create the matrix and the vector for the equation system. storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); @@ -240,7 +240,7 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { + std::unique_ptr SymbolicMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues) { // Only compute the result if there is at least one reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h index 21eaf80d6..7d64a2295 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h @@ -21,23 +21,23 @@ namespace storm { public: typedef typename storm::models::symbolic::NondeterministicModel::RewardModelType RewardModelType; - static std::unique_ptr computeBoundedUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeBoundedUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); static std::unique_ptr computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); - static std::unique_ptr computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); + static std::unique_ptr computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); - static std::unique_ptr computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& statesWithProbability1, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); + static std::unique_ptr computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& statesWithProbability1, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); - static std::unique_ptr computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); + static std::unique_ptr computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); - static std::unique_ptr computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& transitionMatrixBdd, RewardModelType const& rewardModel, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& targetStates, storm::dd::Bdd const& infinityStates, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); + static std::unique_ptr computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& transitionMatrixBdd, RewardModelType const& rewardModel, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& targetStates, storm::dd::Bdd const& infinityStates, storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& startValues = boost::none); }; } diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h index 43954a220..4edd2cb19 100644 --- a/src/storm/modelchecker/results/CheckResult.h +++ b/src/storm/modelchecker/results/CheckResult.h @@ -38,6 +38,8 @@ namespace storm { public: virtual ~CheckResult() = default; + virtual std::unique_ptr clone() const = 0; + /*! * Filters the current result wrt. to the filter, i.e. only keeps the entries that are selected by the filter. * This means that the filter must be a qualitative result of proper type (symbolic/explicit). diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp index 83568b1c8..8da49418a 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp @@ -25,6 +25,11 @@ namespace storm { // Intentionally left empty. } + template + std::unique_ptr ExplicitParetoCurveCheckResult::clone() const { + return std::make_unique>(this->state, this->points, this->underApproximation, this->overApproximation); + } + template bool ExplicitParetoCurveCheckResult::isExplicitParetoCurveCheckResult() const { return true; diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h index 251102f01..5bc42feff 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h @@ -11,7 +11,6 @@ namespace storm { template class ExplicitParetoCurveCheckResult : public ParetoCurveCheckResult { public: - ExplicitParetoCurveCheckResult(); ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector::point_type> const& points, typename ParetoCurveCheckResult::polytope_type const& underApproximation, typename ParetoCurveCheckResult::polytope_type const& overApproximation); ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector::point_type>&& points, typename ParetoCurveCheckResult::polytope_type&& underApproximation, typename ParetoCurveCheckResult::polytope_type&& overApproximation); @@ -22,6 +21,8 @@ namespace storm { ExplicitParetoCurveCheckResult& operator=(ExplicitParetoCurveCheckResult&& other) = default; virtual ~ExplicitParetoCurveCheckResult() = default; + virtual std::unique_ptr clone() const override; + virtual bool isExplicitParetoCurveCheckResult() const override; virtual bool isExplicit() const override; diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp index 07701d807..8dd14275c 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp @@ -29,6 +29,18 @@ namespace storm { // Intentionally left empty. } + ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(boost::variant const& truthValues) : truthValues(truthValues) { + // Intentionally left empty. + } + + ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(boost::variant&& truthValues) : truthValues(std::move(truthValues)) { + // Intentionally left empty. + } + + std::unique_ptr ExplicitQualitativeCheckResult::clone() const { + return std::make_unique(this->truthValues); + } + void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, bool logicalAnd) { STORM_LOG_THROW(second.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type."); STORM_LOG_THROW(first.isResultForAllStates() == second.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type."); diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h index 02a0eb432..af883e1e0 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h @@ -24,7 +24,9 @@ namespace storm { ExplicitQualitativeCheckResult(storm::storage::sparse::state_type state, bool value); ExplicitQualitativeCheckResult(vector_type const& truthValues); ExplicitQualitativeCheckResult(vector_type&& truthValues); - + ExplicitQualitativeCheckResult(boost::variant const& truthValues); + ExplicitQualitativeCheckResult(boost::variant&& truthValues); + ExplicitQualitativeCheckResult(ExplicitQualitativeCheckResult const& other) = default; ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult const& other) = default; #ifndef WINDOWS @@ -32,6 +34,8 @@ namespace storm { ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult&& other) = default; #endif + virtual std::unique_ptr clone() const override; + bool operator[](storm::storage::sparse::state_type index) const; void setValue(storm::storage::sparse::state_type, bool value); diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index ad1f1e296..a3e7d2f6f 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -42,6 +42,21 @@ namespace storm { // Intentionally left empty. } + template + ExplicitQuantitativeCheckResult::ExplicitQuantitativeCheckResult(boost::variant const& values, boost::optional>> scheduler) : values(values), scheduler(scheduler) { + // Intentionally left empty. + } + + template + ExplicitQuantitativeCheckResult::ExplicitQuantitativeCheckResult(boost::variant&& values, boost::optional>> scheduler) : values(std::move(values)), scheduler(scheduler) { + // Intentionally left empty. + } + + template + std::unique_ptr ExplicitQuantitativeCheckResult::clone() const { + return std::make_unique>(this->values, this->scheduler); + } + template typename ExplicitQuantitativeCheckResult::vector_type const& ExplicitQuantitativeCheckResult::getValueVector() const { return boost::get(values); diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h index 41a0f8477..131cf0cea 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -25,7 +25,9 @@ namespace storm { ExplicitQuantitativeCheckResult(storm::storage::sparse::state_type const& state, ValueType const& value); ExplicitQuantitativeCheckResult(vector_type const& values); ExplicitQuantitativeCheckResult(vector_type&& values); - + ExplicitQuantitativeCheckResult(boost::variant const& values, boost::optional>> scheduler = boost::none); + ExplicitQuantitativeCheckResult(boost::variant&& values, boost::optional>> scheduler = boost::none); + ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult const& other) = default; ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult const& other) = default; #ifndef WINDOWS @@ -34,6 +36,8 @@ namespace storm { #endif virtual ~ExplicitQuantitativeCheckResult() = default; + virtual std::unique_ptr clone() const override; + ValueType& operator[](storm::storage::sparse::state_type state); ValueType const& operator[](storm::storage::sparse::state_type state) const; diff --git a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp index ea6320bda..455212aa9 100644 --- a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -19,6 +19,11 @@ namespace storm { // Intentionally left empty. } + template + std::unique_ptr HybridQuantitativeCheckResult::clone() const { + return std::make_unique>(this->reachableStates, this->symbolicStates, this->symbolicValues, this->explicitStates, this->odd, this->explicitValues); + } + template std::unique_ptr HybridQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { storm::dd::Bdd symbolicResult = symbolicStates; diff --git a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.h b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.h index 9ecc336cf..d8359ba04 100644 --- a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.h @@ -23,6 +23,8 @@ namespace storm { HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult&& other) = default; #endif + virtual std::unique_ptr clone() const override; + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override; std::unique_ptr toExplicitQuantitativeCheckResult() const; diff --git a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp index 26679181a..39ae4e265 100644 --- a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp @@ -41,7 +41,6 @@ namespace storm { return overApproximation; } - template std::ostream& ParetoCurveCheckResult::writeToStream(std::ostream& out) const { out << std::endl; diff --git a/src/storm/modelchecker/results/ParetoCurveCheckResult.h b/src/storm/modelchecker/results/ParetoCurveCheckResult.h index 5f0979f44..e2b3be825 100644 --- a/src/storm/modelchecker/results/ParetoCurveCheckResult.h +++ b/src/storm/modelchecker/results/ParetoCurveCheckResult.h @@ -28,7 +28,6 @@ namespace storm { ParetoCurveCheckResult(std::vector const& points, polytope_type const& underApproximation, polytope_type const& overApproximation); ParetoCurveCheckResult(std::vector&& points, polytope_type&& underApproximation, polytope_type&& overApproximation); - // The pareto optimal points that have been found. std::vector points; diff --git a/src/storm/modelchecker/results/QualitativeCheckResult.h b/src/storm/modelchecker/results/QualitativeCheckResult.h index 3b81c0b0c..bd519fe90 100644 --- a/src/storm/modelchecker/results/QualitativeCheckResult.h +++ b/src/storm/modelchecker/results/QualitativeCheckResult.h @@ -10,6 +10,7 @@ namespace storm { virtual ~QualitativeCheckResult() = default; virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other); virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other); + virtual void complement(); virtual bool existsTrue() const = 0; diff --git a/src/storm/modelchecker/results/QuantitativeCheckResult.h b/src/storm/modelchecker/results/QuantitativeCheckResult.h index 285f60755..46e052d5a 100644 --- a/src/storm/modelchecker/results/QuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/QuantitativeCheckResult.h @@ -10,9 +10,8 @@ namespace storm { virtual ~QuantitativeCheckResult() = default; virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const; - - virtual void oneMinus() = 0; - + + virtual void oneMinus() = 0; virtual ValueType getMin() const = 0; virtual ValueType getMax() const = 0; diff --git a/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp index a2db3593a..59aa7fb0f 100644 --- a/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp @@ -25,6 +25,11 @@ namespace storm { STORM_LOG_THROW(this->state.getNonZeroCount() == 1, storm::exceptions::InvalidOperationException, "ParetoCheckResults are only relevant for a single state."); } + template + std::unique_ptr SymbolicParetoCurveCheckResult::clone() const { + return std::make_unique>(this->state, this->points, this->underApproximation, this->overApproximation); + } + template bool SymbolicParetoCurveCheckResult::isSymbolicParetoCurveCheckResult() const { return true; diff --git a/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.h b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.h index edda08abf..8a711b4af 100644 --- a/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.h +++ b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.h @@ -24,6 +24,8 @@ namespace storm { SymbolicParetoCurveCheckResult& operator=(SymbolicParetoCurveCheckResult&& other) = default; virtual ~SymbolicParetoCurveCheckResult() = default; + virtual std::unique_ptr clone() const override; + virtual bool isSymbolicParetoCurveCheckResult() const override; virtual bool isSymbolic() const override; diff --git a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp index eb407eaa3..1fea0544c 100644 --- a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -17,6 +17,11 @@ namespace storm { // Intentionally left empty. } + template + std::unique_ptr SymbolicQualitativeCheckResult::clone() const { + return std::make_unique>(this->reachableStates, this->states, this->truthValues); + } + template bool SymbolicQualitativeCheckResult::isSymbolic() const { return true; diff --git a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.h index 0dc84690b..9afa4cd0f 100644 --- a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -22,6 +22,8 @@ namespace storm { SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult&& other) = default; #endif + virtual std::unique_ptr clone() const override; + virtual bool isSymbolic() const override; virtual bool isResultForAllStates() const override; diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index 52121ff70..ef778a7f7 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -22,6 +22,11 @@ namespace storm { // Intentionally left empty. } + template + std::unique_ptr SymbolicQuantitativeCheckResult::clone() const { + return std::make_unique>(this->reachableStates, this->states, this->values); + } + template std::unique_ptr SymbolicQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { storm::dd::Bdd states = this->states; diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h index cf7e037a8..d1d5fa3ba 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -22,8 +22,9 @@ namespace storm { SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult&& other) = default; #endif - virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override; + virtual std::unique_ptr clone() const override; + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override; virtual bool isSymbolic() const override; virtual bool isResultForAllStates() const override; diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index c6c6ec261..456fc4517 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -490,22 +490,22 @@ namespace storm { } template - std::unique_ptr> SymbolicGeneralMinMaxLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) const { + std::unique_ptr> GeneralSymbolicMinMaxLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) const { return std::make_unique>(A, allRows, illegalMask, rowMetaVariables, columnMetaVariables, choiceVariables, rowColumnMetaVariablePairs, std::make_unique>(), settings); } template - SymbolicMinMaxLinearEquationSolverSettings& SymbolicGeneralMinMaxLinearEquationSolverFactory::getSettings() { + SymbolicMinMaxLinearEquationSolverSettings& GeneralSymbolicMinMaxLinearEquationSolverFactory::getSettings() { return settings; } template - SymbolicMinMaxLinearEquationSolverSettings const& SymbolicGeneralMinMaxLinearEquationSolverFactory::getSettings() const { + SymbolicMinMaxLinearEquationSolverSettings const& GeneralSymbolicMinMaxLinearEquationSolverFactory::getSettings() const { return settings; } template - std::unique_ptr> SymbolicGeneralMinMaxLinearEquationSolverFactory::create() const { + std::unique_ptr> GeneralSymbolicMinMaxLinearEquationSolverFactory::create() const { return std::make_unique>(settings); } @@ -516,9 +516,9 @@ namespace storm { template class SymbolicMinMaxLinearEquationSolver; template class SymbolicMinMaxLinearEquationSolver; - template class SymbolicGeneralMinMaxLinearEquationSolverFactory; - template class SymbolicGeneralMinMaxLinearEquationSolverFactory; - template class SymbolicGeneralMinMaxLinearEquationSolverFactory; + template class GeneralSymbolicMinMaxLinearEquationSolverFactory; + template class GeneralSymbolicMinMaxLinearEquationSolverFactory; + template class GeneralSymbolicMinMaxLinearEquationSolverFactory; } } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h index 6853582f1..78d5bb510 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h @@ -237,7 +237,7 @@ namespace storm { }; template - class SymbolicGeneralMinMaxLinearEquationSolverFactory : public SymbolicMinMaxLinearEquationSolverFactory { + class GeneralSymbolicMinMaxLinearEquationSolverFactory : public SymbolicMinMaxLinearEquationSolverFactory { public: virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) const override; diff --git a/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index 249de13d9..a0cfa7699 100644 --- a/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -42,7 +42,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -140,7 +140,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -238,7 +238,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -318,7 +318,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); diff --git a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp index 8bb43f73c..fbaaf5df4 100644 --- a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp @@ -71,7 +71,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Cudd) { std::shared_ptr> quotientMdp = quotient->as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*quotientMdp, std::make_unique>()); + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*quotientMdp, std::make_unique>()); storm::parser::FormulaParser formulaParser; std::shared_ptr minFormula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"one\"]"); @@ -97,7 +97,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Cudd) { ASSERT_TRUE(quotient->isSymbolicModel()); quotientMdp = quotient->as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker2(*quotientMdp, std::make_unique>()); + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker2(*quotientMdp, std::make_unique>()); result = checker2.check(*minFormula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); @@ -117,7 +117,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Cudd) { ASSERT_TRUE(quotient->isSymbolicModel()); quotientMdp = quotient->as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker3(*quotientMdp, std::make_unique>()); + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker3(*quotientMdp, std::make_unique>()); result = checker3.check(*minFormula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); @@ -191,7 +191,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Sylvan) { std::shared_ptr> quotientMdp = quotient->as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*quotientMdp, std::make_unique>()); + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*quotientMdp, std::make_unique>()); storm::parser::FormulaParser formulaParser; std::shared_ptr minFormula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"one\"]"); @@ -217,7 +217,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Sylvan) { ASSERT_TRUE(quotient->isSymbolicModel()); quotientMdp = quotient->as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker2(*quotientMdp, std::make_unique>()); + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker2(*quotientMdp, std::make_unique>()); result = checker2.check(*minFormula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); @@ -237,7 +237,7 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Sylvan) { ASSERT_TRUE(quotient->isSymbolicModel()); quotientMdp = quotient->as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker3(*quotientMdp, std::make_unique>()); + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker3(*quotientMdp, std::make_unique>()); result = checker3.check(*minFormula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));