diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 8fdfb3054..20f15344b 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -10,6 +10,7 @@ #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/utility/macros.h" #include "storm/utility/vector.h" @@ -134,19 +135,19 @@ 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(std::vector const& exitRateVector, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, std::vector>& vd, std::vector>& vu, std::vector>& wu){ std::ofstream logfile("U+logfile.txt", std::ios::app); - auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); + auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); auto numberOfStates = fullTransitionMatrix.getRowGroupCount(); logfile << "number of states = num of row group count " << numberOfStates << "\n"; - for (int i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) { + for (uint_fast64_t i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) { logfile << " from node " << i << " "; auto from = rowGroupIndices[i]; auto to = rowGroupIndices[i+1]; - for (auto j = from ; j< to; j++){ + for (auto j = from ; j < to; j++){ for (auto &v : fullTransitionMatrix.getRow(j)) { if (markovianStates[i]){ logfile << v.getValue() *exitRateVector[i] << " -> "<< v.getColumn() << "\t"; @@ -160,24 +161,24 @@ namespace storm { logfile << "\n"; logfile << "vd: \n"; - for (int i =0 ; i::SupportsExponential, int>::type=0> + template ::SupportsExponential, int>::type> void SparseMarkovAutomatonCslHelper::calculateVu(uint64_t k, uint64_t node, ValueType lambda, std::vector>& vu, std::vector>& wu, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){ if (vu[k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation. uint64_t N = vu.size()-1; auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); ValueType res =0; - for (long i = k ; i < N ; i++ ){ + for (uint_fast64_t i = k ; i < N ; i++ ){ if (wu[N-1-(i-k)][node]==-1){ calculateWu((N-1-(i-k)),node,lambda,wu,fullTransitionMatrix,markovianStates,psiStates); } @@ -214,11 +215,11 @@ namespace storm { vu[k][node]=res; } - template ::SupportsExponential, int>::type=0> + template ::SupportsExponential, int>::type> void SparseMarkovAutomatonCslHelper::calculateWu(uint64_t k, uint64_t node, ValueType lambda, std::vector>& wu, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){ if (wu[k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation. uint64_t N = wu.size()-1; - auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); + auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); ValueType res; if (k==N){ @@ -267,7 +268,7 @@ namespace storm { wu[k][node]=res; } - template ::SupportsExponential, int>::type=0> + template ::SupportsExponential, int>::type> void SparseMarkovAutomatonCslHelper::calculateVd(uint64_t k, uint64_t node, ValueType lambda, std::vector>& vd, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){ std::ofstream logfile("U+logfile.txt", std::ios::app); @@ -275,7 +276,7 @@ namespace storm { if (vd[k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation. logfile << "calculating vd for k = " << k << " node "<< node << " \t"; uint64_t N = vd.size()-1; - auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); + auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); ValueType res; if (k==N){ @@ -337,13 +338,15 @@ namespace storm { template ::SupportsExponential, int>::type> std::vector SparseMarkovAutomatonCslHelper::unifPlus( std::pair const& boundsPair, std::vector const& exitRateVector, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){ + STORM_LOG_TRACE("Using UnifPlus to compute bounded until probabilities."); + std::ofstream logfile("U+logfile.txt", std::ios::app); ValueType maxNorm = 0; //bitvectors to identify different kind of states - storm::storage::BitVector const &markovianNonGoalStates = markovianStates & ~psiStates; - storm::storage::BitVector const &probabilisticNonGoalStates = ~markovianStates & ~psiStates; - storm::storage::BitVector const &allStates = markovianStates | ~markovianStates; +// storm::storage::BitVector const &markovianNonGoalStates = markovianStates & ~psiStates; +// storm::storage::BitVector const &probabilisticNonGoalStates = ~markovianStates & ~psiStates; + storm::storage::BitVector allStates(markovianStates.size(), true); //vectors to save calculation std::vector> vd,vu,wu; @@ -371,7 +374,7 @@ namespace storm { N = ceil(lambda*T*exp(2)-log(kappa*epsilon)); // (3) uniform - just applied to markovian states - for (int i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) { + for (uint_fast64_t i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) { if (!markovianStates[i]) { continue; } @@ -428,15 +431,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) { - return unifPlus(boundsPair, exitRateVector, transitionMatrix, markovianStates, psiStates); - /* + 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) { + STORM_LOG_TRACE("Using IMCA's technique to compute bounded until probabilities."); + uint64_t numberOfStates = transitionMatrix.getRowGroupCount(); - + // 'Unpack' the bounds to make them more easily accessible. double lowerBound = boundsPair.first; double upperBound = boundsPair.second; - + // (1) Compute the accuracy we need to achieve the required error bound. ValueType maxExitRate = 0; for (auto value : exitRateVector) { @@ -489,7 +492,21 @@ namespace storm { storm::utility::vector::setVectorValues(result, probabilisticNonGoalStates, vProbabilistic); storm::utility::vector::setVectorValues(result, markovianNonGoalStates, vMarkovian); return result; - }*/ + } + } + + 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) { + + auto const& markovAutomatonSettings = storm::settings::getModule(); + if (markovAutomatonSettings.getTechnique() == storm::settings::modules::MarkovAutomatonSettings::BoundedReachabilityTechnique::Imca) { + return computeBoundedUntilProbabilitiesImca(dir, transitionMatrix, exitRateVector, markovianStates, psiStates, boundsPair, minMaxLinearEquationSolverFactory); + } else { + STORM_LOG_ASSERT(markovAutomatonSettings.getTechnique() == storm::settings::modules::MarkovAutomatonSettings::BoundedReachabilityTechnique::UnifPlus, "Unknown solution technique."); + + // Why is optimization direction not passed? + return unifPlus(boundsPair, exitRateVector, transitionMatrix, markovianStates, psiStates); + } } template ::SupportsExponential, int>::type> diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 1dc6dcec5..ff27180bd 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -33,6 +33,9 @@ namespace storm { template ::SupportsExponential, int>::type = 0> static std::vector 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); + 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); + template ::SupportsExponential, int>::type = 0> static std::vector 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); diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 188d1cba2..38e5ff10a 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -37,6 +37,7 @@ #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/utility/macros.h" #include "storm/utility/file.h" #include "storm/settings/Option.h" @@ -534,6 +535,7 @@ namespace storm { 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 new file mode 100644 index 000000000..470de708f --- /dev/null +++ b/src/storm/settings/modules/MarkovAutomatonSettings.cpp @@ -0,0 +1,32 @@ +#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 new file mode 100644 index 000000000..60cdaa1b4 --- /dev/null +++ b/src/storm/settings/modules/MarkovAutomatonSettings.h @@ -0,0 +1,38 @@ +#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/SylvanSettings.h b/src/storm/settings/modules/SylvanSettings.h index b4eed806b..b218cbdfc 100644 --- a/src/storm/settings/modules/SylvanSettings.h +++ b/src/storm/settings/modules/SylvanSettings.h @@ -13,7 +13,7 @@ namespace storm { class SylvanSettings : public ModuleSettings { public: /*! - * Creates a new set of CUDD settings. + * Creates a new set of Sylvan settings. */ SylvanSettings();