Added function to test if a formula is a probability bounded reachability formula, i.e. conforms to the pattern P[<,<=,>,>=]p ([phi U, E] psi) where phi, psi are propositional formulas (consisting only of And, Or, Not and AP).

- For that implemented function that checks if a formula is a propositional logic formula to all three logics.
- Added tests for the function.
- Added documentation for the function.


Former-commit-id: 3fcb84b990

src/formula/AbstractFormula.h

@@ -79,6 +79,16 @@ public:
 	 *	@return true iff all subtrees are valid.
 	 */
 	virtual bool validate(AbstractFormulaChecker<T> const & checker) const = 0;
+
+	/*!
+	 * Returns whether the formula is a propositional logic formula.
+	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 * @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const {
+		return false;
+	}
 };
 
 } // namespace property

src/formula/PrctlFormulaChecker.h

@@ -23,7 +23,7 @@ class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
 		 *	Implementation of AbstractFormulaChecker::validate() using code
 		 *	looking exactly like the sample code given there.
 		 */
-		virtual bool validate(std::shared_ptr<storm::property::abstract::AbstractFormula<T>> const & formula) const {
+		virtual bool validate(std::shared_ptr<storm::property::AbstractFormula<T>> const & formula) const {
 			// What to support: Principles of Model Checking Def. 10.76 + syntactic sugar
 			if (
 					dynamic_pointer_cast<storm::property::prctl::And<T>>(formula) ||

src/formula/csl/AbstractCslFormula.h

@@ -14,6 +14,18 @@ namespace storm {
 namespace property {
 namespace csl {
 
+template <class T> class ProbabilisticBoundOperator;
+template <class T> class Eventually;
+template <class T> class Until;
+
+}
+}
+}
+
+namespace storm {
+namespace property {
+namespace csl {
+
 /*!
  * Abstract base class for all CSL root formulas.
  */
@@ -23,6 +35,37 @@ public:
 	virtual ~AbstractCslFormula() {
 		// Intentionally left empty
 	}
+
+	/*!
+	 * Checks whether the formula is a probabilistic bound reachability formula.
+	 * Returns true iff the formula conforms to the following pattern.
+	 * Pattern: P[<,<=,>,>=]p ([psi U, E] phi) whith psi, phi propositional logic formulas (consisiting only of And, Or, Not and AP).
+	 * That is, a probabilistic bound operator as root with a single until or eventually formula directly below it, whose subformulas are propositional
+	 * (denoting some set of atomic propositions).
+	 *
+	 * @return True iff this is a probabilistic bound reachability formula.
+	 */
+	bool isProbEventuallyAP() const {
+
+		if(dynamic_cast<storm::property::csl::ProbabilisticBoundOperator<T> const *>(this) == nullptr) {
+			return false;
+		}
+
+		auto probFormula = dynamic_cast<storm::property::csl::ProbabilisticBoundOperator<T> const *>(this);
+
+		if(std::dynamic_pointer_cast<storm::property::csl::Eventually<T>>(probFormula->getChild()).get() != nullptr) {
+
+			auto eventuallyFormula = std::dynamic_pointer_cast<storm::property::csl::Eventually<T>>(probFormula->getChild());
+			return eventuallyFormula->getChild()->isPropositional();
+		}
+		else if(std::dynamic_pointer_cast<storm::property::csl::Until<T>>(probFormula->getChild()).get() != nullptr) {
+
+			auto untilFormula = std::dynamic_pointer_cast<storm::property::csl::Until<T>>(probFormula->getChild());
+			return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional();
+		}
+
+		return false;
+	}
 };
 
 } /* namespace csl */

src/formula/csl/And.h

@@ -139,6 +139,15 @@ public:
 		return checker.validate(this->left) && checker.validate(this->right);
 	}
 
+	/*! Returns whether the formula is a propositional logic formula.
+	 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 *  @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return left->isPropositional() && right->isPropositional();
+	}
+
 	/*!
 	 * Sets the left child node.
 	 *

src/formula/csl/Ap.h

@@ -106,6 +106,15 @@ public:
 		return true;
 	}
 
+	/*! Returns whether the formula is a propositional logic formula.
+	 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 *  @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return true;
+	}
+
 	/*!
 	 * @returns the name of the atomic proposition
 	 */

src/formula/csl/Not.h

@@ -125,6 +125,15 @@ public:
 		return checker.validate(this->child);
 	}
 
+	/*! Returns whether the formula is a propositional logic formula.
+	 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 *  @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return child->isPropositional();
+	}
+
 	/*!
 	 * @returns The child node
 	 */

src/formula/csl/Or.h

@@ -137,6 +137,15 @@ public:
 		return checker.validate(this->left) && checker.validate(this->right);
 	}
 
+	/*! Returns whether the formula is a propositional logic formula.
+	 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 *  @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return left->isPropositional() && right->isPropositional();
+	}
+
 	/*!
 	 * Sets the left child node.
 	 *

src/formula/ltl/And.h

@@ -138,6 +138,15 @@ public:
         return checker.validate(this->left) && checker.validate(this->right);
     }
 
+	/*!
+	 * Returns whether the formula is a propositional logic formula.
+	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 * @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return left->isPropositional() && right->isPropositional();
+	}
 
 	/*!
 	 * Sets the left child node.

src/formula/ltl/Ap.h

@@ -118,6 +118,16 @@ public:
 		return true;
 	}
 
+	/*!
+	 * Returns whether the formula is a propositional logic formula.
+	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 * @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return true;
+	}
+
 	/*!
 	 * @returns the name of the atomic proposition
 	 */

src/formula/ltl/Not.h

@@ -123,6 +123,16 @@ public:
 		return checker.validate(this->child);
 	}
 
