Some improvements/corrections to the LTL parser and some test cases for

it

src/formula/Ltl/BoundedUntil.h

@@ -88,6 +88,18 @@ public:
 	  //intentionally left empty
 	}
 
+	/*!
+	 *	@brief Return string representation of this formula.
+	 *
+	 * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
+	 * root of a path formula); hence this function is overwritten in this class.
+	 *
+	 * @return A string representation of the formula.
+	 */
+	virtual std::string toString() const {
+		return "(" + storm::formula::abstract::BoundedUntil<T, AbstractLtlFormula<T>>::toString() + ")";
+	}
+
 	/*!
 	 * Clones the called object.
 	 *

src/formula/Ltl/Until.h

@@ -84,6 +84,18 @@ public:
 	  // Intentionally left empty
 	}
 
+	/*!
+	 *	@brief Return string representation of this formula.
+	 *
+	 * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
+	 * root of a path formula); hence this function is overwritten in this class.
+	 *
+	 * @return A string representation of the formula.
+	 */
+	virtual std::string toString() const {
+		return "(" + storm::formula::abstract::Until<T, AbstractLtlFormula<T>>::toString() + ")";
+	}
+
 	/*!
 	 * Clones the called object.
 	 *

src/formula/abstract/AbstractFormula.h

@@ -62,7 +62,7 @@ public:
 	/*!
 	 *	@brief Return string representation of this formula.
 	 *
-	 *	@note very subclass must implement this method.
+	 *	@note every subclass must implement this method.
 	 *
 	 *	@returns a string representation of the formula
 	 */

src/parser/LtlParser.cpp

@@ -51,9 +51,12 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::formula::ltl::Abstra
 		orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::Or<double>>(qi::_val, qi::_1)];
 		orFormula.name("state formula");
-		andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val =
+		andFormula = untilFormula[qi::_val = qi::_1] > *(qi::lit("&") > untilFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::And<double>>(qi::_val, qi::_1)];
 		andFormula.name("state formula");
+		untilFormula = notFormula[qi::_val = qi::_1] >
+				*((qi::lit("U") >> qi::lit("<=") > qi::int_ > notFormula)[qi::_val = phoenix::new_<storm::formula::ltl::BoundedUntil<double>>(qi::_val, qi::_2, qi::_1)] |
+				  (qi::lit("U") > notFormula)[qi::_val = phoenix::new_<storm::formula::ltl::Until<double>>(qi::_val, qi::_1)]);
 		notFormula = atomicLtlFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicLtlFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::Not<double>>(qi::_1)];
 		notFormula.name("state formula");
@@ -85,7 +88,7 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::formula::ltl::Abstra
 		probabilisticNoBoundOperator.name("no bound operator");*/
 
 		//This block defines rules for parsing probabilistic path formulas
-		pathFormula = (boundedEventually | eventually | globally | boundedUntil | until);
+		pathFormula = (boundedEventually | eventually | globally);//(boundedEventually | eventually | globally | boundedUntil | until);
 		pathFormula.name("ltl formula");
 		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::BoundedEventually<double>>(qi::_2, qi::_1)];
@@ -96,12 +99,6 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::formula::ltl::Abstra
 		globally = (qi::lit("G") > ltlFormula)[qi::_val =
 				phoenix::new_<storm::formula::ltl::Globally<double> >(qi::_1)];
 		globally.name("ltl formula");
-		boundedUntil = (ltlFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::ltl::AbstractLtlFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > ltlFormula)
-				[qi::_val = phoenix::new_<storm::formula::ltl::BoundedUntil<double>>(phoenix::bind(&storm::formula::ltl::AbstractLtlFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::ltl::AbstractLtlFormula<double>>::get, qi::_a)), qi::_3, qi::_2)];
-		boundedUntil.name("ltl formula");
-		until = (ltlFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::ltl::AbstractLtlFormula<double>>>(qi::_1)] >> qi::lit("U") > ltlFormula)[qi::_val =
-				phoenix::new_<storm::formula::ltl::Until<double>>(phoenix::bind(&storm::formula::ltl::AbstractLtlFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::ltl::AbstractLtlFormula<double>>::get, qi::_a)), qi::_2)];
-		until.name("ltl formula");
 
 		start = ltlFormula;
 		start.name("LTL formula");
@@ -113,6 +110,7 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::formula::ltl::Abstra
 	qi::rule<Iterator, storm::formula::ltl::AbstractLtlFormula<double>*(), Skipper> atomicLtlFormula;
 
 	qi::rule<Iterator, storm::formula::ltl::AbstractLtlFormula<double>*(), Skipper> andFormula;
+	qi::rule<Iterator, storm::formula::ltl::AbstractLtlFormula<double>*(), Skipper> untilFormula;
 	qi::rule<Iterator, storm::formula::ltl::AbstractLtlFormula<double>*(), Skipper> atomicProposition;
 	qi::rule<Iterator, storm::formula::ltl::AbstractLtlFormula<double>*(), Skipper> orFormula;
 	qi::rule<Iterator, storm::formula::ltl::AbstractLtlFormula<double>*(), Skipper> notFormula;
