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

Changed API such that the command line settings do not occur in the settings anymore. Moreover, to prevent having 15 Boolean arguments, the build options are now part of the API.

tempestpy_adaptions
sjunges 7 years ago
parent
98d124bd06
commit
2c2dc5acd8
2 changed files with 33 additions and 32 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. 35
      src/storm/api/builder.h
  2. 30
      src/storm/cli/cli.cpp

35
src/storm/api/builder.h
View File

@ -23,10 +23,6 @@
#include "storm/builder/ExplicitModelBuilder.h"
#include "storm/builder/jit/ExplicitJitJaniModelBuilder.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/JitBuilderSettings.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotSupportedException.h"
@ -62,29 +58,18 @@ namespace storm {
}
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildChoiceLabels = false, bool buildChoiceOrigins = false, bool buildStateValuations = false) {
storm::builder::BuilderOptions options(formulas);
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet()) {
options.setBuildAllLabels();
options.setBuildAllRewardModels();
options.clearTerminalStates();
}
options.setBuildChoiceLabels(buildChoiceLabels);
options.setBuildChoiceOrigins(buildChoiceOrigins);
options.setBuildStateValuations(buildStateValuations);
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isJitSet()) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, storm::builder::BuilderOptions const& options, bool jit = false, bool doctor = false) {
if (jit) {
STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Cannot use JIT-based model builder for non-JANI model.");
storm::builder::jit::ExplicitJitJaniModelBuilder<ValueType> builder(model.asJaniModel(), options);
if (storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet()) {
if (doctor) {
bool result = builder.doctor();
STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "The JIT-based model builder cannot be used on your system.");
STORM_LOG_INFO("The JIT-based model builder seems to be working.");
}
return builder.build();
} else {
std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator;
@ -99,6 +84,14 @@ namespace storm {
return builder.build();
}
}
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool jit = false, bool doctor = false) {
storm::builder::BuilderOptions options(formulas);
return buildSparseModel<ValueType>(model, options, jit, doctor);
}
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildSparseModel(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components) {

30
src/storm/cli/cli.cpp
View File

@ -4,34 +4,34 @@
#include "storm/models/ModelBase.h"
#include "storm/settings/modules/DebugSettings.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/exceptions/OptionParserException.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/JaniExportSettings.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/JitBuilderSettings.h"
#include "storm/settings/modules/DebugSettings.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/JaniExportSettings.h"
#include "storm/utility/resources.h"
#include "storm/utility/file.h"
#include "storm/utility/storm-version.h"
#include "storm/utility/cli.h"
#include "storm/utility/macros.h"
#include "storm/utility/initialize.h"
#include "storm/utility/Stopwatch.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/ResourceSettings.h"
#include <type_traits>
#include "storm/api/storm.h"
#include "storm/utility/macros.h"
// Includes for the linked libraries and versions header.
#ifdef STORM_HAVE_INTELTBB
@ -370,7 +370,15 @@ namespace storm {
template <typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
return storm::api::buildSparseModel<ValueType>(input.model.get(), createFormulasToRespect(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
storm::builder::BuilderOptions options(createFormulasToRespect(input.properties));
options.setBuildChoiceLabels(ioSettings.isBuildChoiceLabelsSet());
options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
options.setBuildAllLabels(ioSettings.isBuildFullModelSet());
options.setBuildAllRewardModels(ioSettings.isBuildFullModelSet());
if (ioSettings.isBuildFullModelSet()) {
options.clearTerminalStates();
}
return storm::api::buildSparseModel<ValueType>(input.model.get(), options, ioSettings.isJitSet(), storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet());
}
template <typename ValueType>

Write Preview
Loading…
Cancel
Save