From f85d28325ef4157f113f539d4c69ef538c0541d5 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Fri, 14 Aug 2015 18:34:03 +0200
Subject: [PATCH] Further work towards faster and more modular compilation

Former-commit-id: 9de50910b87917cff17121f01c847203fbf6844b
---
 src/builder/DdPrismModelBuilder.cpp           |   2 +
 src/builder/ExplicitPrismModelBuilder.cpp     |   2 +
 src/models/sparse/DeterministicModel.cpp      |   2 +-
 src/models/sparse/Dtmc.cpp                    |   2 +
 src/models/sparse/Dtmc.h                      |   3 +
 src/models/sparse/MarkovAutomaton.cpp         |   2 +
 src/models/sparse/Mdp.cpp                     |   2 +
 .../DeterministicSparseTransitionParser.cpp   |   1 +
 ...NondeterministicSparseTransitionParser.cpp |   2 +
 src/settings/Argument.cpp                     | 158 ++++++++++++++++++
 src/storage/Decomposition.cpp                 |   1 +
 src/storage/SparseMatrix.h                    |   8 +-
 .../StronglyConnectedComponentDecomposition.h |   1 +
 src/utility/constants.cpp                     |   2 +
 src/utility/constants.h                       |   1 -
 src/utility/numerical.h                       |   1 +
 src/utility/prism.cpp                         |   2 +
 src/utility/prism.h                           |   2 -
 .../parser/DeterministicModelParserTest.cpp   |   4 +
 ...eterministicSparseTransitionParserTest.cpp |   2 +
 .../parser/MarkovAutomatonParserTest.cpp      |   1 +
 .../NondeterministicModelParserTest.cpp       |   3 +
 ...eterministicSparseTransitionParserTest.cpp |   2 +
 test/functional/storage/SparseMatrixTest.cpp  |   1 +
 24 files changed, 198 insertions(+), 9 deletions(-)
 create mode 100644 src/settings/Argument.cpp

diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 48ffa7344..c2c73e01f 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -10,6 +10,8 @@
 
 #include "src/exceptions/InvalidStateException.h"
 
+#include "src/exceptions/InvalidArgumentException.h"
+
 #include "src/utility/prism.h"
 #include "src/utility/math.h"
 #include "src/storage/prism/Program.h"
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index ab034238c..67ecacb09 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -14,6 +14,8 @@
 #include "src/utility/macros.h"
 #include "src/exceptions/WrongFormatException.h"
 
