Test cases for CSL parser

src/formula/StateBoundOperator.h

@@ -129,7 +129,7 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const {
-		std::string result = "";
+		std::string result = " ";
 		switch (comparisonOperator) {
 		case LESS: result += "< "; break;
 		case LESS_EQUAL: result += "<= "; break;

src/formula/SteadyStateBoundOperator.h

@@ -78,11 +78,7 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const {
-		std::string result = "(";
-		result += " S ";
-		result += StateBoundOperator<T>::toString();
-		result += ")";
-		return result;
+		return "S" + StateBoundOperator<T>::toString();
 	}
 
 	/*!

src/formula/SteadyStateNoBoundOperator.h

@@ -57,11 +57,7 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const {
-		std::string result = "(";
-		result += " S ";
-		result += StateNoBoundOperator<T>::toString();
-		result += ")";
-		return result;
+		return "S" + StateNoBoundOperator<T>::toString();
 	}
 
 	/*!

src/parser/CslParser.cpp

@@ -77,13 +77,13 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFor
 		probabilisticBoundOperator.name("state formula");
 		steadyStateBoundOperator = (
 				(qi::lit("S") >> qi::lit(">") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
-										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
+										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::StateBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
 				(qi::lit("S") >> qi::lit(">=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
-										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
+										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::StateBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
 				(qi::lit("S") >> qi::lit("<") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
-										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS, qi::_1, qi::_2)] |
+										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::StateBoundOperator<double>::LESS, qi::_1, qi::_2)] |
 				(qi::lit("S") > qi::lit("<=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
-										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
+										phoenix::new_<storm::formula::SteadyStateBoundOperator<double> >(storm::formula::StateBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
 				);
 		steadyStateBoundOperator.name("state formula");
 
@@ -102,19 +102,19 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFor
 		pathFormula.name("path formula");
 		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::BoundedEventually<double>>(qi::_2, qi::_1)];
-		boundedEventually.name("path formula (for probablistic operator)");
+		boundedEventually.name("path formula (for probabilistic operator)");
 		eventually = (qi::lit("F") > stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Eventually<double> >(qi::_1)];
-		eventually.name("path formula (for probablistic operator)");
+		eventually.name("path formula (for probabilistic operator)");
 		globally = (qi::lit("G") > stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Globally<double> >(qi::_1)];
-		globally.name("path formula (for probablistic operator)");
+		globally.name("path formula (for probabilistic operator)");
 		boundedUntil = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)
 				[qi::_val = phoenix::new_<storm::formula::BoundedUntil<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_3, qi::_2)];
-		boundedUntil.name("path formula (for probablistic operator)");
+		boundedUntil.name("path formula (for probabilistic operator)");
 		until = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Until<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
-		until.name("path formula (for probablistic operator)");
+		until.name("path formula (for probabilistic operator)");
 
 		start = (noBoundOperator | stateFormula);
 		start.name("CSL formula");
@@ -156,12 +156,61 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFor
 };
 
 CslParser::CslParser(std::string formulaString) {
-	// TODO Auto-generated constructor stub
+	// Prepare iterators to input.
+	BaseIteratorType stringIteratorBegin = formulaString.begin();
+	BaseIteratorType stringIteratorEnd = formulaString.end();
+	PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString);
+	PositionIteratorType positionIteratorEnd;
+
+
+	// Prepare resulting intermediate representation of input.
+	storm::formula::AbstractFormula<double>* result_pointer = nullptr;
+
+	CslGrammar<PositionIteratorType,  BOOST_TYPEOF(boost::spirit::ascii::space)> grammar;
+
+	// Now, parse the formula from the given string
+	try {
+		qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer);
+	} catch(const qi::expectation_failure<PositionIteratorType>& e) {
+		// If the parser expected content different than the one provided, display information
+		// about the location of the error.
+		const boost::spirit::classic::file_position_base<std::string>& pos = e.first.get_position();
+
+		// Construct the error message including a caret display of the position in the
+		// erroneous line.
+		std::stringstream msg;
+		msg << pos.file << ", line " << pos.line << ", column " << pos.column
+				<< ": parse error: expected " << e.what_ << std::endl << "\t"
+				<< e.first.get_currentline() << std::endl << "\t";
+		int i = 0;
+		for (i = 0; i < pos.column; ++i) {
+			msg << "-";
+		}
+		msg << "^";
+		for (; i < 80; ++i) {
+			msg << "-";
+		}
+		msg << std::endl;
+
+		std::cerr << msg.str();
+
+		// Now propagate exception.
+		throw storm::exceptions::WrongFormatException() << msg.str();
+	}
+
+	// The syntax can be so wrong that no rule can be matched at all
+	// In that case, no expectation failure is thrown, but the parser just returns nullptr
+	// Then, of course the result is not usable, hence we throw a WrongFormatException, too.
+	if (result_pointer == nullptr) {
+		throw storm::exceptions::WrongFormatException() << "Syntax error in formula";
+	}
 
+	formula = result_pointer;
 }
 
 CslParser::~CslParser() {
-	// TODO Auto-generated destructor stub
+	// Intentionally left empty
+	// Parsed formula is not deleted with the parser!
 }
 
 } /* namespace parser */

test/parser/CslParserTest.cpp

@@ -0,0 +1,158 @@
+/*
+ * CslParserTest.cpp
+ *
+ *  Created on: 09.04.2013
+ *      Author: Thomas Heinemann
+ */
+
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/parser/CslParser.h"
+
+TEST(CslParserTest, parseApOnlyTest) {
+	std::string ap = "ap";
+	storm::parser::CslParser* cslParser = nullptr;
+	ASSERT_NO_THROW(
+			cslParser = new storm::parser::CslParser(ap);
+	);
+
+	ASSERT_NE(cslParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(ap, cslParser->getFormula()->toString());
+
+	delete cslParser->getFormula();
+	delete cslParser;
+
+}
+
+TEST(CslParserTest, parsePropositionalFormulaTest) {
+	storm::parser::CslParser* cslParser = nullptr;
+	ASSERT_NO_THROW(
+			cslParser = new storm::parser::CslParser("!(a & b) | a & ! c")
+	);
+
+	ASSERT_NE(cslParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(cslParser->getFormula()->toString(), "(!(a & b) | (a & !c))");
+
+	delete cslParser->getFormula();
+	delete cslParser;
+
+}
+
+TEST(CslParserTest, parseProbabilisticFormulaTest) {
+	storm::parser::CslParser* cslParser = nullptr;
+	ASSERT_NO_THROW(
+			cslParser = new storm::parser::CslParser("P > 0.5 [ F a ]")
+	);
+
+	ASSERT_NE(cslParser->getFormula(), nullptr);
+
+	storm::formula::ProbabilisticBoundOperator<double>* op = static_cast<storm::formula::ProbabilisticBoundOperator<double>*>(cslParser->getFormula());
+
+	ASSERT_EQ(storm::formula::PathBoundOperator<double>::GREATER, op->getComparisonOperator());
+	ASSERT_EQ(0.5, op->getBound());
+
+	ASSERT_EQ(cslParser->getFormula()->toString(), "P > 0.500000 [F a]");
+
+	delete cslParser->getFormula();
+	delete cslParser;
+
+}
+
+TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
+	storm::parser::CslParser* cslParser = nullptr;
+	ASSERT_NO_THROW(
+			cslParser = new storm::parser::CslParser("S >= 15 [ a & b ]")
+	);
+
+	ASSERT_NE(cslParser->getFormula(), nullptr);
+
+	storm::formula::SteadyStateBoundOperator<double>* op = static_cast<storm::formula::SteadyStateBoundOperator<double>*>(cslParser->getFormula());
+
+	ASSERT_EQ(storm::formula::StateBoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
+	ASSERT_EQ(15.0, op->getBound());
+
+	ASSERT_EQ("S >= 15.000000 [(a & b)]", cslParser->getFormula()->toString());
+
+	delete cslParser->getFormula();
+	delete cslParser;
+}
+
+TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) {
+	storm::parser::CslParser* cslParser = nullptr;
+	ASSERT_NO_THROW(
+			cslParser = new storm::parser::CslParser("S = ? [ P <= 0.5 [ F a ] ]")
+	);
+
+	ASSERT_NE(cslParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(cslParser->getFormula()->toString(), "S = ? [P <= 0.500000 [F a]]");
+
+	delete cslParser->getFormula();
+	delete cslParser;
+
+}
+
+TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
+	storm::parser::CslParser* cslParser = nullptr;
+	ASSERT_NO_THROW(
+			cslParser = new storm::parser::CslParser("P = ? [ a U <= 4 b & (!c) ]")
+	);
+
+	ASSERT_NE(cslParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ(cslParser->getFormula()->toString(), "P = ? [a U<=4 (b & !c)]");
+
+	delete cslParser->getFormula();
+	delete cslParser;
+
+}
+
+TEST(CslParserTest, parseComplexFormulaTest) {
+	storm::parser::CslParser* cslParser = nullptr;
+	ASSERT_NO_THROW(
+			cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])")
+	);
+
+	ASSERT_NE(cslParser->getFormula(), nullptr);
+
+
+	ASSERT_EQ("(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F<=7 (a & b)]]))", cslParser->getFormula()->toString());
+	delete cslParser->getFormula();
+	delete cslParser;
+
+}
+
+
+TEST(CslParserTest, wrongProbabilisticFormulaTest) {
+	storm::parser::CslParser* cslParser = nullptr;
+	ASSERT_THROW(
+			cslParser = new storm::parser::CslParser("P > 0.5 [ a ]"),
+			storm::exceptions::WrongFormatException
+	);
+
+	delete cslParser;
+}
+
+TEST(CslParserTest, wrongFormulaTest) {
+	storm::parser::CslParser* cslParser = nullptr;
+	ASSERT_THROW(
+			cslParser = new storm::parser::CslParser("(a | b) & +"),
+			storm::exceptions::WrongFormatException
+	);
+	delete cslParser;
+}
+
+TEST(CslParserTest, wrongFormulaTest2) {
+	storm::parser::CslParser* cslParser = nullptr;
+	ASSERT_THROW(
+			cslParser = new storm::parser::CslParser("P>0 [ F & a ]"),
+			storm::exceptions::WrongFormatException
+	);
+	delete cslParser;
+}