Some more testing.

Former-commit-id: 3105a0bf3b

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -1016,7 +1016,7 @@ namespace storm {
 
                 // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape.
                 double bound = probBoundFormula->getBound();
-                std::shared_ptr<storm::property::prctl::AbstractPathFormula<double>> pathFormula = probBoundFormula->getPathFormula();
+                std::shared_ptr<storm::property::prctl::AbstractPathFormula<double>> pathFormula = probBoundFormula->getChild();
                 storm::storage::BitVector phiStates;
                 storm::storage::BitVector psiStates;
                 storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);

src/counterexamples/PathBasedSubsystemGenerator.h

@@ -402,7 +402,7 @@ public:
 			return model.getSubDtmc(subSys);
 		}
 		T bound = boundOperator->getBound();
-		std::shared_ptr<storm::property::prctl::AbstractPathFormula<T>> pathFormula = boundOperator->getPathFormula();;
+		std::shared_ptr<storm::property::prctl::AbstractPathFormula<T>> pathFormula = boundOperator->getChild();
 
 		// get "init" labeled states
 		storm::storage::BitVector initStates = model.getLabeledStates("init");

src/formula/actions/FormulaAction.h

@@ -80,7 +80,7 @@ public:
 	 *
 	 */
 	virtual std::string toString() const override {
-		std::string out = "states(";
+		std::string out = "formula(";
 		if(prctlFormula.get() != nullptr) {
 			out += prctlFormula->toString();
 		} else if(cslFormula.get() != nullptr) {

src/formula/actions/RangeAction.h

@@ -87,16 +87,16 @@ private:
 		uint_fast64_t end = to - from;
 
 		// Safety check for access bounds.
-		if(from > result.stateMap.size()) {
+		if(from >= result.stateMap.size()) {
 			LOG4CPLUS_WARN(logger, "Range begins behind the end of the states by " << to - result.stateMap.size() << ". No state was selected.");
 			std::cout << "Range begins behind the end of the states by " << to - result.stateMap.size() << ". No state was selected." << std::endl;
 
 			return Result(out, result.stateMap, result.pathResult, result.stateResult);
 		}
 
-		if(to > result.stateMap.size()) {
+		if(to >= result.stateMap.size()) {
 
-			end = result.selection.size() - from;
+			end = result.selection.size() - from - 1;
 
 			LOG4CPLUS_WARN(logger, "Range ends behind the end of the states by " << to - result.stateMap.size() << ". The range has been cut at the last state.");
 			std::cout << "Range ends behind the end of the states by " << to - result.stateMap.size() << ". The range has been cut at the last state." << std::endl;

src/formula/actions/SortAction.h

@@ -65,7 +65,7 @@ public:
 	 *
 	 */
 	virtual std::string toString() const override {
-		std::string out = "sort, ";
+		std::string out = "sort(";
 		switch (category) {
 			case INDEX:
 				out += "index";
@@ -79,7 +79,7 @@ public:
 				break;
 		}
 		out += ", ";
-		out += ascending ? "ascending" : "descending";
+		out += ascending ? "ascending)" : "descending)";
 		return out;
 	}
 

src/formula/prctl/Next.h

@@ -113,10 +113,8 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const override {
-		std::string result = "(";
-		result += " X ";
+		std::string result = "X ";
 		result += child->toString();
-		result += ")";
 		return result;
 	}
 

src/formula/prctl/PrctlFilter.h

@@ -65,6 +65,11 @@ public:
 		LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toString());
 		std::cout << "Model checking formula:\t" << this->toString() << std::endl;
 
+		writeOut(evaluate(modelchecker), modelchecker);
+	}
+
+	Result evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
+
 		Result result;
 
 		try {
@@ -78,13 +83,9 @@ public:
 		} catch (std::exception& e) {
 			std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
 			LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
-			std::cout << std::endl << "-------------------------------------------" << std::endl;
-
-			return;
 		}
 
-		writeOut(result, modelchecker);
-
+		return result;
 	}
 
 	virtual std::string toString() const override {
@@ -239,12 +240,14 @@ private:
 		return evaluateActions(result, modelchecker);
 	}
 
-	Result evaluateActions(Result result, storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
+	Result evaluateActions(Result const & input, storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
 
 		// Init the state selection and state map vectors.
-		result.selection = storm::storage::BitVector(result.stateResult.size(), true);
-		result.stateMap = std::vector<uint_fast64_t>(result.selection.size());
-		for(uint_fast64_t i = 0; i < result.selection.size(); i++) {
+		Result result = input;
+		uint_fast64_t size = result.stateResult.size() == 0 ? result.pathResult.size() : result.stateResult.size();
+		result.selection = storm::storage::BitVector(size, true);
+		result.stateMap = std::vector<uint_fast64_t>(size);
+		for(uint_fast64_t i = 0; i < size; i++) {
 			result.stateMap[i] = i;
 		}
 
@@ -258,6 +261,13 @@ private:
 
 	void writeOut(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
 
+		// Test if there is anything to write out.
+		// The selection size should only be 0 if an error occurred during the evaluation (since a model with 0 states is invalid).
+		if(result.selection.size() == 0) {
+			std::cout << std::endl << "-------------------------------------------" << std::endl;
+			return;
+		}
+
 		// Test for the kind of result. Values or states.
 		if(!result.pathResult.empty()) {
 

src/formula/prctl/ProbabilisticBoundOperator.h

@@ -60,7 +60,7 @@ public:
 	/*!
 	 * Empty constructor
 	 */
-	ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), pathFormula(nullptr) {
+	ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), child(nullptr) {
 		// Intentionally left empty.
 	}
 
@@ -69,10 +69,10 @@ public:
 	 *
 	 * @param comparisonOperator The relation for the bound.
 	 * @param bound The bound for the probability
-	 * @param pathFormula The child node
+	 * @param child The child node
 	 */
-	ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractPathFormula<T>> const & pathFormula)
-		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
+	ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractPathFormula<T>> const & child)
+		: comparisonOperator(comparisonOperator), bound(bound), child(child) {
 		// Intentionally left empty.
 	}
 
@@ -96,7 +96,7 @@ public:
 		std::shared_ptr<ProbabilisticBoundOperator<T>> result(new ProbabilisticBoundOperator<T>());
 		result->setComparisonOperator(comparisonOperator);
 		result->setBound(bound);
-		result->setPathFormula(pathFormula->clone());
+		result->setChild(child->clone());
 		return result;
 	}
 
@@ -120,7 +120,7 @@ public:
 	 *  @return true iff the subtree conforms to some logic.
 	 */
 	virtual bool validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(pathFormula);
+		return checker.validate(child);
 	}
 
 	/*!
@@ -137,7 +137,7 @@ public:
 		result += " ";
 		result += std::to_string(bound);
 		result += " (";
-		result += pathFormula->toString();
+		result += child->toString();
 		result += ")";
 		return result;
 	}
@@ -145,25 +145,25 @@ public:
 	/*!
 	 * @returns the child node (representation of a formula)
 	 */
-	std::shared_ptr<AbstractPathFormula<T>> const & getPathFormula () const {
-		return pathFormula;
+	std::shared_ptr<AbstractPathFormula<T>> const & getChild () const {
+		return child;
 	}
 
 	/*!
 	 * Sets the child node
 	 *
-	 * @param pathFormula the path formula that becomes the new child node
+	 * @param child the path formula that becomes the new child node
 	 */
-	void setPathFormula(std::shared_ptr<AbstractPathFormula<T>> const & pathFormula) {
-		this->pathFormula = pathFormula;
+	void setChild(std::shared_ptr<AbstractPathFormula<T>> const & child) {
+		this->child = child;
 	}
 
 	/*!
 	 *
 	 * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
 	 */
-	bool pathFormulaIsSet() const {
-		return pathFormula.get() != nullptr;
+	bool childIsSet() const {
+		return child.get() != nullptr;
 	}
 
 	/*!
@@ -206,7 +206,7 @@ public:
 private:
 	storm::property::ComparisonType comparisonOperator;
 	T bound;
-	std::shared_ptr<AbstractPathFormula<T>> pathFormula;
+	std::shared_ptr<AbstractPathFormula<T>> child;
 };
 
 } //namespace prctl

src/formula/prctl/RewardBoundOperator.h

@@ -58,7 +58,7 @@ public:
 	/*!
 	 * Empty constructor
 	 */
-	RewardBoundOperator() : comparisonOperator(LESS), bound(0), pathFormula(nullptr){
+	RewardBoundOperator() : comparisonOperator(LESS), bound(0), child(nullptr){
 		// Intentionally left empty
 	}
 
@@ -67,10 +67,10 @@ public:
 	 *
 	 * @param comparisonOperator The relation for the bound.
 	 * @param bound The bound for the probability
-	 * @param pathFormula The child node
+	 * @param child The child node
 	 */
-	RewardBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractRewardPathFormula<T>> const & pathFormula)
-		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
+	RewardBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractRewardPathFormula<T>> const & child)
+		: comparisonOperator(comparisonOperator), bound(bound), child(child) {
 		// Intentionally left empty
 	}
 
@@ -94,7 +94,7 @@ public:
 		std::shared_ptr<RewardBoundOperator<T>> result(new RewardBoundOperator<T>());
 		result->setComparisonOperator(comparisonOperator);
 		result->setBound(bound);
-		result->setPathFormula(pathFormula->clone());
+		result->setChild(child->clone());
 		return result;
 	}
 
@@ -118,7 +118,7 @@ public:
 	 *  @return true iff the subtree conforms to some logic.
 	 */
 	virtual bool validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->pathFormula);
+		return checker.validate(this->child);
 	}
 
 	/*!
@@ -135,7 +135,7 @@ public:
 		result += " ";
 		result += std::to_string(bound);
 		result += " (";
-		result += pathFormula->toString();
+		result += child->toString();
 		result += ")";
 		return result;
 	}
@@ -143,25 +143,25 @@ public:
 	/*!
 	 * @returns the child node (representation of a formula)
 	 */
-	std::shared_ptr<AbstractRewardPathFormula<T>> const & getPathFormula () const {
-		return pathFormula;
+	std::shared_ptr<AbstractRewardPathFormula<T>> const & getChild () const {
+		return child;
 	}
 
 	/*!
 	 * Sets the child node
 	 *
-	 * @param pathFormula the path formula that becomes the new child node
+	 * @param child the path formula that becomes the new child node
 	 */
-	void setPathFormula(std::shared_ptr<AbstractRewardPathFormula<T>> const & pathFormula) {
-		this->pathFormula = pathFormula;
+	void setChild(std::shared_ptr<AbstractRewardPathFormula<T>> const & child) {
+		this->child = child;
 	}
 
 	/*!
 	 *
 	 * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
 	 */
-	bool pathFormulaIsSet() const {
-		return pathFormula.get() != nullptr;
+	bool childIsSet() const {
+		return child.get() != nullptr;
 	}
 
 	/*!
@@ -204,7 +204,7 @@ public:
 private:
 	storm::property::ComparisonType comparisonOperator;
 	T bound;
-	std::shared_ptr<AbstractRewardPathFormula<T>> pathFormula;
+	std::shared_ptr<AbstractRewardPathFormula<T>> child;
 };
 
 } //namespace prctl

src/modelchecker/prctl/AbstractModelChecker.h

@@ -189,7 +189,7 @@ public:
 	 */
 	virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator<Type> const& formula) const {
 		// First, we need to compute the probability for satisfying the path formula for each state.
-		std::vector<Type> quantitativeResult = formula.getPathFormula()->check(*this, false);
+		std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false);
 
 		// Create resulting bit vector that will hold the yes/no-answer for every state.
 		storm::storage::BitVector result(quantitativeResult.size());
@@ -213,7 +213,7 @@ public:
 	 */
 	virtual storm::storage::BitVector checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator<Type>& formula) const {
 		// First, we need to compute the probability for satisfying the path formula for each state.
-		std::vector<Type> quantitativeResult = formula.getPathFormula()->check(*this, false);
+		std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false);
 
 		// Create resulting bit vector that will hold the yes/no-answer for every state.
 		storm::storage::BitVector result(quantitativeResult.size());

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -87,7 +87,7 @@ namespace storm {
 					}
 
             		// First, we need to compute the probability for satisfying the path formula for each state.
-            		std::vector<Type> quantitativeResult = formula.getPathFormula()->check(*this, false);
+            		std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false);
 
             		//Remove the minimizing operator entry from the stack.
             		this->minimumOperatorStack.pop();
@@ -124,7 +124,7 @@ namespace storm {
 					}
 
             		// First, we need to compute the probability for satisfying the path formula for each state.
-            		std::vector<Type> quantitativeResult = formula.getPathFormula()->check(*this, false);
+            		std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false);
 
             		//Remove the minimizing operator entry from the stack.
 					this->minimumOperatorStack.pop();

