diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp index b80afa2ce..845ba6aa9 100644 --- a/src/storm-dft/settings/DftSettings.cpp +++ b/src/storm-dft/settings/DftSettings.cpp @@ -9,6 +9,7 @@ #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/EigenEquationSolverSettings.h" +#include "storm/settings/modules/ModelCheckerSettings.h" #include "storm/settings/modules/GmmxxEquationSolverSettings.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" #include "storm/settings/modules/EliminationSettings.h" @@ -33,6 +34,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm-pars/settings/ParsSettings.cpp b/src/storm-pars/settings/ParsSettings.cpp index 4b182760b..f7eb39604 100644 --- a/src/storm-pars/settings/ParsSettings.cpp +++ b/src/storm-pars/settings/ParsSettings.cpp @@ -9,6 +9,7 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/BuildSettings.h" +#include "storm/settings/modules/ModelCheckerSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/SylvanSettings.h" #include "storm/settings/modules/EigenEquationSolverSettings.h" @@ -36,8 +37,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); - - + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); @@ -47,7 +47,6 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); - storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 6f63bd94a..fd4ca4ff1 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -23,6 +23,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/ModelCheckerSettings.h" #include "storm/utility/Stopwatch.h" #include "storm/utility/ProgressMeasurement.h" diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 2d99b739c..a97fc9ea3 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -15,6 +15,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/ModelcheckerSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/CounterexampleGeneratorSettings.h" #include "storm/settings/modules/CuddSettings.h" @@ -513,6 +514,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm/settings/modules/ModelCheckerSettings.cpp b/src/storm/settings/modules/ModelCheckerSettings.cpp new file mode 100644 index 000000000..ec5ec7921 --- /dev/null +++ b/src/storm/settings/modules/ModelCheckerSettings.cpp @@ -0,0 +1,28 @@ +#include "storm/settings/modules/ModelCheckerSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/SettingMemento.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" + + +namespace storm { + namespace settings { + namespace modules { + + const std::string GeneralSettings::moduleName = "modelchecker"; + const std::string GeneralSettings::filterRewZeroOptionName = "filterrewzero"; + + ModelCheckerSettings::ModelCheckerSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, filterRewZeroOptionName, false, "If set, states with reward zero are filtered out, potentially reducing the size of the equation system").build()); + } + + bool ModelCheckerSettings::isFilterRewZeroSet() const { + return this->getOption(filterRewZeroOptionName).getHasOptionBeenSet(); + } + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm/settings/modules/ModelCheckerSettings.h b/src/storm/settings/modules/ModelCheckerSettings.h new file mode 100644 index 000000000..4c6a1dfd6 --- /dev/null +++ b/src/storm/settings/modules/ModelCheckerSettings.h @@ -0,0 +1,36 @@ +#pragma once + +#include "storm-config.h" +#include "storm/settings/modules/ModuleSettings.h" + +#include "storm/builder/ExplorationOrder.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the general settings. + */ + class ModelCheckerSettings : public ModuleSettings { + public: + + /*! + * Creates a new set of general settings. + */ + ModelCheckerSettings(); + + bool isFilterRewZeroSet() 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 filterRewZeroOptionName; + }; + + } // namespace modules + } // namespace settings +} // namespace storm +