From 2c2dc5acd89bcdeecf96d2640b6c0096b700bf68 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Sun, 13 Aug 2017 15:36:47 +0200
Subject: [PATCH] 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.

---
 src/storm/api/builder.h | 35 ++++++++++++++---------------------
 src/storm/cli/cli.cpp   | 30 +++++++++++++++++++-----------
 2 files changed, 33 insertions(+), 32 deletions(-)

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<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) {
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 <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>