src/parser/PrctlParser.cpp

@@ -79,11 +79,10 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
 		atomicProposition = (freeIdentifierName)[qi::_val =
 				MAKE(prctl::Ap<double>, qi::_1)];
 		atomicProposition.name("atomic proposition");
-		probabilisticBoundOperator = ((qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
+		probabilisticBoundOperator = ((qi::lit("P") >> comparisonType > qi::double_ > pathFormula)[qi::_val =
 				MAKE(prctl::ProbabilisticBoundOperator<double>, qi::_1, qi::_2, qi::_3)]);
-
 		probabilisticBoundOperator.name("probabilistic bound operator");
-		rewardBoundOperator = ((qi::lit("R") >> comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val =
+		rewardBoundOperator = ((qi::lit("R") >> comparisonType > qi::double_ > rewardPathFormula)[qi::_val =
 				MAKE(prctl::RewardBoundOperator<double>, qi::_1, qi::_2, qi::_3)]);
 		rewardBoundOperator.name("reward bound operator");
 
@@ -92,22 +91,22 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
 		pathFormula.name("path formula");
 		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
 				MAKE(prctl::BoundedEventually<double>, qi::_2, qi::_1)];
-		boundedEventually.name("path formula (for probabilistic operator)");
+		boundedEventually.name("bounded eventually");
 		eventually = (qi::lit("F") > stateFormula)[qi::_val =
 				MAKE(prctl::Eventually<double>, qi::_1)];
-		eventually.name("path formula (for probabilistic operator)");
+		eventually.name("eventually");
 		next = (qi::lit("X") > stateFormula)[qi::_val =
 				MAKE(prctl::Next<double>, qi::_1)];
-		next.name("path formula (for probabilistic operator)");
+		next.name("next");
 		globally = (qi::lit("G") > stateFormula)[qi::_val =
 				MAKE(prctl::Globally<double>, qi::_1)];
-		globally.name("path formula (for probabilistic operator)");
+		globally.name("globally");
 		boundedUntil = (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
 				MAKE(prctl::BoundedUntil<double>, qi::_a, qi::_3, qi::_2)];
-		boundedUntil.name("path formula (for probabilistic operator)");
+		boundedUntil.name("boundedUntil");
 		until = (stateFormula[qi::_a = qi::_1] >> qi::lit("U") > stateFormula)[qi::_val =
 				MAKE(prctl::Until<double>, qi::_a, qi::_2)];
-		until.name("path formula (for probabilistic operator)");
+		until.name("until");
 
 		// This block defines rules for parsing reward path formulas.
 		rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward | qi::lit("(") >> rewardPathFormula >> qi::lit(")") | qi::lit("[") >> rewardPathFormula >> qi::lit("]"));
@@ -175,16 +174,16 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
 		rangeAction.name("range action");
 
 		sortAction = (
-				(qi::lit("sort") > qi::lit("(") >> sortingCategory >> qi::lit(")"))[qi::_val =
+				(qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(")"))[qi::_val =
 						phoenix::new_<storm::property::action::SortAction<double>>(qi::_1)] |
-				(qi::lit("sort") > qi::lit("(") >> sortingCategory >> qi::lit(", ") >> qi::lit("asc") > qi::lit(")"))[qi::_val =
+				(qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("ascending") | qi::lit("asc")) > qi::lit(")"))[qi::_val =
 						phoenix::new_<storm::property::action::SortAction<double>>(qi::_1, true)] |
-				(qi::lit("sort") > qi::lit("(") >> sortingCategory >> qi::lit(", ") >> qi::lit("desc") > qi::lit(")"))[qi::_val =
+				(qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("descending") | qi::lit("desc")) > qi::lit(")"))[qi::_val =
 						phoenix::new_<storm::property::action::SortAction<double>>(qi::_1, false)]
 				);
 		sortAction.name("sort action");
 
-		abstractAction = (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (qi::eps | qi::lit(";"));
+		abstractAction = (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (qi::lit(";") | qi::eps);
 		abstractAction.name("filter action");
 
 		filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
@@ -200,7 +199,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
 		filter.name("PRCTL formula filter");
 
 		start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = MAKE(prctl::PrctlFilter<double>, nullptr)]) > qi::eoi;
-		start.name("PRCTL formula filter");
+		start.name("start");
 
 	}
 

test/functional/modelchecker/FilterTest.cpp

@@ -0,0 +1,83 @@
+/*
+ * FilterTest.cpp
+ *
+ *  Created on: Aug 6, 2014
+ *      Author: Manuel Sascha Weiand
+ */
+
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/models/Dtmc.h"
+#include "src/parser/DeterministicModelParser.h"
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "src/solver/GmmxxLinearEquationSolver.h"
+#include "src/formula/prctl/PrctlFilter.h"
+#include "src/formula/csl/CslFilter.h"
+#include "src/formula/ltl/LtlFilter.h"
+#include "src/parser/PrctlParser.h"
+
+#include <regex>
+
+typedef typename storm::property::prctl::PrctlFilter<double>::Result Result;
+
+TEST(PrctlFilterTest, generalFunctionality) {
+	// Test filter queries of increasing complexity.
+
+	// Setup model and modelchecker.
+	storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
+	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+
+	// Find the best valued state to finally reach a 'b' state.
+	std::string input = "filter[sort(value, descending); range(0,0)](F b)";
+	std::shared_ptr<storm::property::prctl::PrctlFilter<double>> formula(nullptr);
+	ASSERT_NO_THROW(
+				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+	);
+
+	// Here we test if the check method gives the correct result.
+	// To capture the output, redirect cout and test the written buffer content.
+	std::stringstream buffer;
+	std::streambuf *sbuf = std::cout.rdbuf();
+	std::cout.rdbuf(buffer.rdbuf());
+
+	formula->check(mc);
+
+	std::string output = buffer.str();
+	ASSERT_NE(std::string::npos, output.find("\t6: 1"));
+
+	// Reset cout to the original buffer.
+	std::cout.rdbuf(sbuf);
+
+	// The remaining queries use evaluate directly as its easier to work with in a test environment.
+	// Get the probability to reach a b state for all states but those that cannot reach a 'b' state or are 'b' states themselves.
+	// Sorted by value; highest first.
+	input = "filter[formula(P<=0(F b) | b); invert; sort(value, desc)](F b)";
+	ASSERT_NO_THROW(
+				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+	);
+
+	Result result = formula->evaluate(mc);
+
+	// Test the selection.
+	ASSERT_EQ(5, result.selection.getNumberOfSetBits());
+	ASSERT_TRUE(result.selection[0]);
+	ASSERT_TRUE(result.selection[1]);
+	ASSERT_TRUE(result.selection[2]);
+	ASSERT_TRUE(result.selection[3]);
+	ASSERT_TRUE(result.selection[4]);
+	ASSERT_FALSE(result.selection[5]);
+	ASSERT_FALSE(result.selection[6]);
+	ASSERT_FALSE(result.selection[7]);
+
+	// Test the sorting.
+	ASSERT_EQ(3, result.stateMap[0]);
+	ASSERT_EQ(4, result.stateMap[1]);
+	ASSERT_EQ(1, result.stateMap[2]);
+	ASSERT_EQ(0, result.stateMap[3]);
+	ASSERT_EQ(2, result.stateMap[4]);
+	ASSERT_EQ(5, result.stateMap[5]);
+	ASSERT_EQ(6, result.stateMap[6]);
+	ASSERT_EQ(7, result.stateMap[7]);
+}
+
+

test/functional/parser/PrctlParserTest.cpp

@@ -10,6 +10,11 @@
 #include "storm-config.h"
 #include "src/parser/PrctlParser.h"
 #include "src/exceptions/WrongFormatException.h"
+#include "src/formula/actions/FormulaAction.h"
+#include "src/formula/actions/InvertAction.h"
+#include "src/formula/actions/SortAction.h"
+#include "src/formula/actions/RangeAction.h"
+#include "src/formula/actions/BoundAction.h"
 
 namespace prctl = storm::property::prctl;
 
@@ -41,6 +46,35 @@ TEST(PrctlParserTest, parsePropositionalFormulaTest) {
 	ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString());
 }
 
+TEST(PrctlParserTest, parsePathFormulaTest) {
+	std::string input = "X( P<0.9 (a U b))";
+	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
+	ASSERT_NO_THROW(
+				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+	);
+
+	// The parser did not falsely recognize the input as a comment.
+	ASSERT_NE(formula, 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_NE(std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(nextFormula->getChild()).get(), nullptr);
+	auto probBoundFormula = std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(nextFormula->getChild());
+	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_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());
+}
+
 TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
 	std::string input =  "P > 0.5 [ F a ]";
 	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
@@ -124,6 +158,45 @@ TEST(PrctlParserTest, parseComplexFormulaTest) {
 	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());
 }
 
