From 1f1b60e6de9a857641100a3856187504504007ca Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 1 Oct 2014 12:47:05 +0200
Subject: [PATCH 1/3] Added macros that can be used for printing and warnings.
 Included Dennis' fix for model checking of Markov automata. Added check
 methods to the settings modules that check whether the specified options are
 non-contradictive.

Former-commit-id: 18c168795833961d1fd50a8fe4866fc73c6bf984
---
 .../SparseMarkovAutomatonCslModelChecker.h    |  4 +-
 src/settings/SettingsManager.cpp              |  9 ++++
 src/settings/SettingsManager.h                |  5 +++
 .../CounterexampleGeneratorSettings.cpp       | 15 ++++++-
 .../modules/CounterexampleGeneratorSettings.h |  4 +-
 src/settings/modules/GeneralSettings.cpp      | 12 +++++
 src/settings/modules/GeneralSettings.h        |  2 +
 src/settings/modules/GlpkSettings.cpp         | 12 +++++
 src/settings/modules/GlpkSettings.h           |  9 ++++
 .../modules/GmmxxEquationSolverSettings.cpp   | 32 ++++++++++++++
 .../modules/GmmxxEquationSolverSettings.h     | 44 +++++++++++++++++++
 src/settings/modules/GurobiSettings.cpp       | 16 +++++++
 src/settings/modules/GurobiSettings.h         | 16 +++++++
 .../modules/NativeEquationSolverSettings.cpp  | 24 ++++++++++
 .../modules/NativeEquationSolverSettings.h    | 30 +++++++++++++
 src/utility/cli.h                             |  2 +-
 src/utility/macros.h                          | 34 ++++++++++++++
 17 files changed, 265 insertions(+), 5 deletions(-)

diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
index b927b6203..80ba611aa 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
@@ -494,7 +494,7 @@ namespace storm {
                             storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state));
                             
                             for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) {
-                                constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn()));
+                                constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())) * storm::expressions::Expression::createDoubleLiteral(element.getValue());
                             }
                             
                             constraint = constraint + storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne<ValueType>() / exitRates[state]) * storm::expressions::Expression::createDoubleVariable("k");
@@ -512,7 +512,7 @@ namespace storm {
                                 storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state));
 
                                 for (auto element : transitionMatrix.getRow(choice)) {
-                                    constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn()));
+                                    constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())) *  storm::expressions::Expression::createDoubleLiteral(element.getValue());
                                 }
                                 
                                 storm::expressions::Expression rightHandSide = storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero<ValueType>());
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index d8b9284d9..53d31f6f0 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -110,6 +110,9 @@ namespace storm {
             if (optionActive) {
                 setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache);
             }
+            
+            // Finally check whether all modules are okay with the current settings.
+            this->checkAllModules();
         }
         
         void SettingsManager::setFromConfigurationFile(std::string const& configFilename) {
@@ -325,6 +328,12 @@ namespace storm {
             }
         }
         