+	/*!
+	 * Returns whether the formula is a propositional logic formula.
+	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 * @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return child->isPropositional();
+	}
+
 	/*!
 	 * @returns The child node
 	 */

src/formula/ltl/Or.h

@@ -135,6 +135,16 @@ public:
 		return checker.validate(this->left) && checker.validate(this->right);
 	}
 
+	/*!
+	 * Returns whether the formula is a propositional logic formula.
+	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 * @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return left->isPropositional() && right->isPropositional();
+	}
+
 	/*!
 	 * Sets the left child node.
 	 *

src/formula/prctl/AbstractPrctlFormula.h

@@ -14,6 +14,18 @@ namespace storm {
 namespace property {
 namespace prctl {
 
+template <class T> class ProbabilisticBoundOperator;
+template <class T> class Eventually;
+template <class T> class Until;
+
+}
+}
+}
+
+namespace storm {
+namespace property {
+namespace prctl {
+
 /*!
  * Interface class for all PRCTL root formulas.
  */
@@ -23,6 +35,36 @@ public:
 	virtual ~AbstractPrctlFormula() {
 		// Intentionally left empty
 	}
+
+	/*! Returns whether the formula is a probabilistic bound reachability formula.
+	 *  Returns true iff the formula conforms to the following pattern.
+	 *  Pattern: P[<,<=,>,>=]p ([psi U, E] phi) whith psi, phi propositional logic formulas (consisiting only of And, Or, Not and AP).
+	 *  That is, a probabilistic bound operator as root with a single until or eventually formula directly below it, whose subformulas are propositional
+	 *  (denoting some set of atomic propositions).
+	 *
+	 *  @return True iff this is a probabilistic bound reachability formula.
+	 */
+	bool isProbEventuallyAP() const {
+
+		if(dynamic_cast<storm::property::prctl::ProbabilisticBoundOperator<T> const *>(this) == nullptr) {
+			return false;
+		}
+
+		auto probFormula = dynamic_cast<storm::property::prctl::ProbabilisticBoundOperator<T> const *>(this);
+
+		if(std::dynamic_pointer_cast<storm::property::prctl::Eventually<T>>(probFormula->getChild()).get() != nullptr) {
+
+			auto eventuallyFormula = std::dynamic_pointer_cast<storm::property::prctl::Eventually<T>>(probFormula->getChild());
+			return eventuallyFormula->getChild()->isPropositional();
+		}
+		else if(std::dynamic_pointer_cast<storm::property::prctl::Until<T>>(probFormula->getChild()).get() != nullptr) {
+
+			auto untilFormula = std::dynamic_pointer_cast<storm::property::prctl::Until<T>>(probFormula->getChild());
+			return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional();
+		}
+
+		return false;
+	}
 };
 
 } /* namespace prctl */

