diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 6bb648e5f..d72eeee13 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -158,7 +158,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded reachability probabilities is unsupported for this value type."); } - template::SupportsExponential, int>::type= 0> + template::SupportsExponential, int>::type> void SparseMarkovAutomatonCslHelper::printTransitions(const uint64_t N, ValueType const diff, storm::storage::SparseMatrix const &fullTransitionMatrix, std::vector const &exitRateVector, storm::storage::BitVector const &markovianStates, @@ -234,7 +234,7 @@ namespace storm { template ::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::calculateVu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver, std::ofstream& logfile, std::vector const& poisson){ + void SparseMarkovAutomatonCslHelper::calculateVu(Environment const& env, std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver, std::ofstream& logfile, std::vector const& poisson){ if (unifVectors[1][k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation. uint64_t N = unifVectors[1].size()-1; auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); @@ -242,7 +242,7 @@ namespace storm { ValueType res =0; for (uint64_t i = k ; i < N ; i++ ){ if (unifVectors[2][N-1-(i-k)][node]==-1){ - calculateUnifPlusVector(N-1-(i-k),node,2,lambda,probSize,relativeReachability,dir,unifVectors,fullTransitionMatrix, markovianStates,psiStates,solver, logfile, poisson); + calculateUnifPlusVector(env, N-1-(i-k),node,2,lambda,probSize,relativeReachability,dir,unifVectors,fullTransitionMatrix, markovianStates,psiStates,solver, logfile, poisson); //old: relativeReachability, dir, (N-1-(i-k)),node,lambda,wu,fullTransitionMatrix,markovianStates,psiStates, solver); } res+=poisson[i]*unifVectors[2][N-1-(i-k)][node]; @@ -253,8 +253,8 @@ namespace storm { - template::SupportsExponential, int>::type= 0> - void SparseMarkovAutomatonCslHelper::calculateUnifPlusVector(uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, + template::SupportsExponential, int>::type> + void SparseMarkovAutomatonCslHelper::calculateUnifPlusVector(Environment const& env, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector> const &relativeReachability, OptimizationDirection dir, std::vector>> &unifVectors, @@ -312,7 +312,7 @@ namespace storm { for (auto &element : line){ uint64_t to = element.getColumn(); if (unifVectors[kind][k+1][to]==-1){ - calculateUnifPlusVector(k+1,to,kind,lambda,probSize,relativeReachability,dir,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver, logfile, poisson); + calculateUnifPlusVector(env, k+1,to,kind,lambda,probSize,relativeReachability,dir,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver, logfile, poisson); } res+=element.getValue()*unifVectors[kind][k+1][to]; } @@ -340,7 +340,7 @@ namespace storm { continue; } if (unifVectors[kind][k][to] == -1) { - calculateUnifPlusVector(k, to, kind, lambda, probSize, relativeReachability, dir, + calculateUnifPlusVector(env, k, to, kind, lambda, probSize, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, logfile, poisson); } @@ -351,7 +351,7 @@ namespace storm { } } - solver->solveEquations(dir, x, b); + solver->solveEquations(env, dir, x, b); @@ -366,7 +366,7 @@ namespace storm { } - template ::SupportsExponential, int>::type=0> + template ::SupportsExponential, int>::type> uint64_t SparseMarkovAutomatonCslHelper::trajans(storm::storage::SparseMatrix const& transitionMatrix, uint64_t node, std::vector& disc, std::vector& finish, uint64_t* counter) { auto const& rowGroupIndice = transitionMatrix.getRowGroupIndices(); @@ -394,7 +394,7 @@ namespace storm { return finish[node]; } - template::SupportsExponential, int>::type= 0> + template::SupportsExponential, int>::type> void SparseMarkovAutomatonCslHelper::identify( storm::storage::SparseMatrix const &fullTransitionMatrix, storm::storage::BitVector const &markovianStates, storm::storage::BitVector const& psiStates) { @@ -433,7 +433,7 @@ namespace storm { std:: cout << "prob States :" << probStates <<" markovian States: " << markStates << " realProb: "<< realProb << " NDM: " << NDM << " Alternating: " << Alternating << "\n"; } - template ::SupportsExponential, int>::type=0> + template ::SupportsExponential, int>::type> storm::storage::BitVector SparseMarkovAutomatonCslHelper::identifyProbCyclesGoalStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& cycleStates) { storm::storage::BitVector goalStates(cycleStates.size(), false); @@ -457,7 +457,7 @@ namespace storm { } - template ::SupportsExponential, int>::type=0> + template ::SupportsExponential, int>::type> storm::storage::BitVector SparseMarkovAutomatonCslHelper::identifyProbCycles(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){ storm::storage::BitVector const& probabilisticStates = ~markovianStates; @@ -491,7 +491,7 @@ namespace storm { } - template ::SupportsExponential, int>::type=0> + template ::SupportsExponential, int>::type> void SparseMarkovAutomatonCslHelper::deleteProbDiagonals(storm::storage::SparseMatrix& transitionMatrix, storm::storage::BitVector const& markovianStates){ auto const& rowGroupIndices = transitionMatrix.getRowGroupIndices(); @@ -526,7 +526,7 @@ namespace storm { } template::SupportsExponential, int>::type> - std::vector SparseMarkovAutomatonCslHelper::unifPlus(OptimizationDirection dir, + std::vector SparseMarkovAutomatonCslHelper::unifPlus(Environment const& env, OptimizationDirection dir, std::pair const &boundsPair, std::vector const &exitRateVector, storm::storage::SparseMatrix const &transitionMatrix, @@ -615,15 +615,14 @@ namespace storm { } //create equitation solver - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements( - true, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr> solver; if (probSize != 0) { - solver = minMaxLinearEquationSolverFactory.create(probMatrix); + solver = minMaxLinearEquationSolverFactory.create(env, probMatrix); solver->setHasUniqueSolution(); solver->setBounds(storm::utility::zero(), storm::utility::one()); solver->setRequirementsChecked(); @@ -692,13 +691,13 @@ namespace storm { // (5) calculate vectors and maxNorm for (uint64_t i = 0; i < numberOfStates; i++) { for (uint64_t k = N; k <= N; k--) { - calculateUnifPlusVector(k, i, 0, lambda, probSize, relReachability, dir, unifVectors, + calculateUnifPlusVector(env, k, i, 0, lambda, probSize, relReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, logfile, poisson); - calculateUnifPlusVector(k, i, 2, lambda, probSize, relReachability, dir, unifVectors, + calculateUnifPlusVector(env, k, i, 2, lambda, probSize, relReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, logfile, poisson); - calculateVu(relReachability, dir, k, i, 1, lambda, probSize, unifVectors, + calculateVu(env, relReachability, dir, k, i, 1, lambda, probSize, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, logfile, poisson); //also use iteration to keep maxNorm of vd and vup to date, so the loop-condition is easy to prove @@ -728,7 +727,7 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilitiesImca(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::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilitiesImca(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::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { STORM_LOG_TRACE("Using IMCA's technique to compute bounded until probabilities."); uint64_t numberOfStates = transitionMatrix.getRowGroupCount(); @@ -793,15 +792,15 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(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::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + 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& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { auto const& markovAutomatonSettings = storm::settings::getModule(); if (markovAutomatonSettings.getTechnique() == storm::settings::modules::MarkovAutomatonSettings::BoundedReachabilityTechnique::Imca) { - return computeBoundedUntilProbabilitiesImca(dir, transitionMatrix, exitRateVector, markovianStates, psiStates, boundsPair, minMaxLinearEquationSolverFactory); + return computeBoundedUntilProbabilitiesImca(env, dir, transitionMatrix, exitRateVector, markovianStates, psiStates, boundsPair, minMaxLinearEquationSolverFactory); } else { STORM_LOG_ASSERT(markovAutomatonSettings.getTechnique() == storm::settings::modules::MarkovAutomatonSettings::BoundedReachabilityTechnique::UnifPlus, "Unknown solution technique."); - return unifPlus(dir, boundsPair, exitRateVector, transitionMatrix, markovianStates, psiStates, minMaxLinearEquationSolverFactory); + return unifPlus(env, dir, boundsPair, exitRateVector, transitionMatrix, markovianStates, psiStates, minMaxLinearEquationSolverFactory); } } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 73e37cf81..bff568487 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -30,13 +30,13 @@ namespace storm { * */ template ::SupportsExponential, int>::type=0> - static std::vector unifPlus(OptimizationDirection dir, std::pair const& boundsPair, std::vector const& exitRateVector, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector unifPlus(Environment const& env, OptimizationDirection dir, std::pair const& boundsPair, std::vector const& exitRateVector, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); 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& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template ::SupportsExponential, int>::type = 0> - static std::vector computeBoundedUntilProbabilitiesImca(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::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeBoundedUntilProbabilitiesImca(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::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); 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& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); @@ -62,7 +62,7 @@ namespace storm { static void identify(storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates,storm::storage::BitVector const& psiStates); template ::SupportsExponential, int>::type=0> - static void calculateUnifPlusVector(uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector> const& relativeReachability, OptimizationDirection dir, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver, std::ofstream& logfile, std::vector const& poisson); + static void calculateUnifPlusVector(Environment const& env, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector> const& relativeReachability, OptimizationDirection dir, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver, std::ofstream& logfile, std::vector const& poisson); template ::SupportsExponential, int>::type=0> static void deleteProbDiagonals(storm::storage::SparseMatrix& transitionMatrix, storm::storage::BitVector const& markovianStates); @@ -421,7 +421,7 @@ remark : * */ template ::SupportsExponential, int>::type=0> - static void calculateVu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver, std::ofstream& logfile, std::vector const& poisson); + static void calculateVu(Environment const& env, std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver, std::ofstream& logfile, std::vector const& poisson);