From c3184d3afa90025e88c307934c5bad7877ccfa1c Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 3 Mar 2020 23:02:42 +0100 Subject: [PATCH] Consider relevant states in unif+ --- .../SparseMarkovAutomatonCslModelChecker.cpp | 3 +- .../helper/HybridMarkovAutomatonCslHelper.cpp | 3 +- .../helper/SparseMarkovAutomatonCslHelper.cpp | 424 +----------------- .../helper/SparseMarkovAutomatonCslHelper.h | 5 +- 4 files changed, 30 insertions(+), 405 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 225da07ce..10e3355f9 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -11,6 +11,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" +#include "storm/solver/SolveGoal.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -78,7 +79,7 @@ namespace storm { upperBound = storm::utility::infinity(); } - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound)); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound)); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp index 65b1f8ba8..d09a0e58a 100644 --- a/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp @@ -10,6 +10,7 @@ #include "storm/utility/macros.h" #include "storm/utility/graph.h" #include "storm/utility/constants.h" +#include "storm/solver/SolveGoal.h" #include "storm/models/symbolic/StandardRewardModel.h" @@ -66,7 +67,7 @@ namespace storm { conversionWatch.stop(); STORM_LOG_INFO("Converting symbolic matrix to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); - auto explicitResult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, dir, explicitTransitionMatrix, explicitExitRateVector, markovianStates.toVector(odd), phiStates.toVector(odd), psiStates.toVector(odd), {lowerBound, upperBound}); + auto explicitResult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(dir), explicitTransitionMatrix, explicitExitRateVector, markovianStates.toVector(odd), phiStates.toVector(odd), psiStates.toVector(odd), {lowerBound, upperBound}); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(explicitResult))); } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index bfc0d5b13..8e6f427ab 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -47,7 +47,7 @@ namespace storm { // Intentionally left empty } - std::vector computeBoundedUntilProbabilities(storm::Environment const& env, OptimizationDirection dir, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, ValueType const& upperTimeBound) { + std::vector computeBoundedUntilProbabilities(storm::Environment const& env, OptimizationDirection dir, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, ValueType const& upperTimeBound, boost::optional const& relevantStates = boost::none) { // Since there is no lower time bound, we can treat the psiStates as if they are absorbing. // Compute some important subsets of states @@ -56,7 +56,10 @@ namespace storm { storm::storage::BitVector probabilisticMaybeStates = ~markovianStates & maybeStates; storm::storage::BitVector markovianStatesModMaybeStates = markovianMaybeStates % maybeStates; storm::storage::BitVector probabilisticStatesModMaybeStates = probabilisticMaybeStates % maybeStates; - + boost::optional relevantMaybeStates; + if (relevantStates) { + relevantMaybeStates = relevantStates.get() % maybeStates; + } // Catch the case where this is query can be solved by solving the untimed variant instead. // This is the case if there is no Markovian maybe state (e.g. if the initial state is already a psi state) of if the time bound is infinity. if (markovianMaybeStates.empty() || storm::utility::isInfinity(upperTimeBound)) { @@ -178,7 +181,7 @@ namespace storm { } // Check if the lower and upper bound are sufficiently close to each other // TODO: apply this only to relevant values? - converged = checkConvergence(maybeStatesValuesLower, maybeStatesValuesUpper, boost::none, epsilon, relativePrecision, kappa); + converged = checkConvergence(maybeStatesValuesLower, maybeStatesValuesUpper, relevantMaybeStates, epsilon, relativePrecision, kappa); if (converged) { break; } @@ -220,6 +223,7 @@ namespace storm { private: bool checkConvergence(std::vector const& lower, std::vector const& upper, boost::optional const& relevantValues, ValueType const& epsilon, bool relative, ValueType& kappa) { + STORM_LOG_ASSERT(!relevantValues.is_initialized() || relevantValues->size() == lower.size(), "Relevant values size mismatch."); if (!relative) { if (relevantValues) { return storm::utility::vector::equalModuloPrecision(lower, upper, relevantValues.get(), epsilon * (storm::utility::one() - kappa), false); @@ -230,6 +234,12 @@ namespace storm { ValueType truncationError = epsilon * kappa; ValueType twoTimestruncationError = storm::utility::convertNumber(2.0) * truncationError; for (uint64_t i = 0; i < lower.size(); ++i) { + if (relevantValues) { + i = relevantValues->getNextSetIndex(i); + if (i == lower.size()) { + break; + } + } if (lower[i] == upper[i]) { continue; } @@ -331,403 +341,11 @@ namespace storm { return sparseResult; } - void performMarkovianStep(storm::Environment const& env, storm::storage::SparseMatrix const& markovianTransitions, std::vector> const& oneStepToGoalProbabilities, std::vector const& currentMaybeStatesValues, ValueType const& currentGoalValue) const { - // Set up a multiplier for the transitions emerging at Markovian states - auto multiplier = storm::solver::MultiplierFactory().create(env, markovianTransitions); - } - storm::storage::SparseMatrix const& transitionMatrix; std::vector const& exitRateVector; storm::storage::BitVector const& markovianStates; }; - - - - /** - * Data structure holding result vectors (vLower, vUpper, wUpper) for Unif+. - */ - template - struct UnifPlusVectors { - UnifPlusVectors() { - // Intentionally empty - } - - /** - * Initialize results vectors. vLowerOld, vUpperOld and wUpper[k=N] are initialized with zeros. - */ - UnifPlusVectors(uint64_t steps, uint64_t noStates) : numberOfStates(noStates), steps(steps), resLowerOld(numberOfStates, storm::utility::zero()), resLowerNew(numberOfStates, -1), resUpper(numberOfStates, storm::utility::zero()), wUpperOld(numberOfStates, storm::utility::zero()), wUpperNew(numberOfStates, -1) { - // Intentionally left empty - } - - /** - * Prepare new iteration by setting the new result vectors as old result vectors, and initializing the new result vectors with -1 again. - */ - void prepareNewIteration() { - resLowerOld.swap(resLowerNew); - std::fill(resLowerNew.begin(), resLowerNew.end(), -1); - wUpperOld.swap(wUpperNew); - std::fill(wUpperNew.begin(), wUpperNew.end(), -1); - } - - uint64_t numberOfStates; - uint64_t steps; - std::vector resLowerOld; - std::vector resLowerNew; - std::vector resUpper; - std::vector wUpperOld; - std::vector wUpperNew; - }; - - template - void calculateUnifPlusVector(Environment const& env, uint64_t k, uint64_t state, bool calcLower, ValueType lambda, uint64_t numberOfProbabilisticChoices, std::vector> const & relativeReachability, OptimizationDirection dir, UnifPlusVectors& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver, storm::utility::numerical::FoxGlynnResult const& poisson, bool cycleFree) { - // Set reference to acutal vector - std::vector& resVectorOld = calcLower ? unifVectors.resLowerOld : unifVectors.wUpperOld; - std::vector& resVectorNew = calcLower ? unifVectors.resLowerNew : unifVectors.wUpperNew; - - if (resVectorNew[state] != -1) { - // Result already calculated. - return; - } - - auto numberOfStates = fullTransitionMatrix.getRowGroupCount(); - uint64_t N = unifVectors.steps; - auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); - ValueType res; - - // First case, k==N, independent from kind of state. - if (k == N) { - STORM_LOG_ASSERT(false, "Result for k=N was already calculated."); - resVectorNew[state] = storm::utility::zero(); - return; - } - - // Goal state, independent from kind of state. - if (psiStates[state]) { - if (calcLower) { - // v lower - res = storm::utility::zero(); - for (uint64_t i = k; i < N; ++i){ - if (i >= poisson.left && i <= poisson.right) { - res += poisson.weights[i - poisson.left]; - } - } - resVectorNew[state] = res; - } else { - // w upper - resVectorNew[state] = storm::utility::one(); - } - return; - } - - - // Markovian non-goal state. - if (markovianStates[state]) { - res = storm::utility::zero(); - for (auto const& element : fullTransitionMatrix.getRow(rowGroupIndices[state])) { - uint64_t successor = element.getColumn(); - if (resVectorOld[successor] == -1) { - STORM_LOG_ASSERT(false, "Need to calculate previous result."); - calculateUnifPlusVector(env, k+1, successor, calcLower, lambda, numberOfProbabilisticChoices, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, poisson, cycleFree); - } - res += element.getValue() * resVectorOld[successor]; - } - resVectorNew[state]=res; - return; - } - - // Probabilistic non-goal state. - if (cycleFree) { - // If the model is cycle free, do "slight value iteration". (What is that?) - res = -1; - for (uint64_t i = rowGroupIndices[state]; i < rowGroupIndices[state + 1]; ++i) { - auto row = fullTransitionMatrix.getRow(i); - ValueType between = storm::utility::zero(); - for (auto const& element : row) { - uint64_t successor = element.getColumn(); - - // This should never happen, right? The model has no cycles, and therefore also no self-loops. - if (successor == state) { - continue; - } - - if (resVectorNew[successor] == -1) { - calculateUnifPlusVector(env, k, successor, calcLower, lambda, numberOfProbabilisticChoices, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, poisson, cycleFree); - } - between += element.getValue() * resVectorNew[successor]; - } - if (maximize(dir)) { - res = storm::utility::max(res, between); - } else { - if (res != -1) { - res = storm::utility::min(res, between); - } else { - res = between; - } - } - } - resVectorNew[state] = res; - return; - } - - // If we arrived at this point, the model is not cycle free. Use the solver to solve the underlying equation system. - uint64_t numberOfProbabilisticStates = numberOfStates - markovianStates.getNumberOfSetBits(); - std::vector b(numberOfProbabilisticChoices, storm::utility::zero()); - std::vector x(numberOfProbabilisticStates, storm::utility::zero()); - - // Compute right-hand side vector b. - uint64_t row = 0; - for (uint64_t i = 0; i < numberOfStates; ++i) { - if (markovianStates[i]) { - continue; - } - - for (auto j = rowGroupIndices[i]; j < rowGroupIndices[i + 1]; j++) { - uint64_t stateCount = 0; - res = storm::utility::zero(); - for (auto const& element : fullTransitionMatrix.getRow(j)) { - auto successor = element.getColumn(); - if (!markovianStates[successor]) { - continue; - } - - if (resVectorNew[successor] == -1) { - calculateUnifPlusVector(env, k, successor, calcLower, lambda, numberOfProbabilisticChoices, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, poisson, cycleFree); - } - res += relativeReachability[j][stateCount] * resVectorNew[successor]; - ++stateCount; - } - - b[row] = res; - ++row; - } - } - - // Solve the equation system. - solver->solveEquations(env, dir, x, b); - - // Expand the solution for the probabilistic states to all states. - storm::utility::vector::setVectorValues(resVectorNew, ~markovianStates, x); - } - - template - void eliminateProbabilisticSelfLoops(storm::storage::SparseMatrix& transitionMatrix, storm::storage::BitVector const& markovianStates) { - auto const& rowGroupIndices = transitionMatrix.getRowGroupIndices(); - - for (uint64_t i = 0; i < transitionMatrix.getRowGroupCount(); ++i) { - if (markovianStates[i]) { - continue; - } - - for (uint64_t j = rowGroupIndices[i]; j < rowGroupIndices[i + 1]; j++) { - ValueType selfLoop = storm::utility::zero(); - for (auto const& element: transitionMatrix.getRow(j)){ - if (element.getColumn() == i) { - selfLoop += element.getValue(); - } - } - - if (storm::utility::isZero(selfLoop)) { - continue; - } - - for (auto& element : transitionMatrix.getRow(j)) { - if (element.getColumn() != i) { - if (!storm::utility::isOne(selfLoop)) { - element.setValue(element.getValue() / (storm::utility::one() - selfLoop)); - } - } else { - element.setValue(storm::utility::zero()); - } - } - } - } - } - - template - std::vector computeBoundedUntilProbabilitiesUnifPlus(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair) { - STORM_LOG_TRACE("Using UnifPlus to compute bounded until probabilities."); - - // Obtain bit vectors to identify different kind of states. - storm::storage::BitVector allStates(markovianStates.size(), true); - storm::storage::BitVector probabilisticStates = ~markovianStates; - - // Searching for SCCs in probabilistic fragment to decide which algorithm is applied. - bool cycleFree = !storm::utility::graph::hasCycle(transitionMatrix, probabilisticStates); - - // Vectors to store computed vectors. - UnifPlusVectors unifVectors; - - // Transitions from goal states will be ignored. However, we mark them as non-probabilistic to make sure - // we do not apply the MDP algorithm to them. - storm::storage::BitVector markovianAndGoalStates = markovianStates | psiStates; - probabilisticStates &= ~psiStates; - - std::vector mutableExitRates = exitRateVector; - - // Extend the transition matrix with diagonal entries so we can change them easily during the uniformization step. - typename storm::storage::SparseMatrix fullTransitionMatrix = transitionMatrix.getSubmatrix(true, allStates, allStates, true); - - // Eliminate self-loops of probabilistic states. Is this really needed for the "slight value iteration" process? - eliminateProbabilisticSelfLoops(fullTransitionMatrix, markovianAndGoalStates); - typename storm::storage::SparseMatrix probMatrix; - uint64_t numberOfProbabilisticChoices = 0; - if (!probabilisticStates.empty()) { - probMatrix = fullTransitionMatrix.getSubmatrix(true, probabilisticStates, probabilisticStates, true); - numberOfProbabilisticChoices = probMatrix.getRowCount(); - } - - // Get row grouping of transition matrix. - auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); - - // (1) define/declare horizon, epsilon, kappa, N, lambda, maxNorm - uint64_t numberOfStates = fullTransitionMatrix.getRowGroupCount(); - // 'Unpack' the bounds to make them more easily accessible. - double lowerBound = boundsPair.first; - double upperBound = boundsPair.second; - // Lower bound > 0 is not implemented! - STORM_LOG_THROW(lowerBound == 0, storm::exceptions::NotImplementedException, "Support for lower bound > 0 not implemented in Unif+."); - // Truncation error - // TODO: make kappa a parameter. - ValueType kappa = storm::utility::one() / 10; - // Approximation error - ValueType epsilon = storm::settings::getModule().getPrecision(); - // Lambda is largest exit rate - ValueType lambda = exitRateVector[0]; - for (ValueType const& rate : exitRateVector) { - lambda = std::max(rate, lambda); - } - STORM_LOG_DEBUG("Initial lambda is " << lambda << "."); - - // Compute the relative reachability vectors and create solver for models with SCCs. - std::vector> relativeReachabilities(transitionMatrix.getRowCount()); - std::unique_ptr> solver; - if (!cycleFree) { - for (uint64_t i = 0; i < numberOfStates; i++) { - if (markovianAndGoalStates[i]) { - continue; - } - - for (auto j = rowGroupIndices[i]; j < rowGroupIndices[i + 1]; ++j) { - for (auto const& element : fullTransitionMatrix.getRow(j)) { - if (markovianAndGoalStates[element.getColumn()]) { - relativeReachabilities[j].push_back(element.getValue()); - } - } - } - } - - // Create solver. - storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, true, dir); - requirements.clearBounds(); - STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); - - if (numberOfProbabilisticChoices > 0) { - solver = minMaxLinearEquationSolverFactory.create(env, probMatrix); - solver->setHasUniqueSolution(); - solver->setHasNoEndComponents(); - solver->setBounds(storm::utility::zero(), storm::utility::one()); - solver->setRequirementsChecked(); - solver->setCachingEnabled(true); - } - } - - ValueType maxNorm = storm::utility::zero(); - // Maximal step size - uint64_t N; - storm::utility::ProgressMeasurement progressIterations("iterations"); - size_t iteration = 0; - progressIterations.startNewMeasurement(iteration); - // Loop until result is within precision bound. - do { - // (2) update parameter - N = storm::utility::ceil(lambda * upperBound * std::exp(2) - storm::utility::log(kappa * epsilon)); - - // (3) uniform - just applied to Markovian states. - for (uint64_t i = 0; i < numberOfStates; i++) { - if (!markovianAndGoalStates[i] || psiStates[i]) { - continue; - } - - // As the current state is Markovian, its branching probabilities are stored within one row. - uint64_t markovianRowIndex = rowGroupIndices[i]; - - if (mutableExitRates[i] == lambda) { - // Already uniformized. - continue; - } - - auto markovianRow = fullTransitionMatrix.getRow(markovianRowIndex); - ValueType oldExitRate = mutableExitRates[i]; - ValueType newExitRate = lambda; - for (auto& v : markovianRow) { - if (v.getColumn() == i) { - ValueType newSelfLoop = newExitRate - oldExitRate + v.getValue() * oldExitRate; - ValueType newRate = newSelfLoop / newExitRate; - v.setValue(newRate); - } else { - ValueType oldProbability = v.getValue(); - ValueType newProbability = oldProbability * oldExitRate / newExitRate; - v.setValue(newProbability); - } - } - mutableExitRates[i] = newExitRate; - } - - // Compute poisson distribution. - storm::utility::numerical::FoxGlynnResult foxGlynnResult = storm::utility::numerical::foxGlynn(lambda * upperBound, epsilon * kappa / 100); - - // Scale the weights so they sum to one. - for (auto& element : foxGlynnResult.weights) { - element /= foxGlynnResult.totalWeight; - } - - // (4) Define vectors/matrices. - // Initialize result vectors and already insert zeros for iteration N - unifVectors = UnifPlusVectors(N, numberOfStates); - - // (5) Compute vectors and maxNorm. - // Iteration k = N was already performed by initializing with zeros. - - // Iterations k < N - storm::utility::ProgressMeasurement progressSteps("steps in iteration " + std::to_string(iteration)); - progressSteps.setMaxCount(N); - progressSteps.startNewMeasurement(0); - for (int64_t k = N-1; k >= 0; --k) { - if (k < (int64_t)(N-1)) { - unifVectors.prepareNewIteration(); - } - for (uint64_t state = 0; state < numberOfStates; ++state) { - // Calculate results for lower bound and wUpper - calculateUnifPlusVector(env, k, state, true, lambda, numberOfProbabilisticChoices, relativeReachabilities, dir, unifVectors, fullTransitionMatrix, markovianAndGoalStates, psiStates, solver, foxGlynnResult, cycleFree); - calculateUnifPlusVector(env, k, state, false, lambda, numberOfProbabilisticChoices, relativeReachabilities, dir, unifVectors, fullTransitionMatrix, markovianAndGoalStates, psiStates, solver, foxGlynnResult, cycleFree); - // Calculate result for upper bound - uint64_t index = N-1-k; - if (index >= foxGlynnResult.left && index <= foxGlynnResult.right) { - STORM_LOG_ASSERT(unifVectors.wUpperNew[state] != -1, "wUpper was not computed before."); - unifVectors.resUpper[state] += foxGlynnResult.weights[index - foxGlynnResult.left] * unifVectors.wUpperNew[state]; - } - } - progressSteps.updateProgress(N-k); - } - - // Only iterate over result vector, as the results can only get more precise. - maxNorm = storm::utility::zero(); - for (uint64_t i = 0; i < numberOfStates; i++){ - ValueType diff = storm::utility::abs(unifVectors.resUpper[i] - unifVectors.resLowerNew[i]); - maxNorm = std::max(maxNorm, diff); - } - - // (6) Double lambda. - lambda *= 2; - STORM_LOG_DEBUG("Increased lambda to " << lambda << ", max diff is " << maxNorm << "."); - progressIterations.updateProgress(++iteration); - } while (maxNorm > epsilon * (1 - kappa)); - - return unifVectors.resLowerNew; - } - template void computeBoundedReachabilityProbabilitiesImca(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps) { @@ -913,7 +531,7 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair) { + std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair) { // Choose the applicable method auto method = env.solver().timeBounded().getMaMethod(); if (method == storm::solver::MaBoundedReachabilityMethod::Imca) { @@ -930,15 +548,19 @@ namespace storm { } if (method == storm::solver::MaBoundedReachabilityMethod::Imca) { - return computeBoundedUntilProbabilitiesImca(env, dir, transitionMatrix, exitRateVector, markovianStates, psiStates, boundsPair); + return computeBoundedUntilProbabilitiesImca(env, goal.direction(), transitionMatrix, exitRateVector, markovianStates, psiStates, boundsPair); } else { UnifPlusHelper helper(transitionMatrix, exitRateVector, markovianStates); - return helper.computeBoundedUntilProbabilities(env, dir, phiStates, psiStates, boundsPair.second); + boost::optional relevantValues; + if (goal.hasRelevantValues()) { + relevantValues = std::move(goal.relevantValues()); + } + return helper.computeBoundedUntilProbabilities(env, goal.direction(), phiStates, psiStates, boundsPair.second, relevantValues); } } template ::SupportsExponential, int>::type> - std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair) { + std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type."); } @@ -1451,7 +1073,7 @@ namespace storm { return v.front() * uniformizationRate; } - template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair); + template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair); template MDPSparseModelCheckingHelperReturnType SparseMarkovAutomatonCslHelper::computeUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler); @@ -1471,7 +1093,7 @@ namespace storm { template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentVI(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); - template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair); + template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair); template MDPSparseModelCheckingHelperReturnType SparseMarkovAutomatonCslHelper::computeUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index cab2ecd2f..ed0dfddef 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -6,6 +6,7 @@ #include "storm/storage/MaximalEndComponent.h" #include "storm/solver/OptimizationDirection.h" #include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/SolveGoal.h" #include "storm/utility/NumberTraits.h" namespace storm { @@ -19,10 +20,10 @@ namespace storm { public: template ::SupportsExponential, int>::type = 0> - static std::vector computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair); + static std::vector computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair); template ::SupportsExponential, int>::type = 0> - static std::vector computeBoundedUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair); + static std::vector computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair); template static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler);