diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 868c47bba..ca21f99fc 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -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 - std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildChoiceLabels = false, bool buildChoiceOrigins = false, bool buildStateValuations = false) { - storm::builder::BuilderOptions options(formulas); - - if (storm::settings::getModule().isBuildFullModelSet()) { - options.setBuildAllLabels(); - options.setBuildAllRewardModels(); - options.clearTerminalStates(); - } - options.setBuildChoiceLabels(buildChoiceLabels); - options.setBuildChoiceOrigins(buildChoiceOrigins); - options.setBuildStateValuations(buildStateValuations); - - if (storm::settings::getModule().isJitSet()) { + std::shared_ptr> 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 builder(model.asJaniModel(), options); - - if (storm::settings::getModule().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> generator; @@ -99,6 +84,14 @@ namespace storm { return builder.build(); } } + + template + std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool jit = false, bool doctor = false) { + storm::builder::BuilderOptions options(formulas); + return buildSparseModel(model, options, jit, doctor); + + + } template> std::shared_ptr> buildSparseModel(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components) { diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 343006c6d..42a76a7b2 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -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 #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 std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { auto counterexampleGeneratorSettings = storm::settings::getModule(); - return storm::api::buildSparseModel(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(input.model.get(), options, ioSettings.isJitSet(), storm::settings::getModule().isDoctorSet()); } template