+TEST(PrctlParserTest, parsePrctlFilterTest) {
+	std::string input = "filter[formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)";
+	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
+	ASSERT_NO_THROW(
+				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+	);
+
+	// The parser did not falsely recognize the input as a comment.
+	ASSERT_NE(formula, nullptr);
+
+	ASSERT_EQ(5, formula->getActionCount());
+	ASSERT_NE(dynamic_cast<storm::property::action::FormulaAction<double>*>(formula->getAction(0)), nullptr);
+	ASSERT_NE(dynamic_cast<storm::property::action::InvertAction<double>*>(formula->getAction(1)), nullptr);
+	ASSERT_NE(dynamic_cast<storm::property::action::BoundAction<double>*>(formula->getAction(2)), nullptr);
+	ASSERT_NE(dynamic_cast<storm::property::action::SortAction<double>*>(formula->getAction(3)), nullptr);
+	ASSERT_NE(dynamic_cast<storm::property::action::RangeAction<double>*>(formula->getAction(4)), nullptr);
+
+	// The input was parsed correctly.
+	ASSERT_EQ("filter[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::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
+	ASSERT_NO_THROW(
+				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+	);
+
+	// The parser recognized the input as a comment.
+	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.";
+	ASSERT_NO_THROW(
+				formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+	);
+	ASSERT_EQ("R = ? (F a)", formula->toString());
+}
+
 
 TEST(PrctlParserTest, wrongProbabilisticFormulaTest) {
 	std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);