src/formula/prctl/And.h

@@ -139,6 +139,16 @@ public:
 		return checker.validate(this->left) && checker.validate(this->right);
 	}
 
+	/*!
+	 * Returns whether the formula is a propositional logic formula.
+	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 * @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return left->isPropositional() && right->isPropositional();
+	}
+
 	/*!
 	 * Sets the left child node.
 	 *

src/formula/prctl/Ap.h

@@ -106,6 +106,16 @@ public:
 		return true;
 	}
 
+	/*!
+	 * Returns whether the formula is a propositional logic formula.
+	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 * @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return true;
+	}
+
 	/*!
 	 * @returns the name of the atomic proposition
 	 */

src/formula/prctl/Not.h

@@ -124,6 +124,17 @@ public:
 		return checker.validate(this->child);
 	}
 
+
+	/*!
+	 * Returns whether the formula is a propositional logic formula.
+	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 * @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return child->isPropositional();
+	}
+
 	/*!
 	 * @returns The child node
 	 */

src/formula/prctl/Or.h

@@ -136,6 +136,16 @@ public:
         return checker.validate(this->left) && checker.validate(this->right);
     }
 
+	/*!
+	 * Returns whether the formula is a propositional logic formula.
+	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
+	 *
+	 * @return True iff this is a propositional logic formula.
+	 */
+	virtual bool isPropositional() const override {
+		return left->isPropositional() && right->isPropositional();
+	}
+
 	/*!
 	 * Sets the left child node.
 	 *

test/functional/parser/CslParserTest.cpp

@@ -27,6 +27,9 @@ TEST(CslParserTest, parseApOnlyTest) {
 	// The parser did not falsely recognize the input as a comment.
 	ASSERT_NE(formula.get(), nullptr);
 
+	ASSERT_TRUE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
+
 	// The input was parsed correctly.
 	ASSERT_EQ(input, formula->toString());
 }
@@ -41,6 +44,9 @@ TEST(CslParserTest, parsePropositionalFormulaTest) {
 	// The parser did not falsely recognize the input as a comment.
 	ASSERT_NE(formula.get(), nullptr);
 
+	ASSERT_TRUE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
+
 	// The input was parsed correctly.
 	ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString());
 }
@@ -58,16 +64,25 @@ TEST(CslParserTest, parsePathFormulaTest) {
 	// The input was parsed correctly.
 	ASSERT_NE(std::dynamic_pointer_cast<csl::Next<double>>(formula->getChild()).get(), nullptr);
 	auto nextFormula = std::dynamic_pointer_cast<csl::Next<double>>(formula->getChild());
+	ASSERT_FALSE(nextFormula->isPropositional());
+	ASSERT_FALSE(nextFormula->isProbEventuallyAP());
+
 	ASSERT_NE(std::dynamic_pointer_cast<csl::ProbabilisticBoundOperator<double>>(nextFormula->getChild()).get(), nullptr);
 	auto probBoundFormula = std::dynamic_pointer_cast<csl::ProbabilisticBoundOperator<double>>(nextFormula->getChild());
+	ASSERT_EQ(0.9, probBoundFormula->getBound());
+	ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator());
+	ASSERT_FALSE(probBoundFormula->isPropositional());
+	ASSERT_TRUE(probBoundFormula->isProbEventuallyAP());
+
 	ASSERT_NE(std::dynamic_pointer_cast<csl::Until<double>>(probBoundFormula->getChild()).get(), nullptr);
 	auto untilFormula = std::dynamic_pointer_cast<csl::Until<double>>(probBoundFormula->getChild());
+	ASSERT_FALSE(untilFormula->isPropositional());
+	ASSERT_FALSE(untilFormula->isProbEventuallyAP());
+
 	ASSERT_NE(std::dynamic_pointer_cast<csl::Ap<double>>(untilFormula->getLeft()).get(), nullptr);
 	ASSERT_NE(std::dynamic_pointer_cast<csl::Ap<double>>(untilFormula->getRight()).get(), nullptr);
 	ASSERT_EQ("a", std::dynamic_pointer_cast<csl::Ap<double>>(untilFormula->getLeft())->getAp());
 	ASSERT_EQ("b", std::dynamic_pointer_cast<csl::Ap<double>>(untilFormula->getRight())->getAp());
-	ASSERT_EQ(0.9, probBoundFormula->getBound());
-	ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator());
 
 
 	// The string representation is also correct.
@@ -88,6 +103,8 @@ TEST(CslParserTest, parseProbabilisticFormulaTest) {
 	ASSERT_NE(op.get(), nullptr);
 	ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator());
 	ASSERT_EQ(0.5, op->getBound());
+	ASSERT_FALSE(op->isPropositional());
+	ASSERT_TRUE(op->isProbEventuallyAP());
 
 	// Test the string representation for the parsed formula.
 	ASSERT_EQ("P > 0.500000 (F a)", formula->toString());
@@ -107,6 +124,8 @@ TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
 	ASSERT_NE(op.get(), nullptr);
 	ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator());
 	ASSERT_EQ(15.0, op->getBound());
+	ASSERT_FALSE(op->isPropositional());
+	ASSERT_FALSE(op->isProbEventuallyAP());
 
 	// 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());
@@ -122,6 +141,9 @@ TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) {
 	// The parser did not falsely recognize the input as a comment.
 	ASSERT_NE(formula.get(), nullptr);
 
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
+
 	// The input was parsed correctly.
 	ASSERT_EQ("S = ? (P <= 0.500000 (F[0.000000,3.000000] a))", formula->toString());
 }
@@ -136,6 +158,9 @@ TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
 	// The parser did not falsely recognize the input as a comment.
 	ASSERT_NE(formula.get(), nullptr);
 
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
+
 	// The input was parsed correctly.
 	ASSERT_EQ("P = ? (a U[3.000000,4.000000] (b & !c))", formula->toString());
 }
@@ -151,6 +176,9 @@ TEST(CslParserTest, parseComplexFormulaTest) {
 	// The parser did not falsely recognize the input as a comment.
 	ASSERT_NE(formula.get(), nullptr);
 
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
+
 	// 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());
 }
@@ -174,12 +202,15 @@ TEST(CslParserTest, parseCslFilterTest) {
 	ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::SortAction<double>>(formula->getAction(3)).get(), nullptr);
 	ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::RangeAction<double>>(formula->getAction(4)).get(), nullptr);
 
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
+
 	// The input was parsed correctly.
 	ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString());
 }
 
 TEST(CslParserTest, commentTest) {
-	std::string input = "// This is a comment. And this is a commented out formula: P = ? [ F a ]";
+	std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ X a ]";
 	std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
 	ASSERT_NO_THROW(
 				formula = storm::parser::CslParser::parseCslFormula(input)
@@ -189,11 +220,15 @@ TEST(CslParserTest, commentTest) {
 	ASSERT_NE(nullptr, formula.get());
 
 	// Test if the parser recognizes the comment at the end of a line.
-	input = "P = ? [ F a ] // This is a comment.";
+	input = "P<=0.5 [ X a ] // This is a comment.";
 	ASSERT_NO_THROW(
 				formula = storm::parser::CslParser::parseCslFormula(input)
 	);
-	ASSERT_EQ("P = ? (F a)", formula->toString());
+
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
+
+	ASSERT_EQ("P <= 0.500000 (X a)", formula->toString());
 }
 
 TEST(CslParserTest, wrongProbabilisticFormulaTest) {

test/functional/parser/LtlParserTest.cpp

@@ -17,25 +17,29 @@
 namespace ltl = storm::property::ltl;
 
 TEST(LtlParserTest, parseApOnlyTest) {
-	std::string formula = "ap";
-	std::shared_ptr<storm::property::ltl::LtlFilter<double>> ltlFormula(nullptr);
+	std::string input = "ap";
+	std::shared_ptr<storm::property::ltl::LtlFilter<double>> formula(nullptr);
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
+		formula = storm::parser::LtlParser::parseLtlFormula(input);
 	);
 
-	ASSERT_NE(ltlFormula.get(), nullptr);
-	ASSERT_EQ(formula, ltlFormula->toString());
+	ASSERT_TRUE(formula->getChild()->isPropositional());
+
+	ASSERT_NE(formula.get(), nullptr);
+	ASSERT_EQ(input, formula->toString());
 }
 
 TEST(LtlParserTest, parsePropositionalFormulaTest) {
-	std::string formula = "!(a & b) | a & ! c";
-	std::shared_ptr<ltl::LtlFilter<double>> ltlFormula(nullptr);
+	std::string input = "!(a & b) | a & ! c";
+	std::shared_ptr<ltl::LtlFilter<double>> formula(nullptr);
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
+		formula = storm::parser::LtlParser::parseLtlFormula(input);
 	);
 
-	ASSERT_NE(ltlFormula.get(), nullptr);
-	ASSERT_EQ("(!(a & b) | (a & !c))", ltlFormula->toString());
+	ASSERT_TRUE(formula->getChild()->isPropositional());
+
+	ASSERT_NE(formula.get(), nullptr);
+	ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString());
 }
 
 /*!
@@ -43,14 +47,16 @@ TEST(LtlParserTest, parsePropositionalFormulaTest) {
  * "Eventually" operator.
  */
 TEST(LtlParserTest, parseAmbiguousFormulaTest) {
-	std::string formula = "F & b";
-	std::shared_ptr<ltl::LtlFilter<double>> ltlFormula(nullptr);
+	std::string input = "F & b";
+	std::shared_ptr<ltl::LtlFilter<double>> formula(nullptr);
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
+		formula = storm::parser::LtlParser::parseLtlFormula(input);
 	);
 
