Browse Source

introduced model checker settings

tempestpy_adaptions
TimQu 7 years ago
parent
commit
7d705240ce
  1. 2
      src/storm-dft/settings/DftSettings.cpp
  2. 5
      src/storm-pars/settings/ParsSettings.cpp
  3. 1
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  4. 2
      src/storm/settings/SettingsManager.cpp
  5. 28
      src/storm/settings/modules/ModelCheckerSettings.cpp
  6. 36
      src/storm/settings/modules/ModelCheckerSettings.h

2
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::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();
storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>();

5
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::modules::RegionSettings>();
storm::settings::addModule<storm::settings::modules::BuildSettings>();
storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::SylvanSettings>();
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
@ -47,7 +47,6 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::GameSolverSettings>();
storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
storm::settings::addModule<storm::settings::modules::TopologicalCudaMinMaxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::ResourceSettings>();
storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();

1
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"

2
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::modules::IOSettings>();
storm::settings::addModule<storm::settings::modules::BuildSettings>();
storm::settings::addModule<storm::settings::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
storm::settings::addModule<storm::settings::modules::CuddSettings>();

28
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

36
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
Loading…
Cancel
Save