Browse Source

Created settings module for TopologicalValueIterationNondeterministicLinearEquationSolver and integrated that with the solver.

Former-commit-id: fa1ad5ce2a
tempestpy_adaptions
David_Korzeniewski 10 years ago
parent
commit
78d3a392a5
  1. 9
      src/settings/SettingsManager.cpp
  2. 10
      src/settings/SettingsManager.h
  3. 58
      src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp
  4. 87
      src/settings/modules/TopologicalValueIterationEquationSolverSettings.h
  5. 16
      src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
  6. 16
      src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h

9
src/settings/SettingsManager.cpp

@ -26,7 +26,8 @@ namespace storm {
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::NativeEquationSolverSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::BisimulationSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GlpkSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GurobiSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GurobiSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::TopologicalValueIterationEquationSolverSettings(*this)));
}
SettingsManager::~SettingsManager() {
@ -506,6 +507,10 @@ namespace storm {
storm::settings::modules::GurobiSettings const& gurobiSettings() {
return dynamic_cast<storm::settings::modules::GurobiSettings const&>(manager().getModule(storm::settings::modules::GurobiSettings::moduleName));
}
}
storm::settings::modules::TopologicalValueIterationEquationSolverSettings const& topologicalValueIterationEquationSolverSettings() {
return dynamic_cast<storm::settings::modules::TopologicalValueIterationEquationSolverSettings const&>(manager().getModule(storm::settings::modules::TopologicalValueIterationEquationSolverSettings::moduleName));
}
}
}

10
src/settings/SettingsManager.h

@ -28,6 +28,7 @@
#include "src/settings/modules/BisimulationSettings.h"
#include "src/settings/modules/GlpkSettings.h"
#include "src/settings/modules/GurobiSettings.h"
#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
#include "src/utility/macros.h"
#include "src/exceptions/OptionParserException.h"
@ -307,7 +308,14 @@ namespace storm {
*
* @return An object that allows accessing the settings of Gurobi.
*/
storm::settings::modules::GurobiSettings const& gurobiSettings();
storm::settings::modules::GurobiSettings const& gurobiSettings();
/*!
* Retrieves the settings of the topological value iteration-based equation solver.
*
* @return An object that allows accessing the settings of the topological value iteration-based equation solver.
*/
storm::settings::modules::TopologicalValueIterationEquationSolverSettings const& topologicalValueIterationEquationSolverSettings();
} // namespace settings
} // namespace storm

58
src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp

@ -0,0 +1,58 @@
#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
#include "src/settings/SettingsManager.h"
namespace storm {
namespace settings {
namespace modules {
const std::string TopologicalValueIterationEquationSolverSettings::moduleName = "topologicalValueIteration";
const std::string TopologicalValueIterationEquationSolverSettings::maximalIterationsOptionName = "maxiter";
const std::string TopologicalValueIterationEquationSolverSettings::maximalIterationsOptionShortName = "i";
const std::string TopologicalValueIterationEquationSolverSettings::precisionOptionName = "precision";
const std::string TopologicalValueIterationEquationSolverSettings::absoluteOptionName = "absolute";
TopologicalValueIterationEquationSolverSettings::TopologicalValueIterationEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
}
bool TopologicalValueIterationEquationSolverSettings::isMaximalIterationCountSet() const {
return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet();
}
uint_fast64_t TopologicalValueIterationEquationSolverSettings::getMaximalIterationCount() const {
return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
}
bool TopologicalValueIterationEquationSolverSettings::isPrecisionSet() const {
return this->getOption(precisionOptionName).getHasOptionBeenSet();
}
double TopologicalValueIterationEquationSolverSettings::getPrecision() const {
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
}
bool TopologicalValueIterationEquationSolverSettings::isConvergenceCriterionSet() const {
return this->getOption(absoluteOptionName).getHasOptionBeenSet();
}
TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion TopologicalValueIterationEquationSolverSettings::getConvergenceCriterion() const {
return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Absolute : TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Relative;
}
bool TopologicalValueIterationEquationSolverSettings::check() const {
bool optionsSet = isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet();
STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect.");
return true;
}
} // namespace modules
} // namespace settings
} // namespace storm

87
src/settings/modules/TopologicalValueIterationEquationSolverSettings.h

@ -0,0 +1,87 @@
#ifndef STORM_SETTINGS_MODULES_TOPOLOGICALVALUEITERATIONSETTINGS_H_
#define STORM_SETTINGS_MODULES_TOPOLOGICALVALUEITERATIONSETTINGS_H_
#include "src/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for topological value iteration.
*/
class TopologicalValueIterationEquationSolverSettings : public ModuleSettings {
public:
// An enumeration of all available convergence criteria.
enum class ConvergenceCriterion { Absolute, Relative };
/*!
* Creates a new set of topological value iteration settings that is managed by the given manager.
*
* @param settingsManager The responsible manager.
*/
TopologicalValueIterationEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
/*!
* Retrieves whether the maximal iteration count has been set.
*
* @return True iff the maximal iteration count has been set.
*/
bool isMaximalIterationCountSet() const;
/*!
* Retrieves the maximal number of iterations to perform until giving up on converging.
*
* @return The maximal iteration count.
*/
uint_fast64_t getMaximalIterationCount() const;
/*!
* Retrieves whether the precision has been set.
*
* @return True iff the precision has been set.
*/
bool isPrecisionSet() const;
/*!
* Retrieves the precision that is used for detecting convergence.
*
* @return The precision to use for detecting convergence.
*/
double getPrecision() const;
/*!
* Retrieves whether the convergence criterion has been set.
*
* @return True iff the convergence criterion has been set.
*/
bool isConvergenceCriterionSet() const;
/*!
* Retrieves the selected convergence criterion.
*
* @return The selected convergence criterion.
*/
ConvergenceCriterion getConvergenceCriterion() const;
bool check() const override;
// 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;
static const std::string maximalIterationsOptionName;
static const std::string maximalIterationsOptionShortName;
static const std::string precisionOptionName;
static const std::string absoluteOptionName;
};
} // namespace modules
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_TOPOLOGICALVALUEITERATIONSETTINGS_H_ */

