diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h
index 6fb771ca5..38c607771 100644
--- a/src/formula/Formulas.h
+++ b/src/formula/Formulas.h
@@ -8,6 +8,8 @@
 #ifndef STORM_FORMULA_FORMULAS_H_
 #define STORM_FORMULA_FORMULAS_H_
 
+#include "modelChecker/ForwardDeclarations.h"
+
 #include "And.h"
 #include "Ap.h"
 #include "BoundedUntil.h"
diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h
index c673bbfaf..c6e71f613 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.h
+++ b/src/modelChecker/DtmcPrctlModelChecker.h
@@ -8,13 +8,9 @@
 #ifndef STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_
 #define STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_
 
-
-
-#include "src/formula/PctlPathFormula.h"
-#include "src/formula/PctlStateFormula.h"
-
 #include "src/formula/Formulas.h"
 #include "src/utility/Vector.h"
+#include "src/storage/SparseMatrix.h"
 
 #include "src/models/Dtmc.h"
 #include "src/storage/BitVector.h"
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index f3f80289a..1c9c85180 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -1,4 +1,3 @@
-#include "src/storage/SparseMatrix.h"
 #include "src/parser/PrctlParser.h"
 #include "src/utility/OsDetection.h"
 #include "src/utility/ConstTemplates.h"
@@ -46,8 +45,12 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::PctlFor
 		atomicProposition = (freeIdentifierName)[qi::_val =
 				phoenix::new_<storm::formula::Ap<double>>(qi::_1)];
 		probabilisticBoundOperator = (
+				("P>" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
+						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER, qi::_1, qi::_2)] |
 				("P>=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
 						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
+				("P<" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
+								phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS, qi::_1, qi::_2)] |
 				("P<=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val =
 						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
 				);
@@ -132,5 +135,6 @@ storm::parser::PrctlParser::PrctlParser(std::string filename) {
 
 	qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer);
 
+	formula = result_pointer;
 
 }
diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h
index 29f16aa18..595946730 100644
--- a/src/parser/PrctlParser.h
+++ b/src/parser/PrctlParser.h
@@ -20,13 +20,13 @@ class PrctlParser : Parser
 		/*!
 		 *	@brief return formula object parsed from file.
 		 */
-		std::shared_ptr<storm::formula::PctlFormula<double>> getFormula()
+		storm::formula::PctlFormula<double>* getFormula()
 		{
 			return this->formula;
 		}
 	
 	private:
-		std::shared_ptr<storm::formula::PctlFormula<double>> formula;
+		storm::formula::PctlFormula<double>* formula;
 		template<typename Iterator, typename Skipper>
 		struct PrctlGrammar;
 };
diff --git a/src/utility/Vector.h b/src/utility/Vector.h
index 0add7457f..a69b87e4a 100644
--- a/src/utility/Vector.h
+++ b/src/utility/Vector.h
@@ -8,7 +8,7 @@
 #ifndef STORM_UTILITY_VECTOR_H_
 #define STORM_UTILITY_VECTOR_H_
 
-#include "Eigen/src/Core/Matrix.h"
+#include "Eigen/Core"
 #include "ConstTemplates.h"
 #include <iostream>
 
diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp
new file mode 100644
index 000000000..bb18aaaad
--- /dev/null
+++ b/test/parser/PrctlParserTest.cpp
@@ -0,0 +1,27 @@
+/*
+ * PrctlParserTest.cpp
+ *
+ *  Created on: 01.02.2013
+ *      Author: Thomas Heinemann
+ */
+
+
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/parser/PrctlParser.h"
+#include <iostream>
+
+TEST(PrctlParserTest, parseAndOutput) {
+	storm::parser::PrctlParser* prctlParser = nullptr;
+	ASSERT_NO_THROW(
+			prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula.prctl")
+	);
+
+	ASSERT_NE(prctlParser->getFormula(), nullptr);
+
+
+	std::cout << prctlParser->getFormula()->toString();
+
+	delete prctlParser;
+
+}
diff --git a/test/parser/prctl_files/testFormula.prctl b/test/parser/prctl_files/testFormula.prctl
new file mode 100644
index 000000000..fd395528e
--- /dev/null
+++ b/test/parser/prctl_files/testFormula.prctl
@@ -0,0 +1 @@
+((P>=0 [ F a ]) & P<0.5 [ G !(b) ])
\ No newline at end of file