From de2e94cac7af6449b2cad49a5efa64761bbe6821 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 6 Mar 2018 21:27:09 +0100 Subject: [PATCH] polished unifplus code a bit and made it the default MA (bounded reachability) solution method --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 179 ++++++++---------- src/storm/settings/SettingsManager.cpp | 2 - .../modules/MarkovAutomatonSettings.cpp | 32 ---- .../modules/MarkovAutomatonSettings.h | 38 ---- .../modules/MinMaxEquationSolverSettings.cpp | 12 ++ .../modules/MinMaxEquationSolverSettings.h | 11 ++ .../TopologicalMinMaxLinearEquationSolver.cpp | 2 +- 7 files changed, 103 insertions(+), 173 deletions(-) delete mode 100644 src/storm/settings/modules/MarkovAutomatonSettings.cpp delete mode 100644 src/storm/settings/modules/MarkovAutomatonSettings.h diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index f0929c9a0..7bf5f10f5 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -10,7 +10,6 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/MinMaxEquationSolverSettings.h" -#include "storm/settings/modules/MarkovAutomatonSettings.h" #include "storm/environment/Environment.h" @@ -22,8 +21,6 @@ #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/ExpressionManager.h" -//#include "storm/utility/numerical.h" - #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/LpSolver.h" @@ -35,24 +32,9 @@ namespace storm { namespace modelchecker { namespace helper { - - /* - * with having only a subset of the originalMatrix/vector, we need to transform indice - */ - static uint64_t transformIndice(storm::storage::BitVector const& subset, uint64_t fakeId){ - uint64_t id =0; - uint64_t counter =0; - while(counter<=fakeId){ - if(subset[id]){ - counter++; - } - id++; - } - return id-1; - } template - void calculateUnifPlusVector(Environment const& env, uint64_t k, uint64_t state, uint64_t const kind, ValueType lambda, uint64_t numberOfProbabilisticStates, 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, storm::utility::numerical::FoxGlynnResult const& poisson, bool cycleFree) { + void calculateUnifPlusVector(Environment const& env, uint64_t k, uint64_t state, uint64_t const kind, ValueType lambda, uint64_t numberOfProbabilisticChoices, 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, storm::utility::numerical::FoxGlynnResult const& poisson, bool cycleFree) { if (unifVectors[kind][k][state] != -1) { // Result already calculated. @@ -72,7 +54,7 @@ namespace storm { // Goal state, independent from kind of state. if (psiStates[state]) { - if (kind == 0){ + if (kind == 0) { // Vd res = storm::utility::zero(); for (uint64_t i = k; i < N; ++i){ @@ -91,11 +73,11 @@ namespace storm { // Markovian non-goal state. if (markovianStates[state]) { - res = storm::utility::zero; + res = storm::utility::zero(); for (auto const& element : fullTransitionMatrix.getRow(rowGroupIndices[state])) { uint64_t to = element.getColumn(); if (unifVectors[kind][k+1][to] == -1) { - calculateUnifPlusVector(env, k+1, to, kind, lambda, numberOfProbabilisticStates, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, poisson, cycleFree); + calculateUnifPlusVector(env, k+1, to, kind, lambda, numberOfProbabilisticChoices, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, poisson, cycleFree); } res += element.getValue()*unifVectors[kind][k+1][to]; } @@ -111,24 +93,23 @@ namespace storm { auto row = fullTransitionMatrix.getRow(i); ValueType between = 0; for (auto const& element : row) { - uint64_t to = element.getColumn(); + uint64_t successor = element.getColumn(); // This should never happen, right? The model has no cycles, and therefore also no self-loops. - if (to == state) { + if (successor == state) { continue; } - if (unifVectors[kind][k][to] == -1) { - calculateUnifPlusVector(env, k, to, kind, lambda, numberOfProbabilisticStates, relativeReachability, dir, - unifVectors, fullTransitionMatrix, markovianStates, psiStates, - solver, poisson, cycleFree); + + if (unifVectors[kind][k][successor] == -1) { + calculateUnifPlusVector(env, k, successor, kind, lambda, numberOfProbabilisticChoices, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, poisson, cycleFree); } - between += element.getValue() * unifVectors[kind][k][to]; + between += element.getValue() * unifVectors[kind][k][successor]; } if (maximize(dir)) { - res = std::max(res, between); + res = storm::utility::max(res, between); } else { if (res != -1) { - res = std::min(res, between); + res = storm::utility::min(res, between); } else { res = between; } @@ -138,64 +119,65 @@ namespace storm { return; } - //not cycle free - use solver technique, calling SVI per default - //solving all sub-MDP's in one iteration - std::vector b(probSize, 0), x(numberOfProbabilisticStates,0); - //calculate b - uint64_t lineCounter=0; - for (int i =0; i 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; } - auto rowStart = rowGroupIndices[i]; - auto rowEnd = rowGroupIndices[i + 1]; - for (auto j = rowStart; j < rowEnd; j++) { + + for (auto j = rowGroupIndices[i]; j < rowGroupIndices[i + 1]; j++) { uint64_t stateCount = 0; - res = 0; - for (auto &element:fullTransitionMatrix.getRow(j)) { - auto to = element.getColumn(); - if (!markovianStates[to]) { + res = storm::utility::zero(); + for (auto const& element : fullTransitionMatrix.getRow(j)) { + auto successor = element.getColumn(); + if (!markovianStates[successor]) { continue; } - if (unifVectors[kind][k][to] == -1) { - calculateUnifPlusVector(env, k, to, kind, lambda, numberOfProbabilisticStates, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, poisson, cycleFree); + + if (unifVectors[kind][k][successor] == -1) { + calculateUnifPlusVector(env, k, successor, kind, lambda, numberOfProbabilisticStates, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, poisson, cycleFree); } - res = res + relativeReachability[j][stateCount] * unifVectors[kind][k][to]; - stateCount++; + res = res + relativeReachability[j][stateCount] * unifVectors[kind][k][successor]; + ++stateCount; } - b[lineCounter] = res; - lineCounter++; + + b[row] = res; + ++row; } } - solver->solveEquations(env, dir, x, b); - for (uint64_t i = 0; isolveEquations(env, dir, x, b); + + // Expand the solution for the probabilistic states to all states. + storm::utility::vector::setVectorValues(unifVectors[kind][k], ~markovianStates, x); } template - 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, - storm::utility::numerical::FoxGlynnResult const & poisson, bool cycleFree){ - if (unifVectors[1][k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation. - uint64_t N = unifVectors[1].size()-1; + void calculateVu(Environment const& env, std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t state, uint64_t const kind, ValueType lambda, uint64_t numberOfProbabilisticStates, std::vector>>& 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) { + + // Avoiding multiple computation of the same value. + if (unifVectors[1][k][state] != -1) { + return; + } + uint64_t N = unifVectors[1].size() - 1; - ValueType res =0; - for (uint64_t i = k ; i < N ; i++ ){ - if (unifVectors[2][N-1-(i-k)][node]==-1){ - calculateUnifPlusVector(env, N-1-(i-k),node,2,lambda,probSize,relativeReachability,dir,unifVectors,fullTransitionMatrix, markovianStates,psiStates,solver, poisson, cycleFree); + ValueType res = storm::utility::zero(); + for (uint64_t i = k; i < N; ++i) { + if (unifVectors[2][N-1-(i-k)][state] == -1) { + calculateUnifPlusVector(env, N-1-(i-k), state, 2, lambda, numberOfProbabilisticStates, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, psiStates, solver, poisson, cycleFree); } - if (i>=poisson.left && i<=poisson.right){ - res+=poisson.weights[i-poisson.left]*unifVectors[2][N-1-(i-k)][node]; + if (i >= poisson.left && i <= poisson.right) { + res += poisson.weights[i - poisson.left] * unifVectors[2][N-1-(i-k)][state]; } } - unifVectors[1][k][node]=res; + unifVectors[1][k][state] = res; } template @@ -245,10 +227,10 @@ namespace storm { bool cycleFree = sccDecomposition.empty(); // Vectors to store computed vectors. - std::vector>> unifVectors{}; + std::vector>> unifVectors(3); - // Transitions from goal states will be ignored. However, they are not allowed to be probabilistic - // to make sure we do not apply the MDP algorithm to them. + // 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; @@ -257,15 +239,13 @@ namespace storm { // 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 value iteration process? - eliminateProbabilisticSelfLoops(fullTransitionMatrix, markovianStates); + // 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 numberOfProbabilisticStates = probabilisticStates.getNumberOfSetBits(); - if (numberOfProbabilisticStates > 0) { + uint64_t numberOfProbabilisticChoices = 0; + if (!probabilisticStates.empty()) { probMatrix = fullTransitionMatrix.getSubmatrix(true, probabilisticStates, probabilisticStates, true); - - // row count? shouldn't this be row group count? - // probSize = probMatrix.getRowCount(); + numberOfProbabilisticChoices = probMatrix.getRowCount(); } // Get row grouping of transition matrix. @@ -289,13 +269,13 @@ namespace storm { std::unique_ptr> solver; if (!cycleFree) { for (uint64_t i = 0; i < numberOfStates; i++) { - if (markovianStates[i]) { + if (markovianAndGoalStates[i]) { continue; } for (auto j = rowGroupIndices[i]; j < rowGroupIndices[i + 1]; ++j) { - for (auto const& element: fullTransitionMatrix.getRow(j)) { - if (markovianStates[element.getColumn()]) { + for (auto const& element : fullTransitionMatrix.getRow(j)) { + if (markovianAndGoalStates[element.getColumn()]) { relativeReachabilities[j].push_back(element.getValue()); } } @@ -308,7 +288,7 @@ namespace storm { requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); - if (numberOfProbabilisticStates > 0) { + if (numberOfProbabilisticChoices > 0) { solver = minMaxLinearEquationSolverFactory.create(env, probMatrix); solver->setHasUniqueSolution(); solver->setBounds(storm::utility::zero(), storm::utility::one()); @@ -318,6 +298,7 @@ namespace storm { } // Loop until result is within precision bound. + std::vector init(numberOfStates, -1); do { maxNorm = storm::utility::zero(); @@ -326,7 +307,7 @@ namespace storm { // (3) uniform - just applied to Markovian states. for (uint64_t i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) { - if (!markovianStates[i] || psiStates[i]) { + if (!markovianAndGoalStates[i] || psiStates[i]) { continue; } @@ -358,27 +339,25 @@ namespace storm { // Compute poisson distribution. storm::utility::numerical::FoxGlynnResult foxGlynnResult = storm::utility::numerical::foxGlynn(lambda * T, epsilon * kappa / 100); - // Scale the weights so they add up to one. + // Scale the weights so they sum to one. for (auto& element : foxGlynnResult.weights) { element /= foxGlynnResult.totalWeight; } // (4) Define vectors/matrices. - std::vector init(numberOfStates, -1); std::vector> v = std::vector>(N + 1, init); - unifVectors.clear(); - unifVectors.push_back(v); - unifVectors.push_back(v); - unifVectors.push_back(v); + unifVectors[0] = v; + unifVectors[1] = v; + unifVectors[2] = v; // Define 0=vd, 1=vu, 2=wu. // (5) Compute vectors and maxNorm. - for (uint64_t i = 0; i < numberOfStates; i++) { - for (uint64_t k = N; k <= N; k--) { - calculateUnifPlusVector(env, k, i, 0, lambda, numberOfProbabilisticStates, relativeReachabilities, dir, unifVectors, fullTransitionMatrix, markovianAndGoalStates, psiStates, solver, foxGlynnResult, cycleFree); - calculateUnifPlusVector(env, k, i, 2, lambda, numberOfProbabilisticStates, relativeReachabilities, dir, unifVectors, fullTransitionMatrix, markovianAndGoalStates, psiStates, solver, foxGlynnResult, cycleFree); - calculateVu(env, relativeReachabilities, dir, k, i, 1, lambda, numberOfProbabilisticStates, unifVectors, fullTransitionMatrix, markovianAndGoalStates, psiStates, solver, foxGlynnResult, cycleFree); + for (uint64_t i = 0; i < numberOfStates; ++i) { + for (uint64_t k = N; k <= N; --k) { + calculateUnifPlusVector(env, k, i, 0, lambda, numberOfProbabilisticChoices, relativeReachabilities, dir, unifVectors, fullTransitionMatrix, markovianAndGoalStates, psiStates, solver, foxGlynnResult, cycleFree); + calculateUnifPlusVector(env, k, i, 2, lambda, numberOfProbabilisticChoices, relativeReachabilities, dir, unifVectors, fullTransitionMatrix, markovianAndGoalStates, psiStates, solver, foxGlynnResult, cycleFree); + calculateVu(env, relativeReachabilities, dir, k, i, 1, lambda, numberOfProbabilisticChoices, unifVectors, fullTransitionMatrix, markovianAndGoalStates, psiStates, solver, foxGlynnResult, cycleFree); } } @@ -582,11 +561,11 @@ 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& psiStates, std::pair const& boundsPair) { - auto const& markovAutomatonSettings = storm::settings::getModule(); - if (markovAutomatonSettings.getTechnique() == storm::settings::modules::MarkovAutomatonSettings::BoundedReachabilityTechnique::Imca) { + auto const& settings = storm::settings::getModule(); + if (settings.getMarkovAutomatonBoundedReachabilityMethod() == storm::settings::modules::MinMaxEquationSolverSettings::MarkovAutomatonBoundedReachabilityMethod::Imca) { return computeBoundedUntilProbabilitiesImca(env, dir, transitionMatrix, exitRateVector, markovianStates, psiStates, boundsPair); } else { - STORM_LOG_ASSERT(markovAutomatonSettings.getTechnique() == storm::settings::modules::MarkovAutomatonSettings::BoundedReachabilityTechnique::UnifPlus, "Unknown solution technique."); + STORM_LOG_ASSERT(settings.getMarkovAutomatonBoundedReachabilityMethod() == storm::settings::modules::MinMaxEquationSolverSettings::MarkovAutomatonBoundedReachabilityMethod::UnifPlus, "Unknown solution method."); return computeBoundedUntilProbabilitiesUnifPlus(env, dir, boundsPair, exitRateVector, transitionMatrix, markovianStates, psiStates); } diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 89ad6f3cb..fc2b80b35 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -38,7 +38,6 @@ #include "storm/settings/modules/JaniExportSettings.h" #include "storm/settings/modules/JitBuilderSettings.h" #include "storm/settings/modules/MultiObjectiveSettings.h" -#include "storm/settings/modules/MarkovAutomatonSettings.h" #include "storm/settings/modules/MultiplierSettings.h" #include "storm/utility/macros.h" #include "storm/utility/file.h" @@ -552,7 +551,6 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); - storm::settings::addModule(); storm::settings::addModule(); } diff --git a/src/storm/settings/modules/MarkovAutomatonSettings.cpp b/src/storm/settings/modules/MarkovAutomatonSettings.cpp deleted file mode 100644 index 470de708f..000000000 --- a/src/storm/settings/modules/MarkovAutomatonSettings.cpp +++ /dev/null @@ -1,32 +0,0 @@ -#include "storm/settings/modules/MarkovAutomatonSettings.h" - -#include "storm/settings/Option.h" -#include "storm/settings/OptionBuilder.h" -#include "storm/settings/ArgumentBuilder.h" -#include "storm/settings/Argument.h" - -#include "storm/settings/SettingsManager.h" - -namespace storm { - namespace settings { - namespace modules { - - const std::string MarkovAutomatonSettings::moduleName = "ma"; - const std::string MarkovAutomatonSettings::techniqueOptionName = "technique"; - - MarkovAutomatonSettings::MarkovAutomatonSettings() : ModuleSettings(moduleName) { - std::vector techniques = {"imca", "unifplus"}; - this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The technique to use to solve bounded reachability queries.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the technique to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(techniques)).setDefaultValueString("imca").build()).build()); - } - - MarkovAutomatonSettings::BoundedReachabilityTechnique MarkovAutomatonSettings::getTechnique() const { - std::string techniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString(); - if (techniqueAsString == "imca") { - return MarkovAutomatonSettings::BoundedReachabilityTechnique::Imca; - } - return MarkovAutomatonSettings::BoundedReachabilityTechnique::UnifPlus; - } - - } - } -} diff --git a/src/storm/settings/modules/MarkovAutomatonSettings.h b/src/storm/settings/modules/MarkovAutomatonSettings.h deleted file mode 100644 index 60cdaa1b4..000000000 --- a/src/storm/settings/modules/MarkovAutomatonSettings.h +++ /dev/null @@ -1,38 +0,0 @@ -#pragma once - -#include "storm/settings/modules/ModuleSettings.h" - -namespace storm { - namespace settings { - namespace modules { - - /*! - * This class represents the settings for Sylvan. - */ - class MarkovAutomatonSettings : public ModuleSettings { - public: - enum class BoundedReachabilityTechnique { Imca, UnifPlus }; - - /*! - * Creates a new set of Markov automaton settings. - */ - MarkovAutomatonSettings(); - - /*! - * Retrieves the technique to use to solve bounded reachability properties. - * - * @return The selected technique. - */ - BoundedReachabilityTechnique getTechnique() const; - - // The name of the module. - static const std::string moduleName; - - private: - // Define the string names of the options as constants. - static const std::string techniqueOptionName; - }; - - } - } -} diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index add033af0..82c2ba59c 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -18,6 +18,7 @@ namespace storm { const std::string MinMaxEquationSolverSettings::precisionOptionName = "precision"; const std::string MinMaxEquationSolverSettings::absoluteOptionName = "absolute"; const std::string MinMaxEquationSolverSettings::lraMethodOptionName = "lramethod"; + const std::string MinMaxEquationSolverSettings::markovAutomatonBoundedReachabilityMethodOptionName = "mamethod"; const std::string MinMaxEquationSolverSettings::valueIterationMultiplicationStyleOptionName = "vimult"; const std::string MinMaxEquationSolverSettings::intervalIterationSymmetricUpdatesOptionName = "symmetricupdates"; const std::string MinMaxEquationSolverSettings::forceBoundsOptionName = "forcebounds"; @@ -37,6 +38,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, lraMethodOptionName, false, "Sets which method is preferred for computing long run averages.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a long run average computation method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lraMethods)).setDefaultValueString("vi").build()).build()); + std::vector maMethods = {"imca", "unifplus"}; + this->addOption(storm::settings::OptionBuilder(moduleName, markovAutomatonBoundedReachabilityMethodOptionName, true, "The method to use to solve bounded reachability queries on MAs.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(maMethods)).setDefaultValueString("unifplus").build()).build()); + std::vector multiplicationStyles = {"gaussseidel", "regular", "gs", "r"}; this->addOption(storm::settings::OptionBuilder(moduleName, valueIterationMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for value iteration.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplication style.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplicationStyles)).setDefaultValueString("gaussseidel").build()).build()); @@ -109,6 +113,14 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown lra solving technique '" << lraMethodString << "'."); } + + MinMaxEquationSolverSettings::MarkovAutomatonBoundedReachabilityMethod MinMaxEquationSolverSettings::getMarkovAutomatonBoundedReachabilityMethod() const { + std::string techniqueAsString = this->getOption(markovAutomatonBoundedReachabilityMethodOptionName).getArgumentByName("name").getValueAsString(); + if (techniqueAsString == "imca") { + return MinMaxEquationSolverSettings::MarkovAutomatonBoundedReachabilityMethod::Imca; + } + return MinMaxEquationSolverSettings::MarkovAutomatonBoundedReachabilityMethod::UnifPlus; + } storm::solver::MultiplicationStyle MinMaxEquationSolverSettings::getValueIterationMultiplicationStyle() const { std::string multiplicationStyleString = this->getOption(valueIterationMultiplicationStyleOptionName).getArgumentByName("name").getValueAsString(); diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.h b/src/storm/settings/modules/MinMaxEquationSolverSettings.h index ce8b5756c..f64988b6a 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.h +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.h @@ -18,6 +18,9 @@ namespace storm { // An enumeration of all available convergence criteria. enum class ConvergenceCriterion { Absolute, Relative }; + // An enumeration of all available bounded reachability methods for MAs. + enum class MarkovAutomatonBoundedReachabilityMethod { Imca, UnifPlus }; + MinMaxEquationSolverSettings(); /*! @@ -90,6 +93,13 @@ namespace storm { */ storm::solver::LraMethod getLraMethod() const; + /*! + * Retrieves the method to be used for bounded reachability on MAs. + * + * @return The selected method. + */ + MarkovAutomatonBoundedReachabilityMethod getMarkovAutomatonBoundedReachabilityMethod() const; + /*! * Retrieves the multiplication style to use in the min-max methods. * @@ -117,6 +127,7 @@ namespace storm { static const std::string precisionOptionName; static const std::string absoluteOptionName; static const std::string lraMethodOptionName; + static const std::string markovAutomatonBoundedReachabilityMethodOptionName; static const std::string valueIterationMultiplicationStyleOptionName; static const std::string intervalIterationSymmetricUpdatesOptionName; static const std::string forceBoundsOptionName; diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 19a2f0aef..c0d7e0460 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -60,7 +60,7 @@ namespace storm { STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast(this->A->getRowGroupCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); if (this->longestSccChainSize) { - std::cout << "Longest SCC chain size is " << this->longestSccChainSize.get() << std::endl; + STORM_LOG_INFO("Longest SCC chain size is " << this->longestSccChainSize.get()); } bool returnValue = true;