16
src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp

@ -3,7 +3,7 @@
#include <utility>
#include <chrono>
#include "src/settings/Settings.h"
#include "src/settings/SettingsManager.h"
#include "src/utility/vector.h"
#include "src/utility/graph.h"
#include "src/models/PseudoModel.h"
@ -26,12 +26,16 @@ namespace storm {
template<typename ValueType>
TopologicalValueIterationNondeterministicLinearEquationSolver<ValueType>::TopologicalValueIterationNondeterministicLinearEquationSolver() {
// Get the settings object to customize solving.
storm::settings::Settings* settings = storm::settings::Settings::getInstance();
//storm::settings::Settings* settings = storm::settings::Settings::getInstance();
auto settings = storm::settings::topologicalValueIterationEquationSolverSettings();
// Get appropriate settings.
this->maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger();
this->precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
this->relative = !settings->isSet("absolute");
//this->maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger();
//this->precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
//this->relative = !settings->isSet("absolute");
this->maximalNumberOfIterations = settings.getMaximalIterationCount();
this->precision = settings.getPrecision();
this->relative = (settings.getConvergenceCriterion() == TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Relative);
}
template<typename ValueType>

16
src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h

@ -48,13 +48,13 @@ namespace storm {
std::vector<std::pair<bool, storm::storage::StateBlock>> getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition<ValueType> const& sccDecomposition, std::vector<uint_fast64_t> const& topologicalSort, storm::storage::SparseMatrix<ValueType> const& matrix) const;
};
template <typename ValueType>
bool __basicValueIteration_mvReduce_uint64_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<ValueType>> const& columnIndicesAndValues, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
template <typename IndexType, typename ValueType>
bool __basicValueIteration_mvReduce_uint64_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<IndexType, ValueType>> const& columnIndicesAndValues, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
//
throw;
}
template <>
inline bool __basicValueIteration_mvReduce_uint64_minimize<double>(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
inline bool __basicValueIteration_mvReduce_uint64_minimize<uint_fast64_t, double>(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
#ifdef STORM_HAVE_CUDAFORSTORM
return basicValueIteration_mvReduce_uint64_double_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
@ -62,7 +62,7 @@ namespace storm {
#endif
}
template <>
inline bool __basicValueIteration_mvReduce_uint64_minimize<float>(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<float>> const& columnIndicesAndValues, std::vector<float>& x, std::vector<float> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
inline bool __basicValueIteration_mvReduce_uint64_minimize<uint_fast64_t, float>(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<uint_fast64_t, float>> const& columnIndicesAndValues, std::vector<float>& x, std::vector<float> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
#ifdef STORM_HAVE_CUDAFORSTORM
return basicValueIteration_mvReduce_uint64_float_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
@ -70,13 +70,13 @@ namespace storm {
#endif
}
template <typename ValueType>
bool __basicValueIteration_mvReduce_uint64_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<ValueType>> const& columnIndicesAndValues, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
template <typename IndexType, typename ValueType>
bool __basicValueIteration_mvReduce_uint64_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<IndexType, ValueType>> const& columnIndicesAndValues, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
//
throw;
}
template <>
inline bool __basicValueIteration_mvReduce_uint64_maximize<double>(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
inline bool __basicValueIteration_mvReduce_uint64_maximize<uint_fast64_t, double>(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> const& columnIndicesAndValues, std::vector<double>& x, std::vector<double> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
#ifdef STORM_HAVE_CUDAFORSTORM
return basicValueIteration_mvReduce_uint64_double_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
@ -84,7 +84,7 @@ namespace storm {
#endif
}
template <>
inline bool __basicValueIteration_mvReduce_uint64_maximize<float>(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<float>> const& columnIndicesAndValues, std::vector<float>& x, std::vector<float> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
inline bool __basicValueIteration_mvReduce_uint64_maximize<uint_fast64_t, float>(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector<uint_fast64_t> const& matrixRowIndices, std::vector<storm::storage::MatrixEntry<uint_fast64_t, float>> const& columnIndicesAndValues, std::vector<float>& x, std::vector<float> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, size_t& iterationCount) {
#ifdef STORM_HAVE_CUDAFORSTORM
return basicValueIteration_mvReduce_uint64_float_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else

Loading…
Cancel
Save