diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 8400892a0..320cf72bd 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -38,7 +38,16 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { - return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); + if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + return true; + } + if (formula.isProbabilityOperatorFormula()) { + return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + } + if (formula.isGloballyFormula()) { + return true; + } + return false; } template @@ -72,6 +81,15 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.result))); } + template + std::unique_ptr SparseMdpPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret))); + } + template std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType, boost::optional> const& bound) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 2c9c61752..9ae3c3462 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -36,6 +36,7 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional(), boost::optional> const& bound =boost::optional>()); virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index e2c8cb479..a8f977601 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -23,7 +23,7 @@ namespace storm { template std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // Determine the states that have 0 probability of reaching the target states. storm::storage::BitVector maybeStates; @@ -60,7 +60,7 @@ namespace storm { std::vector SparseMdpPrctlHelper::computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Create the vector with which to multiply and initialize it correctly. - std::vector result(transitionMatrix.getRowCount()); + std::vector result(transitionMatrix.getRowGroupCount()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); @@ -73,8 +73,6 @@ namespace storm { template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); - // 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 statesWithProbability01; @@ -91,7 +89,7 @@ namespace storm { LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector. - std::vector result(numberOfStates); + std::vector result(transitionMatrix.getRowGroupCount()); // Set values of resulting vector that are known exactly. storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); @@ -136,6 +134,27 @@ namespace storm { return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, getPolicy, minMaxLinearEquationSolverFactory)); } + template + std::vector SparseMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique) { + + if (useMecBasedTechnique) { + storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions, psiStates); + storm::storage::BitVector statesInPsiMecs(transitionMatrix.getRowGroupCount()); + for (auto const& mec : mecDecomposition) { + for (auto const& stateActionsPair : mec) { + statesInPsiMecs.set(stateActionsPair.first, true); + } + } + + return std::move(computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, false, minMaxLinearEquationSolverFactory).result); + } else { + std::vector result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).result; + for (auto& element : result) { + element = storm::utility::one() - element; + } + return std::move(result); + } + } template template @@ -168,7 +187,7 @@ namespace storm { if (rewardModel.hasStateRewards()) { result = rewardModel.getStateRewardVector(); } else { - result.resize(transitionMatrix.getRowCount()); + result.resize(transitionMatrix.getRowGroupCount()); } std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); @@ -216,7 +235,7 @@ namespace storm { // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates; - storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); + storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true); if (dir == OptimizationDirection::Minimize) { infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterminsticChoiceIndices, backwardTransitions, trueStates, targetStates); } else { @@ -229,7 +248,7 @@ namespace storm { LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector. - std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // Check whether we need to compute exact rewards for some states. if (qualitative) { diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 5f7dc409f..1fb67fae9 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -38,6 +38,8 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false); + template static std::vector computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory);