First test case for prctl parser, and some necessary modifications for

the code

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"

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"

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;
 
 }

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;
 };

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>
 

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;
+
+}

test/parser/prctl_files/testFormula.prctl

@@ -0,0 +1 @@
+((P>=0 [ F a ]) & P<0.5 [ G !(b) ])