/*
 * CslParserTest.cpp
 *
 *  Created on: 09.04.2013
 *      Author: Thomas Heinemann
 */

#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/CslParser.h"
#include "src/exceptions/WrongFormatException.h"

namespace csl = storm::property::csl;

TEST(CslParserTest, parseApOnlyTest) {
	std::string input = "ap";
	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
	ASSERT_NO_THROW(
		formula = storm::parser::CslParser::parseCslFormula(input);
	);

	// The parser did not falsely recognize the input as a comment.
	ASSERT_NE(formula.get(), nullptr);

	// The input was parsed correctly.
	ASSERT_EQ(input, formula->toString());
}

TEST(CslParserTest, parsePropositionalFormulaTest) {
	std::string input = "!(a & b) | a & ! c";
	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
	ASSERT_NO_THROW(
		formula = storm::parser::CslParser::parseCslFormula(input);
	);

	// The parser did not falsely recognize the input as a comment.
	ASSERT_NE(formula.get(), nullptr);

	// The input was parsed correctly.
	ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString());
}

TEST(CslParserTest, parseProbabilisticFormulaTest) {
	std::string input = "P > 0.5 [ F a ]";
	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
	ASSERT_NO_THROW(
		formula = storm::parser::CslParser::parseCslFormula(input);
	);

	// The parser did not falsely recognize the input as a comment.
	ASSERT_NE(formula.get(), nullptr);

	auto op = std::dynamic_pointer_cast<storm::property::csl::ProbabilisticBoundOperator<double>>(formula->getChild());
	ASSERT_NE(op.get(), nullptr);
	ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator());
	ASSERT_EQ(0.5, op->getBound());

	// Test the string representation for the parsed formula.
	ASSERT_EQ("P > 0.500000 (F a)", formula->toString());
}

TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
	std::string input = "S >= 15 [ P < 0.2 [ a U<=3 b ] ]";
	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
	ASSERT_NO_THROW(
		formula = storm::parser::CslParser::parseCslFormula(input);
	);

	// The parser did not falsely recognize the input as a comment.
	ASSERT_NE(formula.get(), nullptr);

	auto op = std::dynamic_pointer_cast<storm::property::csl::SteadyStateBoundOperator<double>>(formula->getChild());
	ASSERT_NE(op.get(), nullptr);
	ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator());
	ASSERT_EQ(15.0, op->getBound());

	// Test the string representation for the parsed formula.
	ASSERT_EQ("S >= 15.000000 (P < 0.200000 (a U[0.000000,3.000000] b))", formula->toString());
}

TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) {
	std::string input = "S = ? [ P <= 0.5 [ F<=3 a ] ]";
	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
	ASSERT_NO_THROW(
		formula = storm::parser::CslParser::parseCslFormula(input);
	);

	// The parser did not falsely recognize the input as a comment.
	ASSERT_NE(formula.get(), nullptr);

	// The input was parsed correctly.
	ASSERT_EQ("S = ? (P <= 0.500000 (F[0.000000,3.000000] a))", formula->toString());
}

TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
	std::string input = "P = ? [ a U [3,4] b & (!c) ]";
	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
	ASSERT_NO_THROW(
		formula = storm::parser::CslParser::parseCslFormula(input);
	);

	// The parser did not falsely recognize the input as a comment.
	ASSERT_NE(formula.get(), nullptr);

	// The input was parsed correctly.
	ASSERT_EQ("P = ? (a U[3.000000,4.000000] (b & !c))", formula->toString());
}


TEST(CslParserTest, parseComplexFormulaTest) {
	std::string input = "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] ])  //and a comment";
	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
	ASSERT_NO_THROW(
		formula = storm::parser::CslParser::parseCslFormula(input);
	);

	// The parser did not falsely recognize the input as a comment.
	ASSERT_NE(formula.get(), nullptr);

	// The input was parsed correctly.
	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.000000 (a & b)))))", formula->toString());
}

TEST(CslParserTest, wrongProbabilisticFormulaTest) {
	std::string input = "P > 0.5 [ a ]";
	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
	ASSERT_THROW(
		formula = storm::parser::CslParser::parseCslFormula(input),
		storm::exceptions::WrongFormatException
	);
}

TEST(CslParserTest, wrongFormulaTest) {
	std::string input = "(a | b) & +";
	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
	ASSERT_THROW(
		formula = storm::parser::CslParser::parseCslFormula(input),
		storm::exceptions::WrongFormatException
	);
}

TEST(CslParserTest, wrongFormulaTest2) {
	std::string input = "P>0 [ F & a ]";
	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
	ASSERT_THROW(
		formula = storm::parser::CslParser::parseCslFormula(input),
		storm::exceptions::WrongFormatException
	);
}