diff --git a/src/formula/AbstractFilter.h b/src/formula/AbstractFilter.h
index ba95d5524..0d03d3b0d 100644
--- a/src/formula/AbstractFilter.h
+++ b/src/formula/AbstractFilter.h
@@ -11,7 +11,7 @@
 #include <vector>
 #include <string>
 #include "src/formula/AbstractFormula.h"
-#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/actions/AbstractAction.h"
 
 namespace storm {
 namespace property {
diff --git a/src/formula/Csl.h b/src/formula/Csl.h
index 8e856f459..f76385f89 100644
--- a/src/formula/Csl.h
+++ b/src/formula/Csl.h
@@ -10,19 +10,19 @@
 
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
-#include "Csl/And.h"
-#include "Csl/Ap.h"
-#include "Csl/Next.h"
-#include "Csl/Not.h"
-#include "Csl/Or.h"
-#include "Csl/ProbabilisticBoundOperator.h"
-#include "Csl/SteadyStateBoundOperator.h"
+#include "csl/And.h"
+#include "csl/Ap.h"
+#include "csl/Next.h"
+#include "csl/Not.h"
+#include "csl/Or.h"
+#include "csl/ProbabilisticBoundOperator.h"
+#include "csl/SteadyStateBoundOperator.h"
 
-#include "Csl/Until.h"
-#include "Csl/Eventually.h"
-#include "Csl/Globally.h"
-#include "Csl/TimeBoundedEventually.h"
-#include "Csl/TimeBoundedUntil.h"
+#include "csl/Until.h"
+#include "csl/Eventually.h"
+#include "csl/Globally.h"
+#include "csl/TimeBoundedEventually.h"
+#include "csl/TimeBoundedUntil.h"
 
 #include "modelchecker/csl/AbstractModelChecker.h"
 
diff --git a/src/formula/Ltl.h b/src/formula/Ltl.h
index cac53a8be..69551ff5c 100644
--- a/src/formula/Ltl.h
+++ b/src/formula/Ltl.h
@@ -10,16 +10,16 @@
 
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
 
-#include "Ltl/And.h"
-#include "Ltl/Ap.h"
-#include "Ltl/BoundedEventually.h"
-#include "Ltl/BoundedUntil.h"
-#include "Ltl/Eventually.h"
-#include "Ltl/Globally.h"
-#include "Ltl/Next.h"
-#include "Ltl/Not.h"
-#include "Ltl/Or.h"
-#include "Ltl/Until.h"
+#include "ltl/And.h"
+#include "ltl/Ap.h"
+#include "ltl/BoundedEventually.h"
+#include "ltl/BoundedUntil.h"
+#include "ltl/Eventually.h"
+#include "ltl/Globally.h"
+#include "ltl/Next.h"
+#include "ltl/Not.h"
+#include "ltl/Or.h"
+#include "ltl/Until.h"
 
 #include "modelchecker/ltl/AbstractModelChecker.h"
 
diff --git a/src/formula/Prctl.h b/src/formula/Prctl.h
index e174d445e..d66e92e03 100644
--- a/src/formula/Prctl.h
+++ b/src/formula/Prctl.h
@@ -10,30 +10,30 @@
 
 #include "modelchecker/prctl/ForwardDeclarations.h"
 
-#include "Prctl/And.h"
-#include "Prctl/Ap.h"
-#include "Prctl/BoundedUntil.h"
-#include "Prctl/BoundedNaryUntil.h"
-#include "Prctl/Next.h"
-#include "Prctl/Not.h"
-#include "Prctl/Or.h"
-#include "Prctl/ProbabilisticBoundOperator.h"
-
-#include "Prctl/Until.h"
-#include "Prctl/Eventually.h"
-#include "Prctl/Globally.h"
-#include "Prctl/BoundedEventually.h"
-
-#include "Prctl/InstantaneousReward.h"
-#include "Prctl/CumulativeReward.h"
-#include "Prctl/ReachabilityReward.h"
-#include "Prctl/RewardBoundOperator.h"
-#include "Prctl/SteadyStateReward.h"
-
-#include "Prctl/AbstractPrctlFormula.h"
-#include "Prctl/AbstractStateFormula.h"
-#include "Prctl/AbstractPathFormula.h"
-#include "Prctl/AbstractRewardPathFormula.h"
+#include "prctl/And.h"
+#include "prctl/Ap.h"
+#include "prctl/BoundedUntil.h"
+#include "prctl/BoundedNaryUntil.h"
+#include "prctl/Next.h"
+#include "prctl/Not.h"
+#include "prctl/Or.h"
+#include "prctl/ProbabilisticBoundOperator.h"
+
+#include "prctl/Until.h"
+#include "prctl/Eventually.h"
+#include "prctl/Globally.h"
+#include "prctl/BoundedEventually.h"
+
+#include "prctl/InstantaneousReward.h"
+#include "prctl/CumulativeReward.h"
+#include "prctl/ReachabilityReward.h"
+#include "prctl/RewardBoundOperator.h"
+#include "prctl/SteadyStateReward.h"
+
+#include "prctl/AbstractPrctlFormula.h"
+#include "prctl/AbstractStateFormula.h"
+#include "prctl/AbstractPathFormula.h"
+#include "prctl/AbstractRewardPathFormula.h"
 
 #include "modelchecker/prctl/AbstractModelChecker.h"
 
diff --git a/src/formula/Actions/AbstractAction.h b/src/formula/actions/AbstractAction.h
similarity index 100%
rename from src/formula/Actions/AbstractAction.h
rename to src/formula/actions/AbstractAction.h
diff --git a/src/formula/Actions/BoundAction.h b/src/formula/actions/BoundAction.h
similarity index 62%
rename from src/formula/Actions/BoundAction.h
rename to src/formula/actions/BoundAction.h
index 4b7f77cc0..f90107742 100644
--- a/src/formula/Actions/BoundAction.h
+++ b/src/formula/actions/BoundAction.h
@@ -8,8 +8,9 @@
 #ifndef STORM_FORMULA_ACTION_BOUNDACTION_H_
 #define STORM_FORMULA_ACTION_BOUNDACTION_H_
 
-#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/actions/AbstractAction.h"
 #include "src/formula/ComparisonType.h"
+#include "src/exceptions/InvalidArgumentException.h"
 
 namespace storm {
 namespace property {
@@ -78,8 +79,8 @@ public:
 				out += ">=";
 				break;
 			default:
-				LOG4CPLUS_INFO(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
-				std::cout << "Unknown comparison operator of value " << comparisonOperator << "." << std::endl;
+				LOG4CPLUS_ERROR(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
+				throw storm::exceptions::InvalidArgumentException() << "Unknown comparison operator of value " << comparisonOperator << ".";
 				break;
 		}
 		out += ", ";
@@ -100,25 +101,30 @@ private:
 
 		if(result.pathResult.size() != 0) {
 
-			//Fill the selction by comapring the values for all previously selected states with theegiven bound using the comparison operator.
-			for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
-				if(result.selection[result.stateMap[i]]) {
+			if(result.stateResult.size() != 0) {
+				LOG4CPLUS_WARN(logger, "Both pathResult and stateResult are set. The filter action is applied using only the pathResult.");
+				std::cout << "Both pathResult and stateResult are set. The filter action is applied using only the pathResult." << std::endl;
+			}
+
+			//Fill the selection by comparing the values for all previously selected states with the given bound using the comparison operator.
+			for(uint_fast64_t i = 0; i < result.pathResult.size(); i++) {
+				if(result.selection[i]) {
 					switch(comparisonOperator) {
 						case storm::property::GREATER_EQUAL:
-							out.set(result.pathResult[result.stateMap[i]] >= bound);
+							out.set(i, result.pathResult[i] >= bound);
 							break;
 						case storm::property::GREATER:
-							out.set(result.pathResult[result.stateMap[i]] > bound);
+							out.set(i, result.pathResult[i] > bound);
 							break;
 						case storm::property::LESS_EQUAL:
-							out.set(result.pathResult[result.stateMap[i]] <= bound);
+							out.set(i, result.pathResult[i] <= bound);
 							break;
 						case storm::property::LESS:
-							out.set(result.pathResult[result.stateMap[i]] < bound);
+							out.set(i, result.pathResult[i] < bound);
 							break;
 						default:
-							LOG4CPLUS_INFO(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
-							std::cout << "Unknown comparison operator of value " << comparisonOperator << "." << std::endl;
+							LOG4CPLUS_ERROR(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
+							throw storm::exceptions::InvalidArgumentException() << "Unknown comparison operator of value " << comparisonOperator << ".";
 							break;
 					}
 				}
@@ -127,23 +133,23 @@ private:
 
 			//Fill the selction by comapring the values for all previously selected states with theegiven bound using the comparison operator.
 			for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
-				if(result.selection[result.stateMap[i]]) {
+				if(result.selection[i]) {
 					switch(comparisonOperator) {
 						case storm::property::GREATER_EQUAL:
-							out.set(result.stateResult[result.stateMap[i]] >= bound);
+							out.set(i, result.stateResult[i] >= bound);
 							break;
 						case storm::property::GREATER:
-							out.set(result.stateResult[result.stateMap[i]] > bound);
+							out.set(i, result.stateResult[i] > bound);
 							break;
 						case storm::property::LESS_EQUAL:
-							out.set(result.stateResult[result.stateMap[i]] <= bound);
+							out.set(i, result.stateResult[i] <= bound);
 							break;
 						case storm::property::LESS:
-							out.set(result.stateResult[result.stateMap[i]] < bound);
+							out.set(i, result.stateResult[i] < bound);
 							break;
 						default:
-							LOG4CPLUS_INFO(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
-							std::cout << "Unknown comparison operator of value " << comparisonOperator << "." << std::endl;
+							LOG4CPLUS_ERROR(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
+							throw storm::exceptions::InvalidArgumentException() << "Unknown comparison operator of value " << comparisonOperator << ".";
 							break;
 					}
 				}
diff --git a/src/formula/Actions/FormulaAction.h b/src/formula/actions/FormulaAction.h
similarity index 94%
rename from src/formula/Actions/FormulaAction.h
rename to src/formula/actions/FormulaAction.h
index 805bc1acb..e3867c721 100644
--- a/src/formula/Actions/FormulaAction.h
+++ b/src/formula/actions/FormulaAction.h
@@ -8,8 +8,9 @@
 #ifndef STORM_FORMULA_ACTION_FORMULAACTION_H_
 #define STORM_FORMULA_ACTION_FORMULAACTION_H_
 
-#include "src/formula/Actions/AbstractAction.h"
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/actions/AbstractAction.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 
 
 #include <string>
diff --git a/src/formula/Actions/InvertAction.h b/src/formula/actions/InvertAction.h
similarity index 96%
rename from src/formula/Actions/InvertAction.h
rename to src/formula/actions/InvertAction.h
index 90192020c..5492e4644 100644
--- a/src/formula/Actions/InvertAction.h
+++ b/src/formula/actions/InvertAction.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_ACTION_INVERTACTION_H_
 #define STORM_FORMULA_ACTION_INVERTACTION_H_
 
-#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/actions/AbstractAction.h"
 
 namespace storm {
 namespace property {
diff --git a/src/formula/Actions/RangeAction.h b/src/formula/actions/RangeAction.h
similarity index 98%
rename from src/formula/Actions/RangeAction.h
rename to src/formula/actions/RangeAction.h
index ce8b0e2ae..85cf7c4af 100644
--- a/src/formula/Actions/RangeAction.h
+++ b/src/formula/actions/RangeAction.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_ACTION_RANGEACTION_H_
 #define STORM_FORMULA_ACTION_RANGEACTION_H_
 
-#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/actions/AbstractAction.h"
 
 namespace storm {
 namespace property {
diff --git a/src/formula/Actions/SortAction.h b/src/formula/actions/SortAction.h
similarity index 98%
rename from src/formula/Actions/SortAction.h
rename to src/formula/actions/SortAction.h
index 5a4c1c622..d75e32fd7 100644
--- a/src/formula/Actions/SortAction.h
+++ b/src/formula/actions/SortAction.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_ACTION_SORTACTION_H_
 #define STORM_FORMULA_ACTION_SORTACTION_H_
 
-#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/actions/AbstractAction.h"
 #include <cctype>
 
 namespace storm {
diff --git a/src/formula/Csl/AbstractCslFormula.h b/src/formula/csl/AbstractCslFormula.h
similarity index 100%
rename from src/formula/Csl/AbstractCslFormula.h
rename to src/formula/csl/AbstractCslFormula.h
diff --git a/src/formula/Csl/AbstractPathFormula.h b/src/formula/csl/AbstractPathFormula.h
similarity index 97%
rename from src/formula/Csl/AbstractPathFormula.h
rename to src/formula/csl/AbstractPathFormula.h
index 951bc6f41..d2cd10fa9 100644
--- a/src/formula/Csl/AbstractPathFormula.h
+++ b/src/formula/csl/AbstractPathFormula.h
@@ -16,7 +16,7 @@ template<class T> class AbstractPathFormula;
 } //namespace property
 } //namespace storm
 
-#include "src/formula/Csl/AbstractCslFormula.h"
+#include "src/formula/csl/AbstractCslFormula.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
 #include <vector>
diff --git a/src/formula/Csl/AbstractStateFormula.h b/src/formula/csl/AbstractStateFormula.h
similarity index 97%
rename from src/formula/Csl/AbstractStateFormula.h
rename to src/formula/csl/AbstractStateFormula.h
index 2bd16471b..07f227961 100644
--- a/src/formula/Csl/AbstractStateFormula.h
+++ b/src/formula/csl/AbstractStateFormula.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_
 #define STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_
 
-#include "src/formula/Csl/AbstractCslFormula.h"
+#include "src/formula/csl/AbstractCslFormula.h"
 #include "src/storage/BitVector.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
diff --git a/src/formula/Csl/And.h b/src/formula/csl/And.h
similarity index 98%
rename from src/formula/Csl/And.h
rename to src/formula/csl/And.h
index 1453cc30b..e8a04e79f 100644
--- a/src/formula/Csl/And.h
+++ b/src/formula/csl/And.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_CSL_AND_H_
 #define STORM_FORMULA_CSL_AND_H_
 
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 #include <string>
diff --git a/src/formula/Csl/Ap.h b/src/formula/csl/Ap.h
similarity index 98%
rename from src/formula/Csl/Ap.h
rename to src/formula/csl/Ap.h
index 66f49c503..0f59dd97b 100644
--- a/src/formula/Csl/Ap.h
+++ b/src/formula/csl/Ap.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_CSL_AP_H_
 #define STORM_FORMULA_CSL_AP_H_
 
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
diff --git a/src/formula/Csl/CslFilter.h b/src/formula/csl/CslFilter.h
similarity index 97%
rename from src/formula/Csl/CslFilter.h
rename to src/formula/csl/CslFilter.h
index 928163fbd..c6144ad02 100644
--- a/src/formula/Csl/CslFilter.h
+++ b/src/formula/csl/CslFilter.h
@@ -9,12 +9,12 @@
 #define STORM_FORMULA_PRCTL_CSLFILTER_H_
 
 #include "src/formula/AbstractFilter.h"
-#include "src/formula/Csl/AbstractCslFormula.h"
-#include "src/formula/Csl/AbstractPathFormula.h"
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractCslFormula.h"
+#include "src/formula/csl/AbstractPathFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 #include "src/modelchecker/csl/AbstractModelChecker.h"
 
-#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/actions/AbstractAction.h"
 
 namespace storm {
 namespace property {
diff --git a/src/formula/Csl/Eventually.h b/src/formula/csl/Eventually.h
similarity index 97%
rename from src/formula/Csl/Eventually.h
rename to src/formula/csl/Eventually.h
index 1d1f1a358..c72f0ce8e 100644
--- a/src/formula/Csl/Eventually.h
+++ b/src/formula/csl/Eventually.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_CSL_EVENTUALLY_H_
 #define STORM_FORMULA_CSL_EVENTUALLY_H_
 
-#include "src/formula/Csl/AbstractPathFormula.h"
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractPathFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
 namespace storm {
diff --git a/src/formula/Csl/Globally.h b/src/formula/csl/Globally.h
similarity index 97%
rename from src/formula/Csl/Globally.h
rename to src/formula/csl/Globally.h
index 85cd32396..f4cd4e71c 100644
--- a/src/formula/Csl/Globally.h
+++ b/src/formula/csl/Globally.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_CSL_GLOBALLY_H_
 #define STORM_FORMULA_CSL_GLOBALLY_H_
 
-#include "src/formula/Csl/AbstractPathFormula.h"
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractPathFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
diff --git a/src/formula/Csl/Next.h b/src/formula/csl/Next.h
similarity index 97%
rename from src/formula/Csl/Next.h
rename to src/formula/csl/Next.h
index f014190aa..e1c7d5407 100644
--- a/src/formula/Csl/Next.h
+++ b/src/formula/csl/Next.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_CSL_NEXT_H_
 #define STORM_FORMULA_CSL_NEXT_H_
 
-#include "src/formula/Csl/AbstractPathFormula.h"
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractPathFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
diff --git a/src/formula/Csl/Not.h b/src/formula/csl/Not.h
similarity index 98%
rename from src/formula/Csl/Not.h
rename to src/formula/csl/Not.h
index 58ca37299..05a924819 100644
--- a/src/formula/Csl/Not.h
+++ b/src/formula/csl/Not.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_CSL_NOT_H_
 #define STORM_FORMULA_CSL_NOT_H_
 
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
diff --git a/src/formula/Csl/Or.h b/src/formula/csl/Or.h
similarity index 98%
rename from src/formula/Csl/Or.h
rename to src/formula/csl/Or.h
index 9533b873a..9eb575b38 100644
--- a/src/formula/Csl/Or.h
+++ b/src/formula/csl/Or.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_CSL_OR_H_
 #define STORM_FORMULA_CSL_OR_H_
 
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
diff --git a/src/formula/Csl/ProbabilisticBoundOperator.h b/src/formula/csl/ProbabilisticBoundOperator.h
similarity index 98%
rename from src/formula/Csl/ProbabilisticBoundOperator.h
rename to src/formula/csl/ProbabilisticBoundOperator.h
index d40bb90e2..48553bb85 100644
--- a/src/formula/Csl/ProbabilisticBoundOperator.h
+++ b/src/formula/csl/ProbabilisticBoundOperator.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_
 #define STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_
 
-#include "src/formula/Csl/AbstractStateFormula.h"
-#include "src/formula/Csl/AbstractPathFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractPathFormula.h"
 #include "src/formula/ComparisonType.h"
 #include "utility/constants.h"
 
diff --git a/src/formula/Csl/SteadyStateBoundOperator.h b/src/formula/csl/SteadyStateBoundOperator.h
similarity index 100%
rename from src/formula/Csl/SteadyStateBoundOperator.h
rename to src/formula/csl/SteadyStateBoundOperator.h
diff --git a/src/formula/Csl/TimeBoundedEventually.h b/src/formula/csl/TimeBoundedEventually.h
similarity index 97%
rename from src/formula/Csl/TimeBoundedEventually.h
rename to src/formula/csl/TimeBoundedEventually.h
index c80eecb4b..f8ef249cf 100644
--- a/src/formula/Csl/TimeBoundedEventually.h
+++ b/src/formula/csl/TimeBoundedEventually.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_
 #define STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_
 
-#include "src/formula/Csl/AbstractPathFormula.h"
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractPathFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 
 namespace storm {
 namespace property {
diff --git a/src/formula/Csl/TimeBoundedUntil.h b/src/formula/csl/TimeBoundedUntil.h
similarity index 98%
rename from src/formula/Csl/TimeBoundedUntil.h
rename to src/formula/csl/TimeBoundedUntil.h
index 3da7fa968..96cb87f24 100644
--- a/src/formula/Csl/TimeBoundedUntil.h
+++ b/src/formula/csl/TimeBoundedUntil.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_
 #define STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_
 
-#include "src/formula/Csl/AbstractPathFormula.h"
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractPathFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 
 namespace storm {
 namespace property {
diff --git a/src/formula/Csl/Until.h b/src/formula/csl/Until.h
similarity index 97%
rename from src/formula/Csl/Until.h
rename to src/formula/csl/Until.h
index 34b44b780..199956d37 100644
--- a/src/formula/Csl/Until.h
+++ b/src/formula/csl/Until.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_CSL_UNTIL_H_
 #define STORM_FORMULA_CSL_UNTIL_H_
 
-#include "src/formula/Csl/AbstractPathFormula.h"
-#include "src/formula/Csl/AbstractStateFormula.h"
+#include "src/formula/csl/AbstractPathFormula.h"
+#include "src/formula/csl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/ltl/AbstractLtlFormula.h
similarity index 100%
rename from src/formula/Ltl/AbstractLtlFormula.h
rename to src/formula/ltl/AbstractLtlFormula.h
diff --git a/src/formula/Ltl/And.h b/src/formula/ltl/And.h
similarity index 100%
rename from src/formula/Ltl/And.h
rename to src/formula/ltl/And.h
diff --git a/src/formula/Ltl/Ap.h b/src/formula/ltl/Ap.h
similarity index 100%
rename from src/formula/Ltl/Ap.h
rename to src/formula/ltl/Ap.h
diff --git a/src/formula/Ltl/BoundedEventually.h b/src/formula/ltl/BoundedEventually.h
similarity index 100%
rename from src/formula/Ltl/BoundedEventually.h
rename to src/formula/ltl/BoundedEventually.h
diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/ltl/BoundedUntil.h
similarity index 99%
rename from src/formula/Ltl/BoundedUntil.h
rename to src/formula/ltl/BoundedUntil.h
index 5daf126b8..755467ef1 100644
--- a/src/formula/Ltl/BoundedUntil.h
+++ b/src/formula/ltl/BoundedUntil.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_LTL_BOUNDEDUNTIL_H_
 #define STORM_FORMULA_LTL_BOUNDEDUNTIL_H_
 
-#include "src/formula/Ltl/AbstractLtlFormula.h"
+#include "src/formula/ltl/AbstractLtlFormula.h"
 #include <cstdint>
 #include <string>
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
diff --git a/src/formula/Ltl/Eventually.h b/src/formula/ltl/Eventually.h
similarity index 98%
rename from src/formula/Ltl/Eventually.h
rename to src/formula/ltl/Eventually.h
index 2825292fe..983ce2de4 100644
--- a/src/formula/Ltl/Eventually.h
+++ b/src/formula/ltl/Eventually.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_LTL_EVENTUALLY_H_
 #define STORM_FORMULA_LTL_EVENTUALLY_H_
 
-#include "src/formula/Ltl/AbstractLtlFormula.h"
+#include "src/formula/ltl/AbstractLtlFormula.h"
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
 
 namespace storm {
diff --git a/src/formula/Ltl/Globally.h b/src/formula/ltl/Globally.h
similarity index 100%
rename from src/formula/Ltl/Globally.h
rename to src/formula/ltl/Globally.h
diff --git a/src/formula/Ltl/LtlFilter.h b/src/formula/ltl/LtlFilter.h
similarity index 98%
rename from src/formula/Ltl/LtlFilter.h
rename to src/formula/ltl/LtlFilter.h
index 96fac586c..b8d7846c0 100644
--- a/src/formula/Ltl/LtlFilter.h
+++ b/src/formula/ltl/LtlFilter.h
@@ -10,8 +10,8 @@
 
 #include "src/formula/AbstractFilter.h"
 #include "src/modelchecker/ltl/AbstractModelChecker.h"
-#include "src/formula/Ltl/AbstractLtlFormula.h"
-#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/ltl/AbstractLtlFormula.h"
+#include "src/formula/actions/AbstractAction.h"
 #include "src/exceptions/NotImplementedException.h"
 
 namespace storm {
diff --git a/src/formula/Ltl/Next.h b/src/formula/ltl/Next.h
similarity index 100%
rename from src/formula/Ltl/Next.h
rename to src/formula/ltl/Next.h
diff --git a/src/formula/Ltl/Not.h b/src/formula/ltl/Not.h
similarity index 100%
rename from src/formula/Ltl/Not.h
rename to src/formula/ltl/Not.h
diff --git a/src/formula/Ltl/Or.h b/src/formula/ltl/Or.h
similarity index 100%
rename from src/formula/Ltl/Or.h
rename to src/formula/ltl/Or.h
diff --git a/src/formula/Ltl/Until.h b/src/formula/ltl/Until.h
similarity index 100%
rename from src/formula/Ltl/Until.h
rename to src/formula/ltl/Until.h
diff --git a/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.cpp b/src/formula/ltl/visitor/AbstractLtlFormulaVisitor.cpp
similarity index 100%
rename from src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.cpp
rename to src/formula/ltl/visitor/AbstractLtlFormulaVisitor.cpp
diff --git a/src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h b/src/formula/ltl/visitor/AbstractLtlFormulaVisitor.h
similarity index 100%
rename from src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h
rename to src/formula/ltl/visitor/AbstractLtlFormulaVisitor.h
diff --git a/src/formula/Prctl/AbstractPathFormula.h b/src/formula/prctl/AbstractPathFormula.h
similarity index 97%
rename from src/formula/Prctl/AbstractPathFormula.h
rename to src/formula/prctl/AbstractPathFormula.h
index 62bb1f7f4..50040082f 100644
--- a/src/formula/Prctl/AbstractPathFormula.h
+++ b/src/formula/prctl/AbstractPathFormula.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
 #define STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
 
-#include "src/formula/Prctl/AbstractPrctlFormula.h"
+#include "src/formula/prctl/AbstractPrctlFormula.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 #include <vector>
diff --git a/src/formula/Prctl/AbstractPrctlFormula.h b/src/formula/prctl/AbstractPrctlFormula.h
similarity index 100%
rename from src/formula/Prctl/AbstractPrctlFormula.h
rename to src/formula/prctl/AbstractPrctlFormula.h
diff --git a/src/formula/Prctl/AbstractRewardPathFormula.h b/src/formula/prctl/AbstractRewardPathFormula.h
similarity index 97%
rename from src/formula/Prctl/AbstractRewardPathFormula.h
rename to src/formula/prctl/AbstractRewardPathFormula.h
index 844adb25b..d28e1003d 100644
--- a/src/formula/Prctl/AbstractRewardPathFormula.h
+++ b/src/formula/prctl/AbstractRewardPathFormula.h
@@ -8,6 +8,8 @@
 #ifndef STORM_FORMULA_PRCTL_ABSTRACTREWARDPATHFORMULA_H_
 #define STORM_FORMULA_PRCTL_ABSTRACTREWARDPATHFORMULA_H_
 
+#include "src/formula/prctl/AbstractPrctlFormula.h"
+
 namespace storm {
 namespace property {
 namespace prctl {
diff --git a/src/formula/Prctl/AbstractStateFormula.h b/src/formula/prctl/AbstractStateFormula.h
similarity index 97%
rename from src/formula/Prctl/AbstractStateFormula.h
rename to src/formula/prctl/AbstractStateFormula.h
index 7eed7fb6a..8af034faa 100644
--- a/src/formula/Prctl/AbstractStateFormula.h
+++ b/src/formula/prctl/AbstractStateFormula.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_
 #define STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_
 
-#include "src/formula/Prctl/AbstractPrctlFormula.h"
+#include "src/formula/prctl/AbstractPrctlFormula.h"
 #include "src/storage/BitVector.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
diff --git a/src/formula/Prctl/And.h b/src/formula/prctl/And.h
similarity index 98%
rename from src/formula/Prctl/And.h
rename to src/formula/prctl/And.h
index dcda9e802..b364e3a63 100644
--- a/src/formula/Prctl/And.h
+++ b/src/formula/prctl/And.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_AND_H_
 #define STORM_FORMULA_PRCTL_AND_H_
 
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 #include <string>
diff --git a/src/formula/Prctl/Ap.h b/src/formula/prctl/Ap.h
similarity index 98%
rename from src/formula/Prctl/Ap.h
rename to src/formula/prctl/Ap.h
index 7e234d434..21ed5b82f 100644
--- a/src/formula/Prctl/Ap.h
+++ b/src/formula/prctl/Ap.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_AP_H_
 #define STORM_FORMULA_PRCTL_AP_H_
 
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
diff --git a/src/formula/Prctl/BoundedEventually.h b/src/formula/prctl/BoundedEventually.h
similarity index 97%
rename from src/formula/Prctl/BoundedEventually.h
rename to src/formula/prctl/BoundedEventually.h
index 0da53493f..59e319b28 100644
--- a/src/formula/Prctl/BoundedEventually.h
+++ b/src/formula/prctl/BoundedEventually.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_PRCTL_BOUNDEDEVENTUALLY_H_
 #define STORM_FORMULA_PRCTL_BOUNDEDEVENTUALLY_H_
 
-#include "src/formula/Prctl/AbstractPathFormula.h"
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/prctl/AbstractPathFormula.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include <cstdint>
 #include <string>
diff --git a/src/formula/Prctl/BoundedNaryUntil.h b/src/formula/prctl/BoundedNaryUntil.h
similarity index 98%
rename from src/formula/Prctl/BoundedNaryUntil.h
rename to src/formula/prctl/BoundedNaryUntil.h
index 9c27158ba..7fc91830d 100644
--- a/src/formula/Prctl/BoundedNaryUntil.h
+++ b/src/formula/prctl/BoundedNaryUntil.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_
 #define STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_
 
-#include "src/formula/Prctl/AbstractPathFormula.h"
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/prctl/AbstractPathFormula.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
 #include <cstdint>
 #include <string>
 #include <vector>
diff --git a/src/formula/Prctl/BoundedUntil.h b/src/formula/prctl/BoundedUntil.h
similarity index 98%
rename from src/formula/Prctl/BoundedUntil.h
rename to src/formula/prctl/BoundedUntil.h
index d7c9d28ca..206c0a202 100644
--- a/src/formula/Prctl/BoundedUntil.h
+++ b/src/formula/prctl/BoundedUntil.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_
 #define STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_
 
-#include "src/formula/Prctl/AbstractPathFormula.h"
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/prctl/AbstractPathFormula.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
 #include <cstdint>
 #include <string>
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
diff --git a/src/formula/Prctl/CumulativeReward.h b/src/formula/prctl/CumulativeReward.h
similarity index 100%
rename from src/formula/Prctl/CumulativeReward.h
rename to src/formula/prctl/CumulativeReward.h
diff --git a/src/formula/Prctl/Eventually.h b/src/formula/prctl/Eventually.h
similarity index 97%
rename from src/formula/Prctl/Eventually.h
rename to src/formula/prctl/Eventually.h
index 733fc924b..cbcbf8c4d 100644
--- a/src/formula/Prctl/Eventually.h
+++ b/src/formula/prctl/Eventually.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_PRCTL_EVENTUALLY_H_
 #define STORM_FORMULA_PRCTL_EVENTUALLY_H_
 
-#include "src/formula/Prctl/AbstractPathFormula.h"
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/prctl/AbstractPathFormula.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
diff --git a/src/formula/Prctl/Globally.h b/src/formula/prctl/Globally.h
similarity index 97%
rename from src/formula/Prctl/Globally.h
rename to src/formula/prctl/Globally.h
index 67a824254..49b4d6d96 100644
--- a/src/formula/Prctl/Globally.h
+++ b/src/formula/prctl/Globally.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_PRCTL_GLOBALLY_H_
 #define STORM_FORMULA_PRCTL_GLOBALLY_H_
 
-#include "src/formula/Prctl/AbstractPathFormula.h"
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/prctl/AbstractPathFormula.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
diff --git a/src/formula/Prctl/InstantaneousReward.h b/src/formula/prctl/InstantaneousReward.h
similarity index 100%
rename from src/formula/Prctl/InstantaneousReward.h
rename to src/formula/prctl/InstantaneousReward.h
diff --git a/src/formula/Prctl/Next.h b/src/formula/prctl/Next.h
similarity index 97%
rename from src/formula/Prctl/Next.h
rename to src/formula/prctl/Next.h
index 776195903..e218d036e 100644
--- a/src/formula/Prctl/Next.h
+++ b/src/formula/prctl/Next.h
@@ -8,8 +8,8 @@
 #ifndef STORM_FORMULA_PRCTL_NEXT_H_
 #define STORM_FORMULA_PRCTL_NEXT_H_
 
-#include "src/formula/Prctl/AbstractPathFormula.h"
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/prctl/AbstractPathFormula.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
diff --git a/src/formula/Prctl/Not.h b/src/formula/prctl/Not.h
similarity index 100%
rename from src/formula/Prctl/Not.h
rename to src/formula/prctl/Not.h
diff --git a/src/formula/Prctl/Or.h b/src/formula/prctl/Or.h
similarity index 98%
rename from src/formula/Prctl/Or.h
rename to src/formula/prctl/Or.h
index dc92ee10a..01482bb33 100644
--- a/src/formula/Prctl/Or.h
+++ b/src/formula/prctl/Or.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_OR_H_
 #define STORM_FORMULA_PRCTL_OR_H_
 
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
diff --git a/src/formula/Prctl/PrctlFilter.h b/src/formula/prctl/PrctlFilter.h
similarity index 98%
rename from src/formula/Prctl/PrctlFilter.h
rename to src/formula/prctl/PrctlFilter.h
index 395337b9a..f9db17d9a 100644
--- a/src/formula/Prctl/PrctlFilter.h
+++ b/src/formula/prctl/PrctlFilter.h
@@ -9,11 +9,11 @@
 #define STORM_FORMULA_PRCTL_PRCTLFILTER_H_
 
 #include "src/formula/AbstractFilter.h"
-#include "src/formula/Prctl/AbstractPrctlFormula.h"
-#include "src/formula/Prctl/AbstractPathFormula.h"
-#include "src/formula/Prctl/AbstractStateFormula.h"
+#include "src/formula/prctl/AbstractPrctlFormula.h"
+#include "src/formula/prctl/AbstractPathFormula.h"
+#include "src/formula/prctl/AbstractStateFormula.h"
 #include "src/modelchecker/prctl/AbstractModelChecker.h"
-#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/actions/AbstractAction.h"
 
 // TODO: Test if this can be can be ommitted.
 namespace storm {
diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/prctl/ProbabilisticBoundOperator.h
similarity index 100%
rename from src/formula/Prctl/ProbabilisticBoundOperator.h
rename to src/formula/prctl/ProbabilisticBoundOperator.h
diff --git a/src/formula/Prctl/ReachabilityReward.h b/src/formula/prctl/ReachabilityReward.h
similarity index 100%
rename from src/formula/Prctl/ReachabilityReward.h
rename to src/formula/prctl/ReachabilityReward.h
diff --git a/src/formula/Prctl/RewardBoundOperator.h b/src/formula/prctl/RewardBoundOperator.h
similarity index 100%
rename from src/formula/Prctl/RewardBoundOperator.h
rename to src/formula/prctl/RewardBoundOperator.h
diff --git a/src/formula/Prctl/SteadyStateReward.h b/src/formula/prctl/SteadyStateReward.h
similarity index 100%
rename from src/formula/Prctl/SteadyStateReward.h
rename to src/formula/prctl/SteadyStateReward.h
diff --git a/src/formula/Prctl/Until.h b/src/formula/prctl/Until.h
similarity index 100%
rename from src/formula/Prctl/Until.h
rename to src/formula/prctl/Until.h
diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp
index f7b11dd14..00a1c1db4 100644
--- a/src/parser/CslParser.cpp
+++ b/src/parser/CslParser.cpp
@@ -10,12 +10,12 @@
 #include "src/utility/constants.h"
 
 // The action class headers.
-#include "src/formula/Actions/AbstractAction.h"
-#include "src/formula/Actions/BoundAction.h"
-#include "src/formula/Actions/InvertAction.h"
-#include "src/formula/Actions/FormulaAction.h"
-#include "src/formula/Actions/RangeAction.h"
-#include "src/formula/Actions/SortAction.h"
+#include "src/formula/actions/AbstractAction.h"
+#include "src/formula/actions/BoundAction.h"
+#include "src/formula/actions/InvertAction.h"
+#include "src/formula/actions/FormulaAction.h"
+#include "src/formula/actions/RangeAction.h"
+#include "src/formula/actions/SortAction.h"
 
 // If the parser fails due to ill-formed data, this exception is thrown.
 #include "src/exceptions/WrongFormatException.h"
diff --git a/src/parser/CslParser.h b/src/parser/CslParser.h
index ddc767438..0960f742f 100644
--- a/src/parser/CslParser.h
+++ b/src/parser/CslParser.h
@@ -9,7 +9,7 @@
 #define STORM_PARSER_CSLPARSER_H_
 
 #include "src/formula/Csl.h"
-#include "src/formula/Csl/CslFilter.h"
+#include "src/formula/csl/CslFilter.h"
 #include <functional>
 
 namespace storm {
diff --git a/src/parser/LtlFileParser.cpp b/src/parser/LtlFileParser.cpp
index d3d9459ae..8ede743a8 100644
--- a/src/parser/LtlFileParser.cpp
+++ b/src/parser/LtlFileParser.cpp
@@ -15,7 +15,7 @@
 namespace storm {
 namespace parser {
 
-std::list<storm::property::ltl::LtlFilter<double>*> LtlFileParser(std::string filename) {
+std::list<storm::property::ltl::LtlFilter<double>*> LtlFileParser::parseLtlFile(std::string filename) {
 	// Open file
 	std::ifstream inputFileStream(filename, std::ios::in);
 
@@ -30,7 +30,7 @@ std::list<storm::property::ltl::LtlFilter<double>*> LtlFileParser(std::string fi
 		std::string line;
 		//The while loop reads the input file line by line
 		while (std::getline(inputFileStream, line)) {
-			result.push_back(storm::parser::LtlParser(line));
+			result.push_back(storm::parser::LtlParser::parseLtlFormula(line));
 		}
 	}
 
diff --git a/src/parser/LtlFileParser.h b/src/parser/LtlFileParser.h
index 7c30abc11..b8375ecec 100644
--- a/src/parser/LtlFileParser.h
+++ b/src/parser/LtlFileParser.h
@@ -9,20 +9,24 @@
 #define LTLFILEPARSER_H_
 
 #include "formula/Ltl.h"
-#include "src/formula/Ltl/LtlFilter.h"
+#include "src/formula/ltl/LtlFilter.h"
 
 #include <list>
 
 namespace storm {
 namespace parser {
 
-/*!
- * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
- *
- * @param filename
- * @return The list of parsed formulas
- */
-std::list<storm::property::ltl::LtlFilter<double>*> LtlFileParser(std::string filename);
+class LtlFileParser {
+public:
+
+	/*!
+	 * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
+	 *
+	 * @param filename
+	 * @return The list of parsed formulas
+	 */
+	static std::list<storm::property::ltl::LtlFilter<double>*> parseLtlFile(std::string filename);
+};
 
 } //namespace parser
 } //namespace storm
diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp
index 6c4787fee..2c7e09a06 100644
--- a/src/parser/LtlParser.cpp
+++ b/src/parser/LtlParser.cpp
@@ -11,11 +11,11 @@
 #include "src/utility/constants.h"
 
 // The action class headers.
-#include "src/formula/Actions/AbstractAction.h"
-#include "src/formula/Actions/BoundAction.h"
-#include "src/formula/Actions/InvertAction.h"
-#include "src/formula/Actions/RangeAction.h"
-#include "src/formula/Actions/SortAction.h"
+#include "src/formula/actions/AbstractAction.h"
+#include "src/formula/actions/BoundAction.h"
+#include "src/formula/actions/InvertAction.h"
+#include "src/formula/actions/RangeAction.h"
+#include "src/formula/actions/SortAction.h"
 
 // If the parser fails due to ill-formed data, this exception is thrown.
 #include "src/exceptions/WrongFormatException.h"
@@ -48,7 +48,7 @@ namespace storm {
 namespace parser {
 
 template<typename Iterator, typename Skipper>
-struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::LtlFilter<double>*(), Skipper > {
+struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::property::ltl::LtlFilter<double>*(), Skipper > {
 	LtlGrammar() : LtlGrammar::base_type(start) {
 		//This block contains helper rules that may be used several times
 		freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))];
@@ -182,11 +182,7 @@ struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::LtlFilter<double
 
 };
 
-} //namespace storm
-} //namespace parser
-
-
-storm::property::ltl::LtlFilter<double>* storm::parser::LtlParser(std::string formulaString) {
+storm::property::ltl::LtlFilter<double>* LtlParser::parseLtlFormula(std::string formulaString) {
 	// Prepare iterators to input.
 	BaseIteratorType stringIteratorBegin = formulaString.begin();
 	BaseIteratorType stringIteratorEnd = formulaString.end();
@@ -239,3 +235,5 @@ storm::property::ltl::LtlFilter<double>* storm::parser::LtlParser(std::string fo
 	return result_pointer;
 }
 
+} //namespace parser
+} //namespace storm
diff --git a/src/parser/LtlParser.h b/src/parser/LtlParser.h
index bbf10d259..d3d8e426f 100644
--- a/src/parser/LtlParser.h
+++ b/src/parser/LtlParser.h
@@ -9,12 +9,20 @@
 #define STORM_PARSER_LTLPARSER_H_
 
 #include "src/formula/Ltl.h"
-#include "src/formula/Ltl/LtlFilter.h"
+#include "src/formula/ltl/LtlFilter.h"
 
 namespace storm {
 namespace parser {
 
 /*!
+ * Reads a LTL formula from a string and return the formula tree.
+ *
+ * If you want to read the formula from a file, use the LtlFileParser class instead.
+ */
+class LtlParser {
+public:
+
+	/*!
 	* Reads a LTL formula from its string representation and parses it into a formula tree, consisting of
 	* classes in the namespace storm::property.
 	*
@@ -23,13 +31,17 @@ namespace parser {
 	* @param formulaString The string representation of the formula
 	* @throw wrongFormatException If the input could not be parsed successfully
 	*/
-storm::property::ltl::LtlFilter<double>* LtlParser(std::string formulaString);
+	static storm::property::ltl::LtlFilter<double>* parseLtlFormula(std::string formulaString);
 
-/*!
- * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas.
- */
-template<typename Iterator, typename Skipper>
-struct LtlGrammar;
+private:
+
+	/*!
+	 * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas.
+	 */
+	template<typename Iterator, typename Skipper>
+	struct LtlGrammar;
+
+};
 
 } /* namespace parser */
 } /* namespace storm */
diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h
index 4d914d8cc..ad29fe812 100644
--- a/src/parser/PrctlFileParser.h
+++ b/src/parser/PrctlFileParser.h
@@ -9,7 +9,7 @@
 #define STORM_PARSER_PRCTLFILEPARSER_H_
 
 #include "formula/Prctl.h"
-#include "src/formula/Prctl/PrctlFilter.h"
+#include "src/formula/prctl/PrctlFilter.h"
 
 #include <list>
 
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 7675f1cd3..da2336b8b 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -3,12 +3,12 @@
 #include "src/utility/constants.h"
 
 // The action class headers.
-#include "src/formula/Actions/AbstractAction.h"
-#include "src/formula/Actions/BoundAction.h"
-#include "src/formula/Actions/InvertAction.h"
-#include "src/formula/Actions/FormulaAction.h"
-#include "src/formula/Actions/RangeAction.h"
-#include "src/formula/Actions/SortAction.h"
+#include "src/formula/actions/AbstractAction.h"
+#include "src/formula/actions/BoundAction.h"
+#include "src/formula/actions/InvertAction.h"
+#include "src/formula/actions/FormulaAction.h"
+#include "src/formula/actions/RangeAction.h"
+#include "src/formula/actions/SortAction.h"
 
 // If the parser fails due to ill-formed data, this exception is thrown.
 #include "src/exceptions/WrongFormatException.h"
@@ -248,10 +248,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 
 };
 
-} //namespace storm
-} //namespace parser
-
-storm::property::prctl::PrctlFilter<double>* storm::parser::PrctlParser::parsePrctlFormula(std::string formulaString) {
+storm::property::prctl::PrctlFilter<double>* PrctlParser::parsePrctlFormula(std::string formulaString) {
 	// Prepare iterators to input.
 	BaseIteratorType stringIteratorBegin = formulaString.begin();
 	BaseIteratorType stringIteratorEnd = formulaString.end();
@@ -296,3 +293,6 @@ storm::property::prctl::PrctlFilter<double>* storm::parser::PrctlParser::parsePr
 
 	return result_pointer;
 }
+
+} //namespace parser
+} //namespace storm
diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h
index 6e1a55c34..b5832727e 100644
--- a/src/parser/PrctlParser.h
+++ b/src/parser/PrctlParser.h
@@ -2,7 +2,7 @@
 #define STORM_PARSER_PRCTLPARSER_H_
 
 #include "src/formula/Prctl.h"
-#include "src/formula/Prctl/PrctlFilter.h"
+#include "src/formula/prctl/PrctlFilter.h"
 
 namespace storm {
 namespace parser {
@@ -11,10 +11,6 @@ namespace parser {
  * Reads a PRCTL formula from a string and return the formula tree.
  *
  * If you want to read the formula from a file, use the PrctlFileParser class instead.
- *
- * @note
- * This class creates a PctlFormula object which can be accessed through the getFormula() method (of base
- * class PrctlParser). However, it will not delete this object.
  */
 class PrctlParser {
 public:
diff --git a/test/functional/parser/ActionTest.cpp b/test/functional/parser/ActionTest.cpp
new file mode 100644
index 000000000..41d5ab58f
--- /dev/null
+++ b/test/functional/parser/ActionTest.cpp
@@ -0,0 +1,157 @@
+/*
+ * ActionTest.cpp
+ *
+ *  Created on: Jun 27, 2014
+ *      Author: Manuel Sascha Weiand
+ */
+
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "src/formula/actions/BoundAction.h"
+
+#include "src/parser/MarkovAutomatonParser.h"
+#include "src/parser/DeterministicModelParser.h"
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
+#include "src/solver/GmmxxLinearEquationSolver.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+typedef typename storm::property::action::AbstractAction<double>::Result Result;
+
+TEST(ActionTest, BoundActionFunctionality) {
+
+	// Setup the modelchecker.
+	storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
+	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+
+	// Build the filter input.
+	// Basically the modelchecking result of "F a" on the used DTMC.
+	std::vector<double> pathResult = mc.checkEventually(storm::property::prctl::Eventually<double>(new storm::property::prctl::Ap<double>("a")), false);
+	std::vector<uint_fast64_t> stateMap(pathResult.size());
+	for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
+		stateMap[i] = i;
+	}
+	Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector());
+
+	// Test the action.
+	// First test that the boundAction build by the empty constructor does not change the selection.
+	storm::property::action::BoundAction<double> action;
+	Result result = action.evaluate(input, mc);
+
+	for(auto value : result.selection) {
+		ASSERT_TRUE(input.selection[value]);
+	}
+
+	// Test that using a strict bound can give different results than using a non-strict bound.
+	action = storm::property::action::BoundAction<double>(storm::property::GREATER, 0);
+	result = action.evaluate(input, mc);
+
+	for(uint_fast64_t i = 0; i < result.selection.size()-2; i++) {
+		ASSERT_TRUE(result.selection[i]);
+	}
+	ASSERT_FALSE(result.selection[6]);
+	ASSERT_FALSE(result.selection[7]);
+
+	// Check whether the state order has any effect on the selected states, which it should not.
+	for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
+		stateMap[i] = pathResult.size() - i - 1;
+	}
+
+	action = storm::property::action::BoundAction<double>(storm::property::GREATER, 0);
+	result = action.evaluate(input, mc);
+
+	for(uint_fast64_t i = 0; i < result.selection.size()-2; i++) {
+		ASSERT_TRUE(result.selection[i]);
+	}
+	ASSERT_FALSE(result.selection[6]);
+	ASSERT_FALSE(result.selection[7]);
+
+	// Test the functionality for state formulas instead.
+	input.pathResult = std::vector<double>();
+	input.stateResult = mc.checkAp(storm::property::prctl::Ap<double>("a"));
+	action = storm::property::action::BoundAction<double>(storm::property::GREATER, 0.5);
+	result = action.evaluate(input, mc);
+
+	for(uint_fast64_t i = 0; i < result.selection.size(); i++) {
+		if(i == 5) {
+			ASSERT_TRUE(result.selection[i]);
+		} else {
+			ASSERT_FALSE(result.selection[i]);
+		}
+	}
+
+	// Make sure that the modelchecker has no influence on the result.
+	storm::models::MarkovAutomaton<double> ma = storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general.lab");
+	storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker<double> cslMc(ma);
+	result = action.evaluate(input, cslMc);
+
+	for(uint_fast64_t i = 0; i < result.selection.size(); i++) {
+		if(i == 5) {
+			ASSERT_TRUE(result.selection[i]);
+		} else {
+			ASSERT_FALSE(result.selection[i]);
+		}
+	}
+}
+
+TEST(ActionTest, BoundActionSafety) {
+
+	// Setup the modelchecker.
+	storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
+	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+
+	// Build the filter input.
+	// Basically the modelchecking result of "F a" on the used DTMC.
+	std::vector<double> pathResult = mc.checkEventually(storm::property::prctl::Eventually<double>(new storm::property::prctl::Ap<double>("a")), false);
+	storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap<double>("a"));
+	std::vector<uint_fast64_t> stateMap(pathResult.size());
+	for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
+		stateMap[i] = i;
+	}
+	Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector());
+
+	// First, test unusual bounds.
+	storm::property::action::BoundAction<double> action(storm::property::LESS, -2044);
+	Result result;
+
+	ASSERT_NO_THROW(result = action.evaluate(input, mc));
+	ASSERT_EQ(0, result.selection.getNumberOfSetBits());
+
+	action = storm::property::action::BoundAction<double>(storm::property::GREATER_EQUAL, 5879);
+
+	ASSERT_NO_THROW(result = action.evaluate(input, mc));
+	ASSERT_EQ(0, result.selection.getNumberOfSetBits());
+
+	action = storm::property::action::BoundAction<double>(storm::property::LESS_EQUAL, 5879);
+
+	ASSERT_NO_THROW(result = action.evaluate(input, mc));
+	ASSERT_EQ(result.selection.size(), result.selection.getNumberOfSetBits());
+
+	// Now, check the behavior under a undefined comparison type.
+	action = storm::property::action::BoundAction<double>(static_cast<storm::property::ComparisonType>(10), 5879);
+	ASSERT_THROW(action.toString(), storm::exceptions::InvalidArgumentException);
+	ASSERT_THROW(action.evaluate(input, mc), storm::exceptions::InvalidArgumentException);
+
+	// Test for a result input with both results filled.
+	// It should put out a warning and use the pathResult.
+	action = storm::property::action::BoundAction<double>(storm::property::GREATER_EQUAL, 0.5);
+	input.stateResult = stateResult;
+
+	// To capture the warning, redirect cout and test the written buffer content.
+	std::stringstream buffer;
+	std::streambuf *sbuf = std::cout.rdbuf();
+	std::cout.rdbuf(buffer.rdbuf());
+
+	ASSERT_NO_THROW(result = action.evaluate(input, mc));
+	std::cout.rdbuf(sbuf);
+
+	ASSERT_FALSE(buffer.str().empty());
+	ASSERT_TRUE(result.selection[0]);
+	ASSERT_FALSE(result.selection[1]);
+	ASSERT_TRUE(result.selection[2]);
+	ASSERT_TRUE(result.selection[5]);
+
+	// Check for empty input.
+	ASSERT_NO_THROW(result = action.evaluate(Result(), mc));
+}
diff --git a/test/functional/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp
index 1da53769d..bba921506 100644
--- a/test/functional/parser/LtlParserTest.cpp
+++ b/test/functional/parser/LtlParserTest.cpp
@@ -12,9 +12,9 @@
 
 TEST(LtlParserTest, parseApOnlyTest) {
 	std::string formula = "ap";
-	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
+	storm::property::ltl::LtlFilter<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser(formula);
+		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
 	);
 
 	ASSERT_NE(ltlFormula, nullptr);
@@ -25,9 +25,9 @@ TEST(LtlParserTest, parseApOnlyTest) {
 
 TEST(LtlParserTest, parsePropositionalFormulaTest) {
 	std::string formula = "!(a & b) | a & ! c";
-	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
+	storm::property::ltl::LtlFilter<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser(formula);
+		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
 	);
 
 	ASSERT_NE(ltlFormula, nullptr);
@@ -42,9 +42,9 @@ TEST(LtlParserTest, parsePropositionalFormulaTest) {
  */
 TEST(LtlParserTest, parseAmbiguousFormulaTest) {
 	std::string formula = "F & b";
-	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
+	storm::property::ltl::LtlFilter<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser(formula);
+		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
 	);
 
 	ASSERT_NE(ltlFormula, nullptr);
@@ -59,9 +59,9 @@ TEST(LtlParserTest, parseAmbiguousFormulaTest) {
  */
 TEST(LtlParserTest, parseAmbiguousFormulaTest2) {
 	std::string formula = "F F";
-	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
+	storm::property::ltl::LtlFilter<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser(formula);
+		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
 	);
 
 	ASSERT_NE(ltlFormula, nullptr);
@@ -72,14 +72,14 @@ TEST(LtlParserTest, parseAmbiguousFormulaTest2) {
 
 TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) {
 	std::string formula = "F<=5 a";
-	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
+	storm::property::ltl::LtlFilter<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser(formula);
+		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
 	);
 
 	ASSERT_NE(ltlFormula, nullptr);
 
-	storm::property::ltl::BoundedEventually<double>* op = static_cast<storm::property::ltl::BoundedEventually<double>*>(ltlFormula);
+	storm::property::ltl::BoundedEventually<double>* op = static_cast<storm::property::ltl::BoundedEventually<double>*>(ltlFormula->getChild());
 	ASSERT_EQ(static_cast<uint_fast64_t>(5), op->getBound());
 
 
@@ -90,14 +90,14 @@ TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) {
 
 TEST(LtlParserTest, parseBoundedUntilFormulaTest) {
 	std::string formula = "a U<=3 b";
-	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
+	storm::property::ltl::LtlFilter<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser(formula);
+		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
 	);
 
 	ASSERT_NE(ltlFormula, nullptr);
 
-	storm::property::ltl::BoundedUntil<double>* op = static_cast<storm::property::ltl::BoundedUntil<double>*>(ltlFormula);
+	storm::property::ltl::BoundedUntil<double>* op = static_cast<storm::property::ltl::BoundedUntil<double>*>(ltlFormula->getChild());
 	ASSERT_EQ(static_cast<uint_fast64_t>(3), op->getBound());
 
 
@@ -108,9 +108,9 @@ TEST(LtlParserTest, parseBoundedUntilFormulaTest) {
 
 TEST(LtlParserTest, parseComplexUntilTest) {
 	std::string formula = "a U b U<=3 c";
-	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
+	storm::property::ltl::LtlFilter<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser(formula);
+		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
 	);
 
 	ASSERT_NE(ltlFormula, nullptr);
@@ -121,9 +121,9 @@ TEST(LtlParserTest, parseComplexUntilTest) {
 
 TEST(LtlParserTest, parseComplexFormulaTest) {
 	std::string formula = "a U F b | G a & F<=3 a U<=7 b // and a comment";
-	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
+	storm::property::ltl::LtlFilter<double>* ltlFormula = nullptr;
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser(formula);
+		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
 	);
 
 	ASSERT_NE(ltlFormula, nullptr);
@@ -134,9 +134,8 @@ TEST(LtlParserTest, parseComplexFormulaTest) {
 
 TEST(LtlParserTest, wrongFormulaTest) {
 	std::string formula = "(a | c) & +";
-	storm::property::ltl::AbstractLtlFormula<double>* ltlFormula = nullptr;
 	ASSERT_THROW(
-		ltlFormula = storm::parser::LtlParser(formula),
+		storm::parser::LtlParser::parseLtlFormula(formula),
 		storm::exceptions::WrongFormatException
 	);
 }