+        void SettingsManager::checkAllModules() const {
+            for (auto const& nameModulePair : this->modules) {
+                nameModulePair.second->check();
+            }
+        }
+        
         SettingsManager const& manager() {
             return SettingsManager::manager();
         }
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index 94d309813..1c77e1d56 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -179,6 +179,11 @@ namespace storm {
              */
             static void addOptionToMap(std::string const& name, std::shared_ptr<Option> const& option, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>>& optionMap);
             
+            /*!
+             * Checks all modules for consistency by calling their respective check method.
+             */
+            void checkAllModules() const;
+            
             /*!
              * Retrieves the (print) length of the longest option of all modules.
              *
diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp
index e2e29834d..6191b1643 100644
--- a/src/settings/modules/CounterexampleGeneratorSettings.cpp
+++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp
@@ -1,6 +1,7 @@
 #include "src/settings/modules/CounterexampleGeneratorSettings.h"
 
 #include "src/settings/SettingsManager.h"
+#include "src/exceptions/InvalidSettingsException.h"
 
 namespace storm {
     namespace settings {
@@ -19,7 +20,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
             }
             
-            bool CounterexampleGeneratorSettings::isMinimalCommandGenerationSet() const {
+            bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const {
                 return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet();
             }
             
@@ -40,6 +41,18 @@ namespace storm {
                 return this->getOption(schedulerCutsOptionName).getHasOptionBeenSet();
             }
             
+            bool CounterexampleGeneratorSettings::check() const {
+                // Ensure that the model was given either symbolically or explicitly.
+                STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified symbolically.");
+                
+                if (isMinimalCommandSetGenerationSet()) {
+                    STORM_LOG_WARN_COND(isUseMaxSatBasedMinimalCommandSetGenerationSet() || !isEncodeReachabilitySet(), "Encoding reachability is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");
+                    STORM_LOG_WARN_COND(isUseMilpBasedMinimalCommandSetGenerationSet() || !isUseSchedulerCutsSet(), "Using scheduler cuts is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");
+                }
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/CounterexampleGeneratorSettings.h b/src/settings/modules/CounterexampleGeneratorSettings.h
index 680224b5a..049747183 100644
--- a/src/settings/modules/CounterexampleGeneratorSettings.h
+++ b/src/settings/modules/CounterexampleGeneratorSettings.h
@@ -24,7 +24,7 @@ namespace storm {
                  *
                  * @return True iff a minimal command set counterexample is to be generated.
                  */
-                bool isMinimalCommandGenerationSet() const;
+                bool isMinimalCommandSetGenerationSet() const;
                 
                 /*!
                  * Retrieves whether the MILP-based technique is to be used to generate a minimal command set
@@ -58,6 +58,8 @@ namespace storm {
                  */
                 bool isUseSchedulerCutsSet() const;
                 
+                bool check() const override;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 45d3b58a6..585bcfdfb 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -2,6 +2,7 @@
 
 #include "src/settings/SettingsManager.h"
 #include "src/settings/SettingMemento.h"
+#include "src/exceptions/InvalidSettingsException.h"
 
 namespace storm {
     namespace settings {
@@ -266,6 +267,17 @@ namespace storm {
                 return this->getOption(statisticsOptionName).getHasOptionBeenSet();
             }
             
+            bool GeneralSettings::check() const {
+                // Ensure that the model was given either symbolically or explicitly.
+                STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both.");
+                
+                // Make sure that one "source" for properties is given.
+                uint_fast64_t propertySources = 0 + (isPctlPropertySet() ? 1 : 0) + (isPctlFileSet() ? 1 : 0) + (isCslPropertySet() ? + 1 : 0) + (isCslFileSet() ? 1 : 0) + (isLtlPropertySet() ? 1 : 0) + (isLtlFileSet() ? 1 : 0);
+                STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify exactly one source of properties.");
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 10e4aa77d..75f48d8f1 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -313,6 +313,8 @@ namespace storm {
                  * @return True iff statistics are to be shown for counterexample generation.
                  */
                 bool isShowStatisticsSet() const;
+                
+                bool check() const override;
 
                 // The name of the module.
                 static const std::string moduleName;
diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp
index c45eb93a5..030a69006 100644
--- a/src/settings/modules/GlpkSettings.cpp
+++ b/src/settings/modules/GlpkSettings.cpp
@@ -19,10 +19,22 @@ namespace storm {
                 return this->getOption(outputOptionName).getHasOptionBeenSet();
             }
             
+            bool GlpkSettings::isIntegerToleranceSet() const {
+                return this->getOption(integerToleranceOption).getHasOptionBeenSet();
+            }
+            
             double GlpkSettings::getIntegerTolerance() const {
                 return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
             }
             
+            bool GlpkSettings::check() const {
+                if (isOutputSet() || isIntegerToleranceSet()) {
+                    STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::glpk, "glpk is not selected as the used LP solver, so setting options for glpk has no effect.");
+                }
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GlpkSettings.h b/src/settings/modules/GlpkSettings.h
index c23b2add0..b58e91746 100644
--- a/src/settings/modules/GlpkSettings.h
+++ b/src/settings/modules/GlpkSettings.h
@@ -26,6 +26,13 @@ namespace storm {
                  */
                 bool isOutputSet() const;
                 
+                /*!
+                 * Retrieves whether the integer tolerance has been set.
+                 *
+                 * @return True iff the integer tolerance has been set.
+                 */
+                bool isIntegerToleranceSet() const;
+                
                 /*!
                  * Retrieves the integer tolerance to be used.
                  *
@@ -33,6 +40,8 @@ namespace storm {
                  */
                 double getIntegerTolerance() const;
                 
+                bool check() const override;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp
index c9c8b1840..4b9f27f9e 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.cpp
+++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp
@@ -32,6 +32,10 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
             }
             
+            bool GmmxxEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {
+                return this->getOption(techniqueOptionName).getHasOptionBeenSet();
+            }
+            
             GmmxxEquationSolverSettings::LinearEquationTechnique GmmxxEquationSolverSettings::getLinearEquationSystemTechnique() const {
                 std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
                 if (linearEquationSystemTechniqueAsString == "bicgstab") {
@@ -46,6 +50,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
             }
             
+            bool GmmxxEquationSolverSettings::isPreconditioningTechniqueSet() const {
+                return this->getOption(preconditionOptionName).getHasOptionBeenSet();
+            }
+            
             GmmxxEquationSolverSettings::PreconditioningTechnique GmmxxEquationSolverSettings::getPreconditioningTechnique() const {
                 std::string preconditioningTechniqueAsString = this->getOption(preconditionOptionName).getArgumentByName("name").getValueAsString();
                 if (preconditioningTechniqueAsString == "ilu") {
@@ -58,22 +66,46 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown preconditioning technique '" << preconditioningTechniqueAsString << "' selected.");
             }
             
+            bool GmmxxEquationSolverSettings::isRestartIterationCountSet() const {
+                return this->getOption(restartOptionName).getHasOptionBeenSet();
+            }
+            
             uint_fast64_t GmmxxEquationSolverSettings::getRestartIterationCount() const {
                 return this->getOption(restartOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
             }
             
+            bool GmmxxEquationSolverSettings::isMaximalIterationCountSet() const {
+                return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet();
+            }
+            
             uint_fast64_t GmmxxEquationSolverSettings::getMaximalIterationCount() const {
                 return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
             }
             
+            bool GmmxxEquationSolverSettings::isPrecisionSet() const {
+                return this->getOption(precisionOptionName).getHasOptionBeenSet();
+            }
+            
             double GmmxxEquationSolverSettings::getPrecision() const {
                 return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
             }
             
+            bool GmmxxEquationSolverSettings::isConvergenceCriterionSet() const {
+                return this->getOption(absoluteOptionName).getHasOptionBeenSet();
+            }
+            
             GmmxxEquationSolverSettings::ConvergenceCriterion GmmxxEquationSolverSettings::getConvergenceCriterion() const {
                 return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? GmmxxEquationSolverSettings::ConvergenceCriterion::Absolute : GmmxxEquationSolverSettings::ConvergenceCriterion::Relative;
             }
             
+            bool GmmxxEquationSolverSettings::check() const {
+                bool optionsSet = isLinearEquationSystemTechniqueSet() || isPreconditioningTechniqueSet() || isRestartIterationCountSet() | isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet();
+                
+                STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect.");
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GmmxxEquationSolverSettings.h b/src/settings/modules/GmmxxEquationSolverSettings.h
index 7504f7456..07bc90174 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.h
+++ b/src/settings/modules/GmmxxEquationSolverSettings.h
@@ -28,6 +28,13 @@ namespace storm {
                  */
                 GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
                 
+                /*!
+                 * Retrieves whether the linear equation system technique has been set.
+                 *
+                 * @return True iff the linear equation system technique has been set.
+                 */
+                bool isLinearEquationSystemTechniqueSet() const;
+                
                 /*!
                  * Retrieves the technique that is to be used for solving systems of linear equations.
                  *
@@ -35,6 +42,13 @@ namespace storm {
                  */
                 LinearEquationTechnique getLinearEquationSystemTechnique() const;
                 
+                /*!
+                 * Retrieves whether the preconditioning technique has been set.
+                 *
+                 * @return True iff the preconditioning technique has been set.
+                 */
+                bool isPreconditioningTechniqueSet() const;
+                
                 /*!
                  * Retrieves the technique that is to be used for preconditioning solving systems of linear equations.
                  *
@@ -42,6 +56,13 @@ namespace storm {
                  */
                 PreconditioningTechnique getPreconditioningTechnique() const;
                 
+                /*!
+                 * Retrieves whether the restart iteration count has been set.
+                 *
+                 * @return True iff the restart iteration count has been set.
+                 */
+                bool isRestartIterationCountSet() const;
+                
                 /*!
                  * Retrieves the number of iterations after which restarted techniques are to be restarted.
                  *
@@ -49,6 +70,13 @@ namespace storm {
                  */
                 uint_fast64_t getRestartIterationCount() const;
                 
+                /*!
+                 * Retrieves whether the maximal iteration count has been set.
+                 *
+                 * @return True iff the maximal iteration count has been set.
+                 */
+                bool isMaximalIterationCountSet() const;
+                
                 /*!
                  * Retrieves the maximal number of iterations to perform until giving up on converging.
                  *
@@ -56,6 +84,13 @@ namespace storm {
                  */
                 uint_fast64_t getMaximalIterationCount() const;
                 
+                /*!
+                 * Retrieves whether the precision has been set.
+                 *
+                 * @return True iff the precision has been set.
+                 */
+                bool isPrecisionSet() const;
+                
                 /*!
                  * Retrieves the precision that is used for detecting convergence.
                  *
@@ -63,6 +98,13 @@ namespace storm {
                  */
                 double getPrecision() const;
                 
+                /*!
+                 * Retrieves whether the convergence criterion has been set.
+                 *
+                 * @return True iff the convergence criterion has been set.
+                 */
+                bool isConvergenceCriterionSet() const;
+                
                 /*!
                  * Retrieves the selected convergence criterion.
                  *
@@ -70,6 +112,8 @@ namespace storm {
                  */
                 ConvergenceCriterion getConvergenceCriterion() const;
                 
+                bool check() const override;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp
index 1038fce26..86751cc1d 100644
--- a/src/settings/modules/GurobiSettings.cpp
+++ b/src/settings/modules/GurobiSettings.cpp
@@ -19,10 +19,18 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
             }
             
+            bool GurobiSettings::isIntegerToleranceSet() const {
+                return this->getOption(integerToleranceOption).getHasOptionBeenSet();
+            }
+            
             double GurobiSettings::getIntegerTolerance() const {
                 return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
             }
             
+            bool GurobiSettings::isNumberOfThreadsSet() const {
+                return this->getOption(threadsOption).getHasOptionBeenSet();
+            }
+            
             uint_fast64_t GurobiSettings::getNumberOfThreads() const {
                 return this->getOption(threadsOption).getArgumentByName("count").getValueAsUnsignedInteger();
             }
@@ -31,6 +39,14 @@ namespace storm {
                 return this->getOption(outputOption).getHasOptionBeenSet();
             }
             
+            bool GurobiSettings::check() const {
+                if (isOutputSet() || isIntegerToleranceSet() || isNumberOfThreadsSet()) {
+                    STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::Gurobi, "Gurobi is not selected as the used LP solver, so setting options for Gurobi has no effect.");
+                }
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GurobiSettings.h b/src/settings/modules/GurobiSettings.h
index d0e92127b..ce7fcd78f 100644
--- a/src/settings/modules/GurobiSettings.h
+++ b/src/settings/modules/GurobiSettings.h
@@ -19,6 +19,13 @@ namespace storm {
                  */
                 GurobiSettings(storm::settings::SettingsManager& settingsManager);
                 
+                /*!
+                 * Retrieves whether the integer tolerance has been set.
+                 *
+                 * @return True iff the integer tolerance has been set.
+                 */
+                bool isIntegerToleranceSet() const;
+                
                 /*!
                  * Retrieves the integer tolerance to be used.
                  *
@@ -26,6 +33,13 @@ namespace storm {
                  */
                 double getIntegerTolerance() const;
                 
+                /*!
+                 * Retrieves whether the number of threads has been set.
+                 *
+                 * @return True iff the number of threads has been set.
+                 */
+                bool isNumberOfThreadsSet() const;
+                
                 /*!
                  * Retrieves the maximal number of threads Gurobi is allowed to use.
                  *
@@ -40,6 +54,8 @@ namespace storm {
                  */
                 bool isOutputSet() const;
                 
+                bool check() const override;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp
index b03feece6..76af99b3e 100644
--- a/src/settings/modules/NativeEquationSolverSettings.cpp
+++ b/src/settings/modules/NativeEquationSolverSettings.cpp
@@ -24,6 +24,10 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
             }
             
+            bool NativeEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {
+                return this->getOption(techniqueOptionName).getHasOptionBeenSet();
+            }
+            
             NativeEquationSolverSettings::LinearEquationTechnique NativeEquationSolverSettings::getLinearEquationSystemTechnique() const {
                 std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
                 if (linearEquationSystemTechniqueAsString == "jacobi") {
@@ -32,18 +36,38 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
             }
             
+            bool NativeEquationSolverSettings::isMaximalIterationCountSet() const {
+                return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet();
+            }
+            
             uint_fast64_t NativeEquationSolverSettings::getMaximalIterationCount() const {
                 return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
             }
             
+            bool NativeEquationSolverSettings::isPrecisionSet() const {
+                return this->getOption(precisionOptionName).getHasOptionBeenSet();
+            }
+            
             double NativeEquationSolverSettings::getPrecision() const {
                 return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
             }
             
+            bool NativeEquationSolverSettings::isConvergenceCriterionSet() const {
+                return this->getOption(absoluteOptionName).getHasOptionBeenSet();
+            }
+            
             NativeEquationSolverSettings::ConvergenceCriterion NativeEquationSolverSettings::getConvergenceCriterion() const {
                 return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? NativeEquationSolverSettings::ConvergenceCriterion::Absolute : NativeEquationSolverSettings::ConvergenceCriterion::Relative;
             }
             
+            bool NativeEquationSolverSettings::check() const {
+                bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet();
+                
+                STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Native || !optionSet, "Native is not selected as the equation solver, so setting options for native has no effect.");
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/NativeEquationSolverSettings.h b/src/settings/modules/NativeEquationSolverSettings.h
index 826d40941..9d6e43ecd 100644
--- a/src/settings/modules/NativeEquationSolverSettings.h
+++ b/src/settings/modules/NativeEquationSolverSettings.h
@@ -25,6 +25,13 @@ namespace storm {
                  */
                 NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
                 
+                /*!
+                 * Retrieves whether the linear equation system technique has been set.
+                 *
+                 * @return True iff the linear equation system technique has been set.
+                 */
+                bool isLinearEquationSystemTechniqueSet() const;
+                
                 /*!
                  * Retrieves the technique that is to be used for solving systems of linear equations.
                  *
@@ -32,6 +39,13 @@ namespace storm {
                  */
                 LinearEquationTechnique getLinearEquationSystemTechnique() const;
                 
+                /*!
+                 * Retrieves whether the maximal iteration count has been set.
+                 *
+                 * @return True iff the maximal iteration count has been set.
+                 */
+                bool isMaximalIterationCountSet() const;
+                
                 /*!
                  * Retrieves the maximal number of iterations to perform until giving up on converging.
                  *
@@ -39,6 +53,13 @@ namespace storm {
                  */
                 uint_fast64_t getMaximalIterationCount() const;
                 
+                /*!
+                 * Retrieves whether the precision has been set.
+                 *
+                 * @return True iff the precision has been set.
+                 */
+                bool isPrecisionSet() const;
+                
                 /*!
                  * Retrieves the precision that is used for detecting convergence.
                  *
@@ -46,6 +67,13 @@ namespace storm {
                  */
                 double getPrecision() const;
                 
+                /*!
+                 * Retrieves whether the convergence criterion has been set.
+                 *
+                 * @return True iff the convergence criterion has been set.
+                 */
+                bool isConvergenceCriterionSet() const;
+                
                 /*!
                  * Retrieves the selected convergence criterion.
                  *
@@ -53,6 +81,8 @@ namespace storm {
                  */
                 ConvergenceCriterion getConvergenceCriterion() const;
                 
+                bool check() const override;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
diff --git a/src/utility/cli.h b/src/utility/cli.h
index b428ef4aa..d0110e67f 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -259,7 +259,7 @@ namespace storm {
             }
             
             void generateCounterexample(std::shared_ptr<storm::models::AbstractModel<double>> model, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>> const& formula) {
-                if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandGenerationSet()) {
+                if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
                     STORM_LOG_THROW(model->getType() == storm::models::MDP, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
                     STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
                     
diff --git a/src/utility/macros.h b/src/utility/macros.h
index 511fdcc12..795f16e96 100644
--- a/src/utility/macros.h
+++ b/src/utility/macros.h
@@ -44,14 +44,48 @@ extern log4cplus::Logger logger;
     LOG4CPLUS_WARN(logger, message);            \
 } while (false)
 
+#define STORM_LOG_WARN_COND(cond, message)      \
+{                                               \
+    if (!(cond)) {                              \
+        LOG4CPLUS_WARN(logger, message);        \
+    }                                           \
+} while (false)
+
 #define STORM_LOG_INFO(message)                 \
 {                                               \
     LOG4CPLUS_INFO(logger, message);            \
 } while (false)
 
+#define STORM_LOG_INFO_COND(cond, message)      \
+{                                               \
+    if (!(cond)) {                              \
+        LOG4CPLUS_INFO(logger, message);        \
+    }                                           \
+} while (false)
+
 #define STORM_LOG_ERROR(message)                \
 {                                               \
     LOG4CPLUS_ERROR(logger, message);           \
 } while (false)
 
+#define STORM_LOG_ERROR_COND(cond, message)     \
+{                                               \
+    if (!(cond)) {                              \
+        LOG4CPLUS_ERROR(logger, message);       \
+    }                                           \
+} while (false)
+
+/*!
+ * Define the macros that print information and optionally also log it.
+ */
+#define STORM_PRINT(message)                    \
+{                                               \
+    STORM_LOG_INFO(message);                    \
+}
+
+#define STORM_PRINT_AND_LOG(message)            \
+{                                               \
+    STORM_PRINT(message);                       \
+}
+
 #endif /* STORM_UTILITY_MACROS_H_ */
\ No newline at end of file

From 0a0485c8f01ce56264f0a8a7acfed7f4b3c5319d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 1 Oct 2014 18:34:40 +0200
Subject: [PATCH 2/3] Added the functionality to specify and parse a
 configuration file to set command line options.

Former-commit-id: 3488b527f7c7ee3c64e92efbbe7a4082f1ec3841
---
 src/settings/SettingsManager.cpp | 148 +++++++++++++++++++++++++++----
 src/settings/SettingsManager.h   |  18 ++++
 src/utility/cli.h                |   3 +-
 3 files changed, 150 insertions(+), 19 deletions(-)

diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index 53d31f6f0..a9eac4a9a 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -110,9 +110,30 @@ namespace storm {
             if (optionActive) {
                 setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache);
             }
-            
-            // Finally check whether all modules are okay with the current settings.
-            this->checkAllModules();
+
+            if (storm::settings::generalSettings().isConfigSet()) {
+                std::map<std::string, std::vector<std::string>> configurationFileSettings = parseConfigFile(storm::settings::generalSettings().getConfigFilename());
+                
+                for (auto const& optionArgumentsPair : configurationFileSettings) {
+                    auto options = this->longNameToOptions.find(optionArgumentsPair.first);
+                    
+                    // We don't need to check whether this option exists or not, because this is already checked when
+                    // parsing the configuration file.
+                    
+                    // Now go through all the matching options and set them according to the values.
+                    for (auto option : options->second) {
+                        if (option->getHasOptionBeenSet()) {
+                            // If the option was already set from the command line, we issue a warning and ignore the
+                            // settings from the configuration file.
+                            STORM_LOG_WARN("The option '" << option->getLongName() << " of module '" << option->getModuleName() << "' has been set in the configuration file, but was overriden on the command line.");
+                        } else {
+                            // If, however, the option has not been set yet, we try to assign values ot its arguments
+                            // based on the argument strings.
+                            setOptionArguments(optionArgumentsPair.first, option, optionArgumentsPair.second);
+                        }
+                    }
+                }
+            }
         }
         
         void SettingsManager::setFromConfigurationFile(std::string const& configFilename) {
@@ -293,6 +314,23 @@ namespace storm {
             return true;
         }
         
+        void SettingsManager::setOptionArguments(std::string const& optionName, std::shared_ptr<Option> option, std::vector<std::string> const& argumentCache) {
+            STORM_LOG_THROW(argumentCache.size() <= option->getArgumentCount(), storm::exceptions::OptionParserException, "Too many arguments for option '" << optionName << "'.");
+            
+            // Now set the provided argument values one by one.
+            for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) {
+                ArgumentBase& argument = option->getArgument(i);
+                bool conversionOk = argument.setFromStringValue(argumentCache[i]);
+                STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Conversion of value of argument '" << argument.getName() << "' to its type failed.");
+            }
+            
+            // In case there are optional arguments that were not set, we set them to their default value.
+            for (uint_fast64_t i = argumentCache.size(); i < option->getArgumentCount(); ++i) {
+                ArgumentBase& argument = option->getArgument(i);
+                argument.setFromDefaultValue();
+            }
+        }
+        
         void SettingsManager::setOptionsArguments(std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache) {
             auto optionIterator = optionMap.find(optionName);
             STORM_LOG_THROW(optionIterator != optionMap.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");
@@ -300,20 +338,7 @@ namespace storm {
             // Iterate over all options and set the arguments.
             for (auto& option : optionIterator->second) {
                 option->setHasOptionBeenSet();
-                STORM_LOG_THROW(argumentCache.size() <= option->getArgumentCount(), storm::exceptions::OptionParserException, "Too many arguments for option '" << optionName << "'.");
-                
-                // Now set the provided argument values one by one.
-                for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) {
-                    ArgumentBase& argument = option->getArgument(i);
-                    bool conversionOk = argument.setFromStringValue(argumentCache[i]);
-                    STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Conversion of value of argument '" << argument.getName() << "' to its type failed.");
-                }
-                
-                // In case there are optional arguments that were not set, we set them to their default value.
-                for (uint_fast64_t i = argumentCache.size(); i < option->getArgumentCount(); ++i) {
-                    ArgumentBase& argument = option->getArgument(i);
-                    argument.setFromDefaultValue();
-                }
+                setOptionArguments(optionName, option, argumentCache);
             }
         }
         
@@ -334,6 +359,95 @@ namespace storm {
             }
         }
         
+        std::map<std::string, std::vector<std::string>> SettingsManager::parseConfigFile(std::string const& filename) const {
+            std::map<std::string, std::vector<std::string>> result;
+            
+            std::ifstream input(filename);
+            STORM_LOG_THROW(input.good(), storm::exceptions::OptionParserException, "Could not read from config file '" << filename << "'.");
+
+            bool globalScope = true;
+            std::string activeModule = "";
+            uint_fast64_t lineNumber = 1;
+            for (std::string line; getline(input, line); ++lineNumber) {
+                // If the first character of the line is a "[", we expect the settings of a new module to start and
+                // the line to be of the shape [<module>].
+                if (line.at(0) == '[') {
+                    STORM_LOG_THROW(line.at(0) == '[' && line.find("]") == line.length() - 1 && line.find("[", 1) == line.npos, storm::exceptions::OptionParserException, "Illegal module name header in configuration file '" << filename << " in line " << std::to_string(lineNumber) << ". Expected [<module>] where <module> is a placeholder for a known module.");
+                    
+                    // Extract the module name and check whether it's a legal one.
+                    std::string moduleName = line.substr(1, line.length() - 2);
+                    STORM_LOG_THROW(moduleName != "" && (moduleName == "global" || (this->modules.find(moduleName) != this->modules.end())), storm::exceptions::OptionParserException, "Module header in configuration file '" << filename << " in line " << std::to_string(lineNumber) << " refers to unknown module '" << moduleName << ".");
+                    
+                    // If the module name is "global", we unset the currently active module and treat all options to follow as unprefixed.
+                    if (moduleName == "global") {
+                        globalScope = true;
+                    } else {
+                        activeModule = moduleName;
+                        globalScope = false;
+                    }
+                } else {
+                    // In this case, we expect the line to be of the shape o or o=a b c, where o is an option and a, b
+                    // and c are the values that are supposed to be assigned to the arguments of the option.
+                    std::size_t assignmentSignIndex = line.find("=");
+                    bool containsAssignment = false;
+                    if (assignmentSignIndex != line.npos) {
+                        containsAssignment = true;
+                    }
+                    
+                    std::string optionName;
+                    if (containsAssignment) {
+                        optionName = line.substr(0, assignmentSignIndex);
+                    } else {
+                        optionName = line;
+                    }
+                    
+                    if (globalScope) {
+                        STORM_LOG_THROW(this->longNameToOptions.find(optionName) != this->longNameToOptions.end(), storm::exceptions::OptionParserException, "Option assignment in configuration file '" << filename << " in line " << lineNumber << " refers to unknown option '" << optionName << "'.");
+                    } else {
+                        STORM_LOG_THROW(this->longNameToOptions.find(activeModule + ":" + optionName) != this->longNameToOptions.end(), storm::exceptions::OptionParserException, "Option assignment in configuration file '" << filename << " in line " << lineNumber << " refers to unknown option '" << activeModule << ":" <<  optionName << "'.");
+                    }
+                    
+                    // If the current line is an assignment, split the right-hand side of the assignment into parts
+                    // enclosed by quotation marks.
+                    if (containsAssignment) {
+                        std::string assignedValues = line.substr(assignmentSignIndex + 1);
+                        std::vector<std::string> argumentCache;
+                    
+                        // As horrible as it may look, this regular expression matches either a quoted string (possibly
+                        // containing escaped quotes) or a simple word (without whitespaces and quotes).
+                        std::regex argumentRegex("\"(([^\\\\\"]|((\\\\\\\\)*\\\\\")|\\\\[^\"])*)\"|(([^ \\\\\"]|((\\\\\\\\)*\\\\\")|\\\\[^\"])+)");
+                        boost::algorithm::trim_left(assignedValues);
+                        
+                        while (!assignedValues.empty()) {
+                            std::smatch match;
+                            bool hasMatch = std::regex_search(assignedValues, match, argumentRegex);
+                            
+                            // If the input could not be matched, we have a parsing error.
+                            STORM_LOG_THROW(hasMatch, storm::exceptions::OptionParserException, "Parsing error in configuration file '" << filename << "' in line " << lineNumber << ". Unexpected input '" << assignedValues << "'.");
+
+                            // Extract the matched argument and cut off the quotation marks if necessary.
+                            std::string matchedArgument = std::string(match[0].first, match[0].second);
+                            if (matchedArgument.at(0) == '"') {
+                                matchedArgument = matchedArgument.substr(1, matchedArgument.length() - 2);
+                            }
+                            argumentCache.push_back(matchedArgument);
+                            
+                            assignedValues = assignedValues.substr(match.length());
+                            boost::algorithm::trim_left(assignedValues);
+                        }
+                        
+                        // After successfully parsing the argument values, we store them in the result map.
+                        result.emplace((!globalScope ? activeModule + ":" : "") + optionName, argumentCache);
+                    } else {
+                        // In this case, we can just insert the option to indicate it should be set (without arguments).
+                        result.emplace((!globalScope ? activeModule + ":" : "") + optionName, std::vector<std::string>());
+                    }
+                }
+            }
+            
+            return result;
+        }
+        
         SettingsManager const& manager() {
             return SettingsManager::manager();
         }
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index 1c77e1d56..41383f336 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -8,6 +8,7 @@
 #include <utility>
 #include <functional>
 #include <unordered_map>
+#include <map>
 #include <vector>
 #include <memory>
 
@@ -156,6 +157,15 @@ namespace storm {
              */
             void addOption(std::shared_ptr<Option> const& option);
             
+            /*!
+             * Sets the arguments of the given option from the provided strings.
+             *
+             * @param optionName The name of the option. This is only used for error output.
+             * @param option The option for which to set the arguments.
+             * @param argumentCache The arguments of the option as string values.
+             */
+            static void setOptionArguments(std::string const& optionName, std::shared_ptr<Option> option, std::vector<std::string> const& argumentCache);
+            
             /*!
              * Sets the arguments of the options matching the given name from the provided strings.
              *
@@ -198,6 +208,14 @@ namespace storm {
              * @return The length of the longest option name.
              */
             uint_fast64_t getPrintLengthOfLongestOption(std::string const& moduleName) const;
+            
+            /*!
+             * Parses the given file and stores the settings in the returned map.
+             *
+             * @param filename The name of the file that is to be scanned for settings.
+             * @return A mapping of option names to the argument values (represented as strings).
+             */
+            std::map<std::string, std::vector<std::string>> parseConfigFile(std::string const& filename) const;
         };
         
         /*!
diff --git a/src/utility/cli.h b/src/utility/cli.h
index d0110e67f..4ceb64a95 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -199,9 +199,8 @@ namespace storm {
                 try {
                     manager.setFromCommandLine(argc, argv);
                 } catch (storm::exceptions::OptionParserException& e) {
-                    std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
-                    std::cout << std::endl;
                     manager.printHelp();
+                    throw e;
                     return false;
                 }
                 

From 428518ee12ddd4aa4dd6e50401de5c6e976d156f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 1 Oct 2014 21:06:21 +0200
Subject: [PATCH 3/3] Added some error checking to configuration file parsing.

Former-commit-id: 48920feeddbbf0630ae26542a4706a30ca1744c4
---
 src/settings/SettingsManager.cpp | 79 +++++++++++++++++---------------
 src/utility/macros.h             |  3 +-
 2 files changed, 44 insertions(+), 38 deletions(-)

diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index a9eac4a9a..26fb6070d 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -111,37 +111,41 @@ namespace storm {
                 setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache);
             }
 
+            // Include the options from a possibly specified configuration file, but don't overwrite existing settings.
             if (storm::settings::generalSettings().isConfigSet()) {
-                std::map<std::string, std::vector<std::string>> configurationFileSettings = parseConfigFile(storm::settings::generalSettings().getConfigFilename());
-                
-                for (auto const& optionArgumentsPair : configurationFileSettings) {
-                    auto options = this->longNameToOptions.find(optionArgumentsPair.first);
-                    
-                    // We don't need to check whether this option exists or not, because this is already checked when
-                    // parsing the configuration file.
-                    
-                    // Now go through all the matching options and set them according to the values.
-                    for (auto option : options->second) {
-                        if (option->getHasOptionBeenSet()) {
-                            // If the option was already set from the command line, we issue a warning and ignore the
-                            // settings from the configuration file.
-                            STORM_LOG_WARN("The option '" << option->getLongName() << " of module '" << option->getModuleName() << "' has been set in the configuration file, but was overriden on the command line.");
-                        } else {
-                            // If, however, the option has not been set yet, we try to assign values ot its arguments
-                            // based on the argument strings.
-                            setOptionArguments(optionArgumentsPair.first, option, optionArgumentsPair.second);
-                        }
-                    }
-                }
+                this->setFromConfigurationFile(storm::settings::generalSettings().getConfigFilename());
             }
+            
+            // Finally, check whether all modules are okay with the current settings.
+            this->checkAllModules();
         }
         
         void SettingsManager::setFromConfigurationFile(std::string const& configFilename) {
-            STORM_LOG_ASSERT(false, "Not yet implemented.");
+            std::map<std::string, std::vector<std::string>> configurationFileSettings = parseConfigFile(configFilename);
+            
+            for (auto const& optionArgumentsPair : configurationFileSettings) {
+                auto options = this->longNameToOptions.find(optionArgumentsPair.first);
+                
+                // We don't need to check whether this option exists or not, because this is already checked when
+                // parsing the configuration file.
+                
+                // Now go through all the matching options and set them according to the values.
+                for (auto option : options->second) {
+                    if (option->getHasOptionBeenSet()) {
+                        // If the option was already set from the command line, we issue a warning and ignore the
+                        // settings from the configuration file.
+                        STORM_LOG_WARN("The option '" << option->getLongName() << "' of module '" << option->getModuleName() << "' has been set in the configuration file '" << configFilename << "', but was overwritten on the command line." << std::endl);
+                    } else {
+                        // If, however, the option has not been set yet, we try to assign values ot its arguments
+                        // based on the argument strings.
+                        setOptionArguments(optionArgumentsPair.first, option, optionArgumentsPair.second);
+                    }
+                }
+            }
         }
         
         void SettingsManager::printHelp(std::string const& hint) const {
-            std::cout << "usage: storm [options]" << std::endl << std::endl;
+            STORM_PRINT("usage: storm [options]" << std::endl << std::endl);
             
             if (hint == "all") {
                 // Find longest option name.
@@ -190,7 +194,7 @@ namespace storm {
                 // Print the matching modules.
                 uint_fast64_t maxLength = std::max(maxLengthModules, maxLengthOptions);
                 if (matchingModuleNames.size() > 0) {
-                    std::cout << "Matching modules for hint '" << hint << "':" << std::endl;
+                    STORM_PRINT("Matching modules for hint '" << hint << "':" << std::endl)
                     for (auto const& matchingModuleName : matchingModuleNames) {
                         printHelpForModule(matchingModuleName, maxLength);
                     }
@@ -198,14 +202,14 @@ namespace storm {
                 
                 // Print the matching options.
                 if (matchingOptions.size() > 0) {
-                    std::cout << "Matching options for hint '" << hint << "':" << std::endl;
+                    STORM_PRINT("Matching options for hint '" << hint << "':" << std::endl);
                     for (auto const& option : matchingOptions) {
-                        std::cout << std::setw(maxLength) << std::left << *option << std::endl;
+                        STORM_PRINT(std::setw(maxLength) << std::left << *option << std::endl);
                     }
                 }
                 
                 if (matchingModuleNames.empty() && matchingOptions.empty()) {
-                    std::cout << "Hint '" << hint << "' did not match any modules or options." << std::endl;
+                    STORM_PRINT("Hint '" << hint << "' did not match any modules or options." << std::endl);
                 }
             }
         }
@@ -213,20 +217,16 @@ namespace storm {
         void SettingsManager::printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength) const {
             auto moduleIterator = moduleOptions.find(moduleName);
             STORM_LOG_THROW(moduleIterator != moduleOptions.end(), storm::exceptions::IllegalFunctionCallException, "Cannot print help for unknown module '" << moduleName << "'.");
-            std::cout << "##### Module '" << moduleName << "' ";
-            for (uint_fast64_t i = 0; i < std::min(maxLength, maxLength - moduleName.length() - 16); ++i) {
-                std::cout << "#";
-            }
-            std::cout << std::endl;
+            STORM_PRINT("##### Module '" << moduleName << "' " << std::string(std::min(maxLength, maxLength - moduleName.length() - 16), '#') << std::endl);
             
             // Save the flags for std::cout so we can manipulate them and be sure they will be restored as soon as this
             // stream goes out of scope.
             boost::io::ios_flags_saver out(std::cout);
             
             for (auto const& option : moduleIterator->second) {
-                std::cout << std::setw(maxLength) << std::left << *option << std::endl;
+                STORM_PRINT(std::setw(maxLength) << std::left << *option << std::endl);
             }
-            std::cout << std::endl;
+            STORM_PRINT(std::endl);
         }
         
         uint_fast64_t SettingsManager::getPrintLengthOfLongestOption() const {
@@ -329,6 +329,8 @@ namespace storm {
                 ArgumentBase& argument = option->getArgument(i);
                 argument.setFromDefaultValue();
             }
+            
+            option->setHasOptionBeenSet();
         }
         
         void SettingsManager::setOptionsArguments(std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache) {
@@ -337,7 +339,6 @@ namespace storm {
             
             // Iterate over all options and set the arguments.
             for (auto& option : optionIterator->second) {
-                option->setHasOptionBeenSet();
                 setOptionArguments(optionName, option, argumentCache);
             }
         }
@@ -407,6 +408,9 @@ namespace storm {
                         STORM_LOG_THROW(this->longNameToOptions.find(activeModule + ":" + optionName) != this->longNameToOptions.end(), storm::exceptions::OptionParserException, "Option assignment in configuration file '" << filename << " in line " << lineNumber << " refers to unknown option '" << activeModule << ":" <<  optionName << "'.");
                     }
                     
+                    std::string fullOptionName = (!globalScope ? activeModule + ":" : "") + optionName;
+                    STORM_LOG_WARN_COND(result.find(fullOptionName) == result.end(), "Option '" << fullOptionName << "' is set in line " << lineNumber << " of configuration file " << filename << ", but has been set before.");
+                    
                     // If the current line is an assignment, split the right-hand side of the assignment into parts
                     // enclosed by quotation marks.
                     if (containsAssignment) {
@@ -436,11 +440,12 @@ namespace storm {
                             boost::algorithm::trim_left(assignedValues);
                         }
                         
+                        
                         // After successfully parsing the argument values, we store them in the result map.
-                        result.emplace((!globalScope ? activeModule + ":" : "") + optionName, argumentCache);
+                        result.emplace(fullOptionName, argumentCache);
                     } else {
                         // In this case, we can just insert the option to indicate it should be set (without arguments).
-                        result.emplace((!globalScope ? activeModule + ":" : "") + optionName, std::vector<std::string>());
+                        result.emplace(fullOptionName, std::vector<std::string>());
                     }
                 }
             }
diff --git a/src/utility/macros.h b/src/utility/macros.h
index 795f16e96..a8d75d3c8 100644
--- a/src/utility/macros.h
+++ b/src/utility/macros.h
@@ -80,11 +80,12 @@ extern log4cplus::Logger logger;
  */
 #define STORM_PRINT(message)                    \
 {                                               \
-    STORM_LOG_INFO(message);                    \
+    std::cout << message;                       \
 }
 
 #define STORM_PRINT_AND_LOG(message)            \
 {                                               \
+    STORM_LOG_INFO(message);                    \
     STORM_PRINT(message);                       \
 }