-	ASSERT_NE(ltlFormula.get(), nullptr);
-	ASSERT_EQ("(F & b)", ltlFormula->toString());
+	ASSERT_TRUE(formula->getChild()->isPropositional());
+
+	ASSERT_NE(formula.get(), nullptr);
+	ASSERT_EQ("(F & b)", formula->toString());
 }
 
 /*!
@@ -58,48 +64,54 @@ TEST(LtlParserTest, parseAmbiguousFormulaTest) {
  * depending where it occurs.
  */
 TEST(LtlParserTest, parseAmbiguousFormulaTest2) {
-	std::string formula = "F F";
-	std::shared_ptr<ltl::LtlFilter<double>> ltlFormula(nullptr);
+	std::string input = "F F";
+	std::shared_ptr<ltl::LtlFilter<double>> formula(nullptr);
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
+		formula = storm::parser::LtlParser::parseLtlFormula(input);
 	);
 
-	ASSERT_NE(ltlFormula.get(), nullptr);
-	ASSERT_EQ("F F", ltlFormula->toString());
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+
+	ASSERT_NE(formula.get(), nullptr);
+	ASSERT_EQ("F F", formula->toString());
 }
 
 TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) {
-	std::string formula = "F<=5 a";
-	std::shared_ptr<ltl::LtlFilter<double>> ltlFormula(nullptr);
+	std::string input = "F<=5 a";
+	std::shared_ptr<ltl::LtlFilter<double>> formula(nullptr);
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
+		formula = storm::parser::LtlParser::parseLtlFormula(input);
 	);
 
