sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Move settings to separate file

tempestpy_adaptions
Jip Spel 6 years ago
parent
6b8997c6ba
commit
2883f81be1
6 changed files with 124 additions and 67 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      src/storm-pars-cli/storm-pars.cpp
  2. 5
      src/storm-pars/settings/ParsSettings.cpp
  3. 54
      src/storm-pars/settings/modules/MonotonicitySettings.cpp
  4. 60
      src/storm-pars/settings/modules/MonotonicitySettings.h
  5. 32
      src/storm-pars/settings/modules/ParametricSettings.cpp
  6. 30
      src/storm-pars/settings/modules/ParametricSettings.h

10
src/storm-pars-cli/storm-pars.cpp
View File

@ -13,6 +13,7 @@
#include "storm-pars/settings/ParsSettings.h"
#include "storm-pars/settings/modules/ParametricSettings.h"
#include "storm-pars/settings/modules/MonotonicitySettings.h"
#include "storm-pars/settings/modules/RegionSettings.h"
#include "storm-pars/transformer/SparseParametricMdpSimplifier.h"
@ -558,6 +559,7 @@ namespace storm {
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
auto parSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
auto monSettings = storm::settings::getModule<storm::settings::modules::MonotonicitySettings>();
auto engine = coreSettings.getEngine();
STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models.");
@ -595,7 +597,7 @@ namespace storm {
}
}
if (parSettings.isMonotonicityAnalysisSet()) {
if (monSettings.isMonotonicityAnalysisSet()) {
// Simplify the model
storm::utility::Stopwatch simplifyingWatch(true);
if (model->isOfType(storm::models::ModelType::Dtmc)) {
@ -650,7 +652,7 @@ namespace storm {
}
if (parSettings.isSccEliminationSet()) {
if (monSettings.isSccEliminationSet()) {
storm::utility::Stopwatch eliminationWatch(true);
// TODO: check for correct Model type
STORM_PRINT("Applying scc elimination" << std::endl);
@ -714,11 +716,11 @@ namespace storm {
model->printModelInformationToStream(std::cout);
}
if (parSettings.isMonotonicityAnalysisSet()) {
if (monSettings.isMonotonicityAnalysisSet()) {
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
// Monotonicity
storm::utility::Stopwatch monotonicityWatch(true);
auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(model, formulas, parSettings.isValidateAssumptionsSet(), parSettings.getNumberOfSamples(), parSettings.getMonotonicityAnalysisPrecision());
auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(model, formulas, monSettings.isValidateAssumptionsSet(), monSettings.getNumberOfSamples(), monSettings.getMonotonicityAnalysisPrecision());
monotonicityChecker.checkMonotonicity();
monotonicityWatch.stop();
STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl

5
src/storm-pars/settings/ParsSettings.cpp
View File

@ -2,6 +2,8 @@
#include "storm-pars/settings/modules/ParametricSettings.h"
#include "storm-pars/settings/modules/RegionSettings.h"
#include "storm-pars/settings/modules/MonotonicitySettings.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
@ -28,12 +30,13 @@ namespace storm {
namespace settings {
void initializeParsSettings(std::string const& name, std::string const& executableName) {
storm::settings::mutableManager().setName(name, executableName);
// Register relevant settings modules.
storm::settings::addModule<storm::settings::modules::GeneralSettings>();
storm::settings::addModule<storm::settings::modules::IOSettings>();
storm::settings::addModule<storm::settings::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::ParametricSettings>();
storm::settings::addModule<storm::settings::modules::MonotonicitySettings>();
storm::settings::addModule<storm::settings::modules::RegionSettings>();
storm::settings::addModule<storm::settings::modules::BuildSettings>();
storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();

54
src/storm-pars/settings/modules/MonotonicitySettings.cpp
View File

@ -0,0 +1,54 @@
#include "storm-pars/settings/modules/MonotonicitySettings.h"
#include "storm/settings/Option.h"
#include "storm/settings/OptionBuilder.h"
#include "storm/settings/ArgumentBuilder.h"
#include "storm/settings/Argument.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/IllegalArgumentValueException.h"
namespace storm {
namespace settings {
namespace modules {
const std::string MonotonicitySettings::moduleName = "monotonicity";
const std::string MonotonicitySettings::monotonicityAnalysis = "monotonicity-analysis";
const std::string MonotonicitySettings::sccElimination = "mon-elim-scc";
const std::string MonotonicitySettings::validateAssumptions = "mon-validate-assumptions";
const std::string MonotonicitySettings::samplesMonotonicityAnalysis = "mon-samples";
const std::string MonotonicitySettings::precision = "mon-precision";
MonotonicitySettings::MonotonicitySettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, monotonicityAnalysis, false, "Sets whether monotonicity analysis is done").setIsAdvanced().build());
this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated in the monotonicity analysis").setIsAdvanced().build());
this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").setIsAdvanced().build());
this->addOption(storm::settings::OptionBuilder(moduleName, samplesMonotonicityAnalysis, false, "Sets whether monotonicity should be checked on samples").setIsAdvanced()
.addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mon-samples", "The number of samples taken in monotonicity-analysis can be given, default is 0, no samples").setDefaultValueUnsignedInteger(0).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, precision, false, "Sets precision of monotonicity checking on samples").setIsAdvanced()
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("mon-precision", "The precision of checking monotonicity on samples, default is 1e-6").setDefaultValueDouble(0.000001).build()).build());
}
bool MonotonicitySettings::isMonotonicityAnalysisSet() const {
return this->getOption(monotonicityAnalysis).getHasOptionBeenSet();
}
bool MonotonicitySettings::isSccEliminationSet() const {
return this->getOption(sccElimination).getHasOptionBeenSet();
}
bool MonotonicitySettings::isValidateAssumptionsSet() const {
return this->getOption(validateAssumptions).getHasOptionBeenSet();
}
uint_fast64_t MonotonicitySettings::getNumberOfSamples() const {
return this->getOption(samplesMonotonicityAnalysis).getArgumentByName("mon-samples").getValueAsUnsignedInteger();
}
double MonotonicitySettings::getMonotonicityAnalysisPrecision() const {
return this->getOption(precision).getArgumentByName("mon-precision").getValueAsDouble();
}
} // namespace modules
} // namespace settings
} // namespace storm

60
src/storm-pars/settings/modules/MonotonicitySettings.h
View File

@ -0,0 +1,60 @@
#ifndef STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_
#define STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_
#include "storm/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for monotonicity checking.
*/
class MonotonicitySettings : public ModuleSettings {
public:
/*!
* Creates a new set of monotonicity checking settings.
*/
MonotonicitySettings();
/*!
* Retrieves whether monotonicity analysis should be applied.
*/
bool isMonotonicityAnalysisSet() const;
/*!
* Retrieves whether SCCs in the monotonicity analysis should be eliminated.
*/
bool isSccEliminationSet() const;
/*!
* Retrieves whether assumptions in monotonicity analysis should be validated
*/
bool isValidateAssumptionsSet() const;
/*!
* Retrieves the number of samples used for sampling in the monotonicity analysis
*/
uint_fast64_t getNumberOfSamples() const;
/*!
* Retrieves the precision for the extremal value
*/
double getMonotonicityAnalysisPrecision() const;
const static std::string moduleName;
private:
const static std::string monotonicityAnalysis;
const static std::string sccElimination;
const static std::string validateAssumptions;
const static std::string samplesMonotonicityAnalysis;
const static std::string precision;
};
} // namespace modules
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_ */

32
src/storm-pars/settings/modules/ParametricSettings.cpp
View File

@ -21,11 +21,6 @@ namespace storm {
const std::string ParametricSettings::samplesOptionName = "samples";
const std::string ParametricSettings::samplesGraphPreservingOptionName = "samples-graph-preserving";
const std::string ParametricSettings::sampleExactOptionName = "sample-exact";
const std::string ParametricSettings::monotonicityAnalysis = "monotonicity-analysis";
const std::string ParametricSettings::sccElimination = "mon-elim-scc";
const std::string ParametricSettings::validateAssumptions = "mon-validate-assumptions";
const std::string ParametricSettings::samplesMonotonicityAnalysis = "mon-samples";
const std::string ParametricSettings::precision = "mon-precision";
ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.")
@ -37,14 +32,6 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("samples", "The samples are semicolon-separated entries of the form 'Var1=Val1:Val2:...:Valk,Var2=... that span the sample spaces.").setDefaultValueString("").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, samplesGraphPreservingOptionName, false, "Sets whether it can be assumed that the samples are graph-preserving.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, sampleExactOptionName, false, "Sets whether to sample using exact arithmetic.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, monotonicityAnalysis, false, "Sets whether monotonicity analysis is done").build());
this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated in the monotonicity analysis").build());
this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").build());
this->addOption(storm::settings::OptionBuilder(moduleName, samplesMonotonicityAnalysis, false, "Sets whether monotonicity should be checked on samples")
.addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mon-samples", "The number of samples taken in monotonicity-analysis can be given, default is 0, no samples").setDefaultValueUnsignedInteger(0).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, precision, false, "Sets precision of monotonicity checking on samples")
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("mon-precision", "The precision of checking monotonicity on samples, default is 1e-6").setDefaultValueDouble(0.000001).build()).build());
}
bool ParametricSettings::exportResultToFile() const {
@ -79,25 +66,6 @@ namespace storm {
return this->getOption(sampleExactOptionName).getHasOptionBeenSet();
}
bool ParametricSettings::isMonotonicityAnalysisSet() const {
return this->getOption(monotonicityAnalysis).getHasOptionBeenSet();
}
bool ParametricSettings::isSccEliminationSet() const {
return this->getOption(sccElimination).getHasOptionBeenSet();
}
bool ParametricSettings::isValidateAssumptionsSet() const {
return this->getOption(validateAssumptions).getHasOptionBeenSet();
}
uint_fast64_t ParametricSettings::getNumberOfSamples() const {
return this->getOption(samplesMonotonicityAnalysis).getArgumentByName("mon-samples").getValueAsUnsignedInteger();
}
double ParametricSettings::getMonotonicityAnalysisPrecision() const {
return this->getOption(precision).getArgumentByName("mon-precision").getValueAsDouble();
}
} // namespace modules
} // namespace settings
} // namespace storm

30
src/storm-pars/settings/modules/ParametricSettings.h
View File

@ -64,31 +64,6 @@ namespace storm {
*/
bool isSampleExactSet() const;
/*!
* Retrieves whether monotonicity analysis should be applied.
*/
bool isMonotonicityAnalysisSet() const;
/*!
* Retrieves whether SCCs in the monotonicity analysis should be eliminated.
*/
bool isSccEliminationSet() const;
/*!
* Retrieves whether assumptions in monotonicity analysis should be validated
*/
bool isValidateAssumptionsSet() const;
/*!
* Retrieves the number of samples used for sampling in the monotonicity analysis
*/
uint_fast64_t getNumberOfSamples() const;
/*!
* Retrieves the precision for the extremal value
*/
double getMonotonicityAnalysisPrecision() const;
const static std::string moduleName;
private:
@ -100,11 +75,6 @@ namespace storm {
const static std::string samplesOptionName;
const static std::string samplesGraphPreservingOptionName;
const static std::string sampleExactOptionName;
const static std::string monotonicityAnalysis;
const static std::string sccElimination;
const static std::string validateAssumptions;
const static std::string samplesMonotonicityAnalysis;
const static std::string precision;
};
} // namespace modules

Write Preview
Loading…
Cancel
Save