@@ -125,8 +123,8 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::formula::ltl::Abstra
 	qi::rule<Iterator, storm::formula::ltl::BoundedEventually<double>*(), Skipper> boundedEventually;
 	qi::rule<Iterator, storm::formula::ltl::Eventually<double>*(), Skipper> eventually;
 	qi::rule<Iterator, storm::formula::ltl::Globally<double>*(), Skipper> globally;
-	qi::rule<Iterator, storm::formula::ltl::BoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::formula::ltl::AbstractLtlFormula<double>>>, Skipper> boundedUntil;
-	qi::rule<Iterator, storm::formula::ltl::Until<double>*(), qi::locals< std::shared_ptr<storm::formula::ltl::AbstractLtlFormula<double>>>, Skipper> until;
+	qi::rule<Iterator, storm::formula::ltl::AbstractLtlFormula<double>*(), qi::locals< std::shared_ptr<storm::formula::ltl::AbstractLtlFormula<double>>>, Skipper> boundedUntil;
+	qi::rule<Iterator, storm::formula::ltl::AbstractLtlFormula<double>*(), qi::locals< std::shared_ptr<storm::formula::ltl::AbstractLtlFormula<double>>>, Skipper> until;
 
 	qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
 

test/parser/CslParserTest.cpp

@@ -94,7 +94,6 @@ TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) {
 
 	delete cslParser->getFormula();
 	delete cslParser;
-
 }
 
 TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {

test/parser/LtlParserTest.cpp

@@ -0,0 +1,107 @@
+/*
+ * LtlParserTest.cpp
+ *
+ *  Created on: 22.04.2013
+ *      Author: thomas
+ */
+
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/parser/LtlParser.h"
+
+TEST(LtlParserTest, parseApOnlyTest) {
+	std::string ap = "ap";
+	storm::parser::LtlParser* ltlParser = nullptr;
+	ASSERT_NO_THROW(
+			ltlParser = new storm::parser::LtlParser(ap);
+	);
+
+	ASSERT_NE(ltlParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(ltlParser->getFormula()->toString(), ap);
+
+	delete ltlParser->getFormula();
+	delete ltlParser;
+}
+
+TEST(LtlParserTest, parsePropositionalFormulaTest) {
+	storm::parser::LtlParser* ltlParser = nullptr;
+	ASSERT_NO_THROW(
+			ltlParser = new storm::parser::LtlParser("!(a & b) | a & ! c")
+	);
+
+	ASSERT_NE(ltlParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(ltlParser->getFormula()->toString(), "(!(a & b) | (a & !c))");
+
+	delete ltlParser->getFormula();
+	delete ltlParser;
+}
+
+TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) {
+	storm::parser::LtlParser* ltlParser = nullptr;
+	ASSERT_NO_THROW(
+			ltlParser = new storm::parser::LtlParser("F<=5 a")
+	);
+
+	ASSERT_NE(ltlParser->getFormula(), nullptr);
+
+	storm::formula::ltl::BoundedEventually<double>* op = static_cast<storm::formula::ltl::BoundedEventually<double>*>(ltlParser->getFormula());
+
+	ASSERT_EQ(static_cast<uint_fast64_t>(5), op->getBound());
+
+	ASSERT_EQ(ltlParser->getFormula()->toString(), "F<=5 a");
+
+	delete ltlParser->getFormula();
+	delete ltlParser;
+}
+
+TEST(LtlParserTest, parseBoundedUntilFormulaTest) {
+	storm::parser::LtlParser* ltlParser = nullptr;
+	ASSERT_NO_THROW(
+			ltlParser = new storm::parser::LtlParser("a U<=3 b")
+	);
+
+	ASSERT_NE(ltlParser->getFormula(), nullptr);
+
+	storm::formula::ltl::BoundedUntil<double>* op = static_cast<storm::formula::ltl::BoundedUntil<double>*>(ltlParser->getFormula());
+
+	ASSERT_EQ(static_cast<uint_fast64_t>(3), op->getBound());
+
+	ASSERT_EQ("(a U<=3 b)", ltlParser->getFormula()->toString());
+
+	delete ltlParser->getFormula();
+	delete ltlParser;
+}
+
+TEST(LtlParserTest, parseComplexUntilTest) {
+	storm::parser::LtlParser* ltlParser = nullptr;
+	ASSERT_NO_THROW(
+			ltlParser = new storm::parser::LtlParser("a U b U<=3 c")
+	);
+
+	ASSERT_NE(ltlParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(ltlParser->getFormula()->toString(), "((a U b) U<=3 c)");
+
+	delete ltlParser->getFormula();
+	delete ltlParser;
+}
+
+TEST(LtlParserTest, parseComplexFormulaTest) {
+	storm::parser::LtlParser* ltlParser = nullptr;
+	ASSERT_NO_THROW(
+			ltlParser = new storm::parser::LtlParser("a U F b | G a & F<=3 a U<=7 b")
+	);
+
+	ASSERT_NE(ltlParser->getFormula(), nullptr);
+
+	ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", ltlParser->getFormula()->toString());
+	delete ltlParser->getFormula();
+	delete ltlParser;
+
+}
+