+#include "src/exceptions/InvalidArgumentException.h"
+
 namespace storm {
     namespace builder {
         template <typename ValueType, typename IndexType>
diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp
index 68d18ba77..d4a0e25b0 100644
--- a/src/models/sparse/DeterministicModel.cpp
+++ b/src/models/sparse/DeterministicModel.cpp
@@ -1,5 +1,5 @@
 #include "src/models/sparse/DeterministicModel.h"
-
+#include "src/utility/constants.h"
 #include "src/adapters/CarlAdapter.h"
 
 namespace storm {
diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp
index b5dbaa40c..70ed59a72 100644
--- a/src/models/sparse/Dtmc.cpp
+++ b/src/models/sparse/Dtmc.cpp
@@ -2,6 +2,8 @@
 
 #include "src/adapters/CarlAdapter.h"
 #include "src/exceptions/NotImplementedException.h"
+#include "src/exceptions/InvalidArgumentException.h"
+#include "src/utility/constants.h"
 
 namespace storm {
     namespace models {
diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h
index 0bf0cfce1..aacf4379d 100644
--- a/src/models/sparse/Dtmc.h
+++ b/src/models/sparse/Dtmc.h
@@ -1,8 +1,11 @@
 #ifndef STORM_MODELS_SPARSE_DTMC_H_
 #define STORM_MODELS_SPARSE_DTMC_H_
+#include <unordered_set>
 
 #include "src/models/sparse/DeterministicModel.h"
 #include "src/utility/OsDetection.h"
+#include "src/utility/constants.h"
+#include "src/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace models {
diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp
index d161a64f6..83d099f69 100644
--- a/src/models/sparse/MarkovAutomaton.cpp
+++ b/src/models/sparse/MarkovAutomaton.cpp
@@ -1,5 +1,7 @@
 #include "src/models/sparse/MarkovAutomaton.h"
 
+#include "src/exceptions/InvalidArgumentException.h"
+#include "src/utility/constants.h"
 #include "src/adapters/CarlAdapter.h"
 
 namespace storm {
diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp
index 469dfe54e..46b413228 100644
--- a/src/models/sparse/Mdp.cpp
+++ b/src/models/sparse/Mdp.cpp
@@ -1,5 +1,7 @@
 #include "src/models/sparse/Mdp.h"
 
+#include "src/exceptions/InvalidArgumentException.h"
+#include "src/utility/constants.h"
 #include "src/adapters/CarlAdapter.h"
 
 namespace storm {
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index e7aa4f348..e66c8e208 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -19,6 +19,7 @@
 #include "src/parser/MappedFile.h"
 #include "src/exceptions/FileIoException.h"
 #include "src/exceptions/WrongFormatException.h"
+#include "src/exceptions/InvalidArgumentException.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GeneralSettings.h"
 
diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp
index af8754e89..1388e3ae4 100644
--- a/src/parser/NondeterministicSparseTransitionParser.cpp
+++ b/src/parser/NondeterministicSparseTransitionParser.cpp
@@ -14,6 +14,8 @@
 #include "src/settings/modules/GeneralSettings.h"
 #include "src/exceptions/FileIoException.h"
 #include "src/exceptions/OutOfRangeException.h"
+
+#include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/WrongFormatException.h"
 
 #include "src/utility/cstring.h"
diff --git a/src/settings/Argument.cpp b/src/settings/Argument.cpp
new file mode 100644
index 000000000..f2c3478db
--- /dev/null
+++ b/src/settings/Argument.cpp
@@ -0,0 +1,158 @@
+
+#include "Argument.h"
+
+#include "src/exceptions/IllegalArgumentException.h"
+#include "src/exceptions/IllegalArgumentValueException.h"
+#include "src/exceptions/IllegalFunctionCallException.h"
+#include "src/settings/ArgumentTypeInferationHelper.h"
+#include "src/utility/macros.h"
+
+
+namespace storm {
+	namespace settings {
+      
+        template<typename T>
+			Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(false), defaultValue(), hasDefaultValue(false) {
+                // Intentionally left empty.
+			}
+            
+           template<typename T>
+            Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(), hasDefaultValue(true) {
+                this->setDefaultValue(defaultValue);
+            }
+            
+           template<typename T>
+		    bool Argument<T>::getIsOptional() const  {
+                return this->isOptional;
+            }
+            
+			template<typename T>
+            bool Argument<T>::setFromStringValue(std::string const& fromStringValue)  {
+				bool conversionOk = false;
+				T newValue = ArgumentBase::convertFromString<T>(fromStringValue, conversionOk);
+				if (!conversionOk) {
+                    return false;
+				}
+				return this->setFromTypeValue(newValue);
+			}
+            
+			template<typename T>
+            bool Argument<T>::setFromTypeValue(T const& newValue, bool hasBeenSet) {
+				if (!this->validate(newValue)) {
+                    return false;
+				}
+				this->argumentValue = newValue;
+				this->hasBeenSet = hasBeenSet;
+				return true;
+			}
+            
+			template<typename T>
+            ArgumentType Argument<T>::getType() const  {
+				return this->argumentType;
+			}
+            
+          
+			        
+			template<typename T>
+            T const& Argument<T>::getArgumentValue() const {
+                STORM_LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument '" << this->getName() << "', because it was neither set nor specifies a default value.");
+                if (this->getHasBeenSet()) {
+                    return this->argumentValue;
+                } else {
+                    return this->defaultValue;
+                }
+			}
+            
+			template<typename T>
+            bool Argument<T>::getHasDefaultValue() const  {
+				return this->hasDefaultValue;
+			}
+            
+			template<typename T>
+            void Argument<T>::setFromDefaultValue()  {
+                STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument has none.");
+				bool result = this->setFromTypeValue(this->defaultValue, false);
+                STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument, because it was rejected.");
+			}
+            
+			template<typename T>
+            std::string Argument<T>::getValueAsString() const  {
+				switch (this->argumentType) {
+					case ArgumentType::String:
+						return inferToString(ArgumentType::String, this->getArgumentValue());
+					case ArgumentType::Boolean: {
+						bool iValue = inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
+						if (iValue) {
+							return "true";
+						} else {
+							return "false";
+						}
+					}
+					default: return ArgumentBase::convertToString(this->argumentValue);
+				}
+			}
+			
+			template<typename T>
+            int_fast64_t Argument<T>::getValueAsInteger() const  {
+				switch (this->argumentType) {
+					case ArgumentType::Integer:
+						return inferToInteger(ArgumentType::Integer, this->getArgumentValue());
+					default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as integer."); break;
+                }
+            }
+            
+            
+            template<typename T>
+            uint_fast64_t Argument<T>::getValueAsUnsignedInteger() const  {
+                switch (this->argumentType) {
+                    case ArgumentType::UnsignedInteger:
+                        return inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue());
+                    default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as unsigned integer."); break;
+                }
+            }
+            
+            
+            template<typename T>
+            double Argument<T>::getValueAsDouble() const  {
+                switch (this->argumentType) {
+                    case ArgumentType::Double:
+                        return inferToDouble(ArgumentType::Double, this->getArgumentValue());
+                    default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as double."); break;
+                }
+            }
+            
+            template<typename T>
+            bool Argument<T>::getValueAsBoolean() const  {
+                switch (this->argumentType) {
+                    case ArgumentType::Boolean:
+                        return inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
+                    default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as boolean."); break;
+                }
+            }
+    
+           
+            template<typename T>
+            void Argument<T>::setDefaultValue(T const& newDefault) {
+                STORM_LOG_THROW(this->validate(newDefault), storm::exceptions::IllegalArgumentValueException, "The default value for the argument did not pass all validation functions.");
+                this->defaultValue = newDefault;
+                this->hasDefaultValue = true;
+            }
+                        
+            
+            template<typename T>
+            bool Argument<T>::validate(T const& value) const {
+                bool result = true;
+                for (auto const& lambda : validationFunctions) {
+                    result = result && lambda(value);
+                }
+                return result;
+            }
+            
+            template class Argument<std::string>;
+            template class Argument<int_fast64_t>;
+            template class Argument<uint_fast64_t>;
+            template class Argument<double>;
+            template class Argument<bool>;
+    }
+}
+        
\ No newline at end of file
diff --git a/src/storage/Decomposition.cpp b/src/storage/Decomposition.cpp
index 884b77a4e..4e2ebcb02 100644
--- a/src/storage/Decomposition.cpp
+++ b/src/storage/Decomposition.cpp
@@ -4,6 +4,7 @@
 
 #include "src/storage/StronglyConnectedComponent.h"
 #include "src/storage/MaximalEndComponent.h"
+#include "src/utility/constants.h"
 
 namespace storm {
     namespace storage {
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 555cd379c..730b192ff 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -6,13 +6,8 @@
 #include <cstdint>
 #include <iterator>
 
-#include "src/storage/BitVector.h"
-#include "src/utility/constants.h"
 #include "src/utility/OsDetection.h"
 
-#include "src/exceptions/InvalidArgumentException.h"
-#include "src/exceptions/OutOfRangeException.h"
-
 #include <boost/functional/hash.hpp>
 
 // Forward declaration for adapter classes.
@@ -26,11 +21,14 @@ namespace storm {
 		template<typename T>
 		class TopologicalValueIterationMinMaxLinearEquationSolver;
 	}
+        
+        
 }
 
 namespace storm {
     namespace storage {
         
+        class BitVector;
         // Forward declare matrix class.
         template<typename T> class SparseMatrix;
         
diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h
index 3d2897b70..b909dc43a 100644
--- a/src/storage/StronglyConnectedComponentDecomposition.h
+++ b/src/storage/StronglyConnectedComponentDecomposition.h
@@ -5,6 +5,7 @@
 #include "src/storage/Decomposition.h"
 #include "src/storage/StronglyConnectedComponent.h"
 #include "src/storage/BitVector.h"
+#include "src/utility/constants.h"
 
 namespace storm {
     namespace models {
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 8b518413c..5b5a68348 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -5,6 +5,8 @@
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GeneralSettings.h"
 
+#include "src/adapters/CarlAdapter.h"
+
 namespace storm {
     namespace utility {
         
diff --git a/src/utility/constants.h b/src/utility/constants.h
index 82994f16f..2e5206711 100644
--- a/src/utility/constants.h
+++ b/src/utility/constants.h
@@ -12,7 +12,6 @@
 #include <limits>
 #include <cstdint>
 
-#include "src/adapters/CarlAdapter.h"
 
 namespace storm {
     
diff --git a/src/utility/numerical.h b/src/utility/numerical.h
index baf8bd1a2..f7b0fd40b 100644
--- a/src/utility/numerical.h
+++ b/src/utility/numerical.h
@@ -5,6 +5,7 @@
 #include "src/utility/macros.h"
 #include "src/utility/constants.h"
 #include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/OutOfRangeException.h"
 
 namespace storm {
     namespace utility {
diff --git a/src/utility/prism.cpp b/src/utility/prism.cpp
index b392616fe..5901d3434 100644
--- a/src/utility/prism.cpp
+++ b/src/utility/prism.cpp
@@ -2,6 +2,8 @@
 #include "src/storage/expressions/ExpressionManager.h"
 #include "src/storage/prism/Program.h"
 
+#include "src/exceptions/InvalidArgumentException.h"
+#include "macros.h"
 
 namespace storm {
     namespace utility {
diff --git a/src/utility/prism.h b/src/utility/prism.h
index 87365e38d..c1c13347d 100644
--- a/src/utility/prism.h
+++ b/src/utility/prism.h
@@ -7,8 +7,6 @@
 #include <boost/container/flat_set.hpp>
 
 #include "src/utility/OsDetection.h"
-#include "src/utility/macros.h"
-#include "src/exceptions/InvalidArgumentException.h"
 
 
 namespace storm {
diff --git a/test/functional/parser/DeterministicModelParserTest.cpp b/test/functional/parser/DeterministicModelParserTest.cpp
index 305df7e46..53fe51ca4 100644
--- a/test/functional/parser/DeterministicModelParserTest.cpp
+++ b/test/functional/parser/DeterministicModelParserTest.cpp
@@ -6,6 +6,10 @@
 #include "src/models/sparse/Ctmc.h"
 #include "src/exceptions/FileIoException.h"
 
+#include "src/exceptions/InvalidArgumentException.h"
+
+#include "src/exceptions/OutOfRangeException.h"
+
 TEST(DeterministicModelParserTest, NonExistingFile) {
 	// No matter what happens, please do NOT create a file with the name "nonExistingFile.not"!
 	ASSERT_THROW(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException);
diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp
index 3a07f46f7..f8bab07e5 100644
--- a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp
+++ b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp
@@ -16,6 +16,8 @@
 #include "src/exceptions/FileIoException.h"
 #include "src/exceptions/WrongFormatException.h"
 
+#include "src/exceptions/InvalidArgumentException.h"
+
 TEST(DeterministicSparseTransitionParserTest, NonExistingFile) {
 
 	// No matter what happens, please do NOT create a file with the name "nonExistingFile.not"!
diff --git a/test/functional/parser/MarkovAutomatonParserTest.cpp b/test/functional/parser/MarkovAutomatonParserTest.cpp
index b104d43fc..479b60752 100644
--- a/test/functional/parser/MarkovAutomatonParserTest.cpp
+++ b/test/functional/parser/MarkovAutomatonParserTest.cpp
@@ -3,6 +3,7 @@
 
 #include "src/parser/MarkovAutomatonParser.h"
 #include "src/exceptions/FileIoException.h"
+#include "src/exceptions/OutOfRangeException.h"
 
 TEST(MarkovAutomatonParserTest, NonExistingFile) {
 
diff --git a/test/functional/parser/NondeterministicModelParserTest.cpp b/test/functional/parser/NondeterministicModelParserTest.cpp
index 3ba479cc9..d87b5cdf0 100644
--- a/test/functional/parser/NondeterministicModelParserTest.cpp
+++ b/test/functional/parser/NondeterministicModelParserTest.cpp
@@ -5,6 +5,9 @@
 #include "src/models/sparse/Mdp.h"
 #include "src/exceptions/FileIoException.h"
 
+#include "src/exceptions/OutOfRangeException.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
 TEST(NondeterministicModelParserTest, NonExistingFile) {
 	// No matter what happens, please do NOT create a file with the name "nonExistingFile.not"!
 	ASSERT_THROW(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException);
diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
index 07fef8955..72ae40e47 100644
--- a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
+++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
@@ -17,6 +17,8 @@
 #include "src/exceptions/FileIoException.h"
 #include "src/exceptions/WrongFormatException.h"
 
+#include "src/exceptions/InvalidArgumentException.h"
+
 TEST(NondeterministicSparseTransitionParserTest, NonExistingFile) {
 
 	// No matter what happens, please do NOT create a file with the name "nonExistingFile.not"!
diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp
index 6e4b9980c..1fe0041f7 100644
--- a/test/functional/storage/SparseMatrixTest.cpp
+++ b/test/functional/storage/SparseMatrixTest.cpp
@@ -1,5 +1,6 @@
 #include "gtest/gtest.h"
 #include "src/storage/SparseMatrix.h"
+#include "src/storage/BitVector.h"
 #include "src/exceptions/InvalidStateException.h"
 #include "src/exceptions/OutOfRangeException.h"