-	ASSERT_NE(ltlFormula.get(), nullptr);
+	ASSERT_NE(formula.get(), nullptr);
 
-	std::shared_ptr<storm::property::ltl::BoundedEventually<double>> op = std::dynamic_pointer_cast<storm::property::ltl::BoundedEventually<double>>(ltlFormula->getChild());
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+
+	std::shared_ptr<storm::property::ltl::BoundedEventually<double>> op = std::dynamic_pointer_cast<storm::property::ltl::BoundedEventually<double>>(formula->getChild());
 	ASSERT_NE(op.get(), nullptr);
 	ASSERT_EQ(static_cast<uint_fast64_t>(5), op->getBound());
 
 
-	ASSERT_EQ("F<=5 a", ltlFormula->toString());
+	ASSERT_EQ("F<=5 a", formula->toString());
 }
 
 TEST(LtlParserTest, parseBoundedUntilFormulaTest) {
-	std::string formula = "a U<=3 b";
-	std::shared_ptr<ltl::LtlFilter<double>> ltlFormula(nullptr);
+	std::string input = "a U<=3 b";
+	std::shared_ptr<ltl::LtlFilter<double>> formula(nullptr);
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
+		formula = storm::parser::LtlParser::parseLtlFormula(input);
 	);
 
-	ASSERT_NE(ltlFormula.get(), nullptr);
+	ASSERT_NE(formula.get(), nullptr);
 
-	std::shared_ptr<storm::property::ltl::BoundedUntil<double>> op = std::dynamic_pointer_cast<storm::property::ltl::BoundedUntil<double>>(ltlFormula->getChild());
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+
+	std::shared_ptr<storm::property::ltl::BoundedUntil<double>> op = std::dynamic_pointer_cast<storm::property::ltl::BoundedUntil<double>>(formula->getChild());
 	ASSERT_NE(op.get(), nullptr);
 	ASSERT_EQ(static_cast<uint_fast64_t>(3), op->getBound());
 
 
-	ASSERT_EQ("(a U<=3 b)", ltlFormula->toString());
+	ASSERT_EQ("(a U<=3 b)", formula->toString());
 }
 
 TEST(LtlParserTest, parseLtlFilterTest) {
@@ -112,6 +124,8 @@ TEST(LtlParserTest, parseLtlFilterTest) {
 	// The parser did not falsely recognize the input as a comment.
 	ASSERT_NE(formula, nullptr);
 
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+
 	ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator());
 
 	ASSERT_EQ(4, formula->getActionCount());
@@ -133,41 +147,45 @@ TEST(LtlParserTest, commentTest) {
 
 	// The parser recognized the input as a comment.
 	ASSERT_NE(nullptr, formula.get());
+	ASSERT_EQ(nullptr, formula->getChild().get());
 
 	// Test if the parser recognizes the comment at the end of a line.
 	input = "F X a // This is a comment.";
 	ASSERT_NO_THROW(
 				formula = storm::parser::LtlParser::parseLtlFormula(input)
 	);
+
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+
 	ASSERT_EQ("F X a", formula->toString());
 }
 
 TEST(LtlParserTest, parseComplexUntilTest) {
-	std::string formula = "a U b U<=3 c";
-	std::shared_ptr<ltl::LtlFilter<double>> ltlFormula(nullptr);
+	std::string input = "a U b U<=3 c";
+	std::shared_ptr<ltl::LtlFilter<double>> formula(nullptr);
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
+		formula = storm::parser::LtlParser::parseLtlFormula(input);
 	);
 
-	ASSERT_NE(ltlFormula.get(), nullptr);
-	ASSERT_EQ("((a U b) U<=3 c)", ltlFormula->toString());
+	ASSERT_NE(formula.get(), nullptr);
+	ASSERT_EQ("((a U b) U<=3 c)", formula->toString());
 }
 
 TEST(LtlParserTest, parseComplexFormulaTest) {
-	std::string formula = "a U F b | G a & F<=3 a U<=7 b // and a comment";
-	std::shared_ptr<ltl::LtlFilter<double>> ltlFormula(nullptr);
+	std::string input = "a U F b | G a & F<=3 a U<=7 b // and a comment";
+	std::shared_ptr<ltl::LtlFilter<double>> formula(nullptr);
 	ASSERT_NO_THROW(
-		ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula);
+		formula = storm::parser::LtlParser::parseLtlFormula(input);
 	);
 
-	ASSERT_NE(ltlFormula.get(), nullptr);
-	ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", ltlFormula->toString());
+	ASSERT_NE(formula.get(), nullptr);
+	ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", formula->toString());
 }
 
 TEST(LtlParserTest, wrongFormulaTest) {
-	std::string formula = "(a | c) & +";
+	std::string input = "(a | c) & +";
 	ASSERT_THROW(
-		storm::parser::LtlParser::parseLtlFormula(formula),
+		storm::parser::LtlParser::parseLtlFormula(input),
 		storm::exceptions::WrongFormatException
 	);
 }

test/functional/parser/PrctlParserTest.cpp

@@ -26,7 +26,10 @@ TEST(PrctlParserTest, parseApOnlyTest) {
 	);
 
 	// The parser did not falsely recognize the input as a comment.
-	ASSERT_NE(formula, nullptr);
+	ASSERT_NE(formula.get(), nullptr);
+
+	ASSERT_TRUE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
 
 	// The input was parsed correctly.
 	ASSERT_EQ(input, formula->toString());
@@ -40,7 +43,10 @@ TEST(PrctlParserTest, parsePropositionalFormulaTest) {
 	);
 
 	// The parser did not falsely recognize the input as a comment.
-	ASSERT_NE(formula, nullptr);
+	ASSERT_NE(formula.get(), nullptr);
+
+	ASSERT_TRUE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
 
 	// The input was parsed correctly.
 	ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString());
@@ -54,22 +60,30 @@ TEST(PrctlParserTest, parsePathFormulaTest) {
 	);
 
 	// The parser did not falsely recognize the input as a comment.
-	ASSERT_NE(formula, nullptr);
+	ASSERT_NE(formula.get(), nullptr);
 
 	// The input was parsed correctly.
 	ASSERT_NE(std::dynamic_pointer_cast<prctl::Next<double>>(formula->getChild()).get(), nullptr);
 	auto nextFormula = std::dynamic_pointer_cast<prctl::Next<double>>(formula->getChild());
+	ASSERT_FALSE(nextFormula->isPropositional());
+	ASSERT_FALSE(nextFormula->isProbEventuallyAP());
+
 	ASSERT_NE(std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(nextFormula->getChild()).get(), nullptr);
 	auto probBoundFormula = std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(nextFormula->getChild());
+	ASSERT_EQ(0.9, probBoundFormula->getBound());
+	ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator());
+	ASSERT_FALSE(probBoundFormula->isPropositional());
+	ASSERT_TRUE(probBoundFormula->isProbEventuallyAP());
+
 	ASSERT_NE(std::dynamic_pointer_cast<prctl::Until<double>>(probBoundFormula->getChild()).get(), nullptr);
 	auto untilFormula = std::dynamic_pointer_cast<prctl::Until<double>>(probBoundFormula->getChild());
+	ASSERT_FALSE(untilFormula->isPropositional());
+	ASSERT_FALSE(untilFormula->isProbEventuallyAP());
+
 	ASSERT_NE(std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getLeft()).get(), nullptr);
 	ASSERT_NE(std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getRight()).get(), nullptr);
 	ASSERT_EQ("a", std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getLeft())->getAp());
 	ASSERT_EQ("b", std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getRight())->getAp());
-	ASSERT_EQ(0.9, probBoundFormula->getBound());
-	ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator());
-
 
 	// The string representation is also correct.
 	ASSERT_EQ("P = ? (X P < 0.900000 (a U b))", formula->toString());
@@ -83,7 +97,7 @@ TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
 	);
 
 	// The parser did not falsely recognize the input as a comment.
-	ASSERT_NE(formula, nullptr);
+	ASSERT_NE(formula.get(), nullptr);
 
 
 	ASSERT_NE(std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(formula->getChild()).get(), nullptr);
@@ -91,6 +105,8 @@ TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
 
 	ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator());
 	ASSERT_EQ(0.5, op->getBound());
+	ASSERT_FALSE(op->isPropositional());
+	ASSERT_TRUE(op->isProbEventuallyAP());
 
 	// Test the string representation for the parsed formula.
 	ASSERT_EQ("P > 0.500000 (F a)", formula->toString());
@@ -104,13 +120,15 @@ TEST(PrctlParserTest, parseRewardFormulaTest) {
 	);
 
 	// The parser did not falsely recognize the input as a comment.
-	ASSERT_NE(formula, nullptr);
+	ASSERT_NE(formula.get(), nullptr);
 
 	ASSERT_NE(std::dynamic_pointer_cast<prctl::RewardBoundOperator<double>>(formula->getChild()).get(), nullptr);
 	std::shared_ptr<prctl::RewardBoundOperator<double>> op = std::static_pointer_cast<prctl::RewardBoundOperator<double>>(formula->getChild());
 
 	ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator());
 	ASSERT_EQ(15.0, op->getBound());
+	ASSERT_FALSE(op->isPropositional());
+	ASSERT_FALSE(op->isProbEventuallyAP());
 
 	// Test the string representation for the parsed formula.
 	ASSERT_EQ("R >= 15.000000 (I=5)", formula->toString());
@@ -124,7 +142,10 @@ TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) {
 	);
 
 	// The parser did not falsely recognize the input as a comment.
-	ASSERT_NE(formula, nullptr);
+	ASSERT_NE(formula.get(), nullptr);
+
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
 
 	// The input was parsed correctly.
 	ASSERT_EQ("R = ? (F a)", formula->toString());
@@ -138,7 +159,10 @@ TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) {
 	);
 
 	// The parser did not falsely recognize the input as a comment.
-	ASSERT_NE(formula, nullptr);
+	ASSERT_NE(formula.get(), nullptr);
+
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
 
 	// The input was parsed correctly.
 	ASSERT_EQ("P = ? (a U<=4 (b & !c))", formula->toString());
@@ -152,7 +176,10 @@ TEST(PrctlParserTest, parseComplexFormulaTest) {
 	);
 
 	// The parser did not falsely recognize the input as a comment.
-	ASSERT_NE(formula, nullptr);
+	ASSERT_NE(formula.get(), nullptr);
+
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
 
 	// The input was parsed correctly.
 	ASSERT_EQ("(R <= 0.500000 (S) & (R > 15.000000 (C <= 0.500000) | !P < 0.400000 (G P > 0.900000 (F<=7 (a & b)))))", formula->toString());
@@ -166,7 +193,7 @@ TEST(PrctlParserTest, parsePrctlFilterTest) {
 	);
 
 	// The parser did not falsely recognize the input as a comment.
-	ASSERT_NE(formula, nullptr);
+	ASSERT_NE(formula.get(), nullptr);
 
 	ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator());
 
@@ -177,12 +204,15 @@ TEST(PrctlParserTest, parsePrctlFilterTest) {
 	ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::SortAction<double>>(formula->getAction(3)).get(), nullptr);
 	ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::RangeAction<double>>(formula->getAction(4)).get(), nullptr);
 
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
+
 	// The input was parsed correctly.
 	ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString());
 }
 
 TEST(PrctlParserTest, commentTest) {
-	std::string input = "// This is a comment. And this is a commented out formula: R = ? [ F a ]";
+	std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ X a ]";
 	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
 	ASSERT_NO_THROW(
 				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
@@ -192,11 +222,15 @@ TEST(PrctlParserTest, commentTest) {
 	ASSERT_NE(nullptr, formula.get());
 
 	// Test if the parser recognizes the comment at the end of a line.
-	input = "R = ? [ F a ] // This is a comment.";
+	input = "P<=0.5 [ X a ] // This is a comment.";
 	ASSERT_NO_THROW(
 				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
 	);
-	ASSERT_EQ("R = ? (F a)", formula->toString());
+
+	ASSERT_FALSE(formula->getChild()->isPropositional());
+	ASSERT_FALSE(formula->getChild()->isProbEventuallyAP());
+
+	ASSERT_EQ("P <= 0.500000 (X a)", formula->toString());
 }