Finished the implementation of the Cls and Ltl filters.

-Mostly copy and paste from the prctl version with some individual changes.

Next up: Testing.


Former-commit-id: 19a4f90255

src/formula/Actions/FormulaAction.h

@@ -0,0 +1,103 @@
+/*
+ * PrctlFormulaAction.h
+ *
+ *  Created on: Jun 6, 2014
+ *      Author: Manuel Sascha Weiand
+ */
+
+#ifndef STORM_FORMULA_ACTION_FORMULAACTION_H_
+#define STORM_FORMULA_ACTION_FORMULAACTION_H_
+
+#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
+
+
+#include <string>
+
+namespace storm {
+namespace property {
+namespace action {
+
+template <class T>
+class FormulaAction : public AbstractAction<T> {
+
+	typedef typename AbstractAction<T>::Result Result;
+
+public:
+
+	FormulaAction(storm::property::prctl::AbstractStateFormula<T>* prctlFormula) : prctlFormula(prctlFormula), cslFormula(nullptr) {
+		//Intentionally left empty.
+	}
+
+	FormulaAction(storm::property::csl::AbstractStateFormula<T>* cslFormula) : prctlFormula(nullptr), cslFormula(cslFormula) {
+		//Intentionally left empty.
+	}
+
+	/*!
+	 * Virtual destructor
+	 * To ensure that the right destructor is called
+	 */
+	virtual ~FormulaAction() {
+		if(prctlFormula != nullptr) {
+			delete prctlFormula;
+		}
+		if(cslFormula != nullptr) {
+			delete cslFormula;
+		}
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
+
+		storm::storage::BitVector selection(result.selection);
+
+		//Compute the modelchecking results of the actions state formula and deselect all states that do not satisfy it.
+		if(prctlFormula != nullptr) {
+			selection = selection & prctlFormula->check(mc);
+		}
+
+		return Result(selection, result.stateMap, result.pathResult, result.stateResult);
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
+
+		storm::storage::BitVector selection(result.selection);
+
+		//Compute the modelchecking results of the actions state formula and deselect all states that do not satisfy it.
+		if(cslFormula != nullptr) {
+			selection = selection & cslFormula->check(mc);
+		}
+
+		return Result(selection, result.stateMap, result.pathResult, result.stateResult);
+	}
+
+	/*!
+	 *
+	 */
+	virtual std::string toString() const override {
+		std::string out = "states(";
+		if(prctlFormula != nullptr) {
+			out += prctlFormula->toString();
+		} else if(cslFormula != nullptr) {
+			out += cslFormula->toString();
+		}
+		out += ")";
+		return out;
+	}
+
+private:
+	storm::property::prctl::AbstractStateFormula<T>* prctlFormula;
+	storm::property::csl::AbstractStateFormula<T>* cslFormula;
+
+};
+
+} //namespace action
+} //namespace property
+} //namespace storm
+
+#endif /* STORM_FORMULA_ACTION_FORMULAACTION_H_ */

src/formula/Csl/CslFilter.h

@@ -14,6 +14,16 @@
 #include "src/formula/Csl/AbstractStateFormula.h"
 #include "src/modelchecker/csl/AbstractModelChecker.h"
 
+#include "src/formula/Actions/AbstractAction.h"
+
+namespace storm {
+namespace property {
+namespace action {
+ template <typename T> class AbstractAction;
+}
+}
+}
+
 namespace storm {
 namespace property {
 namespace csl {
@@ -21,6 +31,8 @@ namespace csl {
 template <class T>
 class CslFilter : public storm::property::AbstractFilter<T> {
 
+	typedef typename storm::property::action::AbstractAction<T>::Result Result;
+
 public:
 
 	CslFilter() : AbstractFilter<T>(UNDEFINED), child(nullptr), steadyStateQuery(false) {
@@ -44,82 +56,31 @@ public:
 		delete child;
 	}
 
-	void check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const {
+	void check(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
 
 		// Write out the formula to be checked.
 		std::cout << std::endl;
-		LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toFormulaString());
-		std::cout << "Model checking formula:\t" << this->toFormulaString() << std::endl;
+		LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toString());
+		std::cout << "Model checking formula:\t" << this->toString() << std::endl;
 
-		// Do a dynamic cast to test for the actual formula type and call the correct evaluation function.
-		if(dynamic_cast<AbstractStateFormula<T>*>(child) != nullptr) {
+		Result result;
 
-			// Check the formula and apply the filter actions.
-			storm::storage::BitVector result;
-
-			try {
-				result = evaluate(modelchecker, static_cast<AbstractStateFormula<T>*>(child));
-			} 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;
+		try {
+			if(dynamic_cast<AbstractStateFormula<T> *>(child) != nullptr) {
+				result = evaluate(modelchecker, dynamic_cast<AbstractStateFormula<T> *>(child));
+			} else if (dynamic_cast<AbstractPathFormula<T> *>(child) != nullptr) {
+				result = evaluate(modelchecker, dynamic_cast<AbstractPathFormula<T> *>(child));
 			}
-
-			// Now write out the result.
-
-			if(this->actions.empty()) {
-
-				// There is no filter action given. So provide legacy support:
-				// Return the results for all states labeled with "init".
-				LOG4CPLUS_INFO(logger, "Result for initial states:");
-				std::cout << "Result for initial states:" << std::endl;
-				for (auto initialState : modelchecker.getModel().getInitialStates()) {
-					LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied"));
-					std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl;
-				}
-			}
-
+		} 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;
 		}
-		else if (dynamic_cast<AbstractPathFormula<T>*>(child) != nullptr) {
-
-			// Check the formula and apply the filter actions.
-			std::vector<T> result;
 
-			try {
-				result = evaluate(modelchecker, static_cast<AbstractPathFormula<T>*>(child));
-			} 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;
+		writeOut(result, modelchecker);
 
-				return;
-			}
-
-			// Now write out the result.
-
-			if(this->actions.empty()) {
-
-				// There is no filter action given. So provide legacy support:
-				// Return the results for all states labeled with "init".
-				LOG4CPLUS_INFO(logger, "Result for initial states:");
-				std::cout << "Result for initial states:" << std::endl;
-				for (auto initialState : modelchecker.getModel().getInitialStates()) {
-					LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]);
-					std::cout << "\t" << initialState << ": " << result[initialState] << std::endl;
-				}
-			}
-
-			std::cout << std::endl << "-------------------------------------------" << std::endl;
-
-		}
-		else {
-			// This branch should be unreachable. If you ended up here, something strange has happened.
-			//TODO: Error here.
-		}
 	}
 
 	virtual std::string toString() const override {
@@ -242,10 +203,7 @@ private:
 
 
 		// Now apply all filter actions and return the result.
-		for(auto action : this->actions) {
-			result = action->evaluate(result);
-		}
-		return result;
+		return evaluateActions(result, modelchecker);
 	}
 
 	std::vector<T> evaluate(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker, AbstractPathFormula<T>* formula) const {
@@ -259,13 +217,83 @@ private:
 			result = formula->check(modelchecker, false);
 		}
 
+		// Now apply all filter actions and return the result.
+		return evaluateActions(result, modelchecker);
+	}
+
+	Result evaluateActions(Result result, storm::modelchecker::csl::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.stateMap[i] = i;
+		}
+
 		// Now apply all filter actions and return the result.
 		for(auto action : this->actions) {
-			result = action->evaluate(result);
+			result = action->evaluate(result, modelchecker);
 		}
 		return result;
 	}
 
+	void writeOut(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
+
+		// Test for the kind of result. Values or states.
+		if(!result.pathResult.empty()) {
+
+			// Write out the selected value results in the order given by the stateMap.
+			if(this->actions.empty()) {
+
+				// There is no filter action given. So provide legacy support:
+				// Return the results for all states labeled with "init".
+				LOG4CPLUS_INFO(logger, "Result for initial states:");
+				std::cout << "Result for initial states:" << std::endl;
+				for (auto initialState : modelchecker.template getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
+					LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result.pathResult[initialState]);
+					std::cout << "\t" << initialState << ": " << result.pathResult[initialState] << std::endl;
+				}
+			} else {
+				LOG4CPLUS_INFO(logger, "Result for " << result.selection.getNumberOfSetBits() << " selected states:");
+				std::cout << "Result for " << result.selection.getNumberOfSetBits() << " selected states:" << std::endl;
+
+				for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
+					if(result.selection.get(result.stateMap[i])) {
+						LOG4CPLUS_INFO(logger, "\t" << result.stateMap[i] << ": " << result.pathResult[result.stateMap[i]]);
+						std::cout << "\t" << result.stateMap[i] << ": " << result.pathResult[result.stateMap[i]] << std::endl;
+					}
+				}
+			}
+
+		} else {
+
+			// Write out the selected state results in the order given by the stateMap.
+			if(this->actions.empty()) {
+
+				// There is no filter action given. So provide legacy support:
+				// Return the results for all states labeled with "init".
+				LOG4CPLUS_INFO(logger, "Result for initial states:");
+				std::cout << "Result for initial states:" << std::endl;
+				for (auto initialState : modelchecker.template getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
+					LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.stateResult[initialState] ? "satisfied" : "not satisfied"));
+					std::cout << "\t" << initialState << ": " << result.stateResult[initialState] << std::endl;
+				}
+			} else {
+				LOG4CPLUS_INFO(logger, "Result for " << result.selection.getNumberOfSetBits() << " selected states:");
+				std::cout << "Result for " << result.selection.getNumberOfSetBits() << " selected states:" << std::endl;
+
+				for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
+					if(result.selection.get(result.stateMap[i])) {
+						LOG4CPLUS_INFO(logger, "\t" << result.stateMap[i] << ": " << (result.stateResult[result.stateMap[i]] ? "satisfied" : "not satisfied"));
+						std::cout << "\t" << result.stateMap[i] << ": " << (result.stateResult[result.stateMap[i]] ? "satisfied" : "not satisfied") << std::endl;
+					}
+				}
+			}
+		}
+
+		std::cout << std::endl << "-------------------------------------------" << std::endl;
+	}
+
 	AbstractCslFormula<T>* child;
 
 	bool steadyStateQuery;

src/formula/Ltl/LtlFilter.h

@@ -10,6 +10,17 @@
 
 #include "src/formula/AbstractFilter.h"
 #include "src/modelchecker/ltl/AbstractModelChecker.h"
+#include "src/formula/Ltl/AbstractLtlFormula.h"
+#include "src/formula/Actions/AbstractAction.h"
+#include "src/exceptions/NotImplementedException.h"
+
+namespace storm {
+namespace property {
+namespace action {
+ template <typename T> class AbstractAction;
+}
+}
+}
 
 namespace storm {
 namespace property {
@@ -18,21 +29,23 @@ namespace ltl {
 template <class T>
 class LtlFilter : public storm::property::AbstractFilter<T> {
 
+	typedef typename storm::property::action::AbstractAction<T>::Result Result;
+
 public:
 
-	LtlFilter() : child(nullptr) {
+	LtlFilter() : AbstractFilter<T>(UNDEFINED), child(nullptr) {
 		// Intentionally left empty.
 	}
 
-	LtlFilter(AbstractLtlFormula* child) : child(child) {
+	LtlFilter(AbstractLtlFormula<T>* child, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(opt), child(child) {
 		// Intentionally left empty.
 	}
 
-	LtlFilter(AbstractLtlFormula* child, action::Action<T>* action) : child(child) {
+	LtlFilter(AbstractLtlFormula<T>* child, action::AbstractAction<T>* action, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(action, opt), child(child) {
 		this->actions.push_back(action);
 	}
 
-	LtlFilter(AbstractLtlFormula* child, std::vector<action::Action<T>*> actions) : AbstractFilter<T>(actions), child(child) {
+	LtlFilter(AbstractLtlFormula<T>* child, std::vector<action::AbstractAction<T>*> actions, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(actions, opt), child(child) {
 		// Intentionally left empty.
 	}
 
@@ -52,15 +65,13 @@ public:
 
 		// Write out the formula to be checked.
 		std::cout << std::endl;
-		LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toFormulaString());
-		std::cout << "Model checking formula:\t" << this->toFormulaString() << std::endl;
+		LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toString());
+		std::cout << "Model checking formula:\t" << this->toString() << std::endl;
 
-
-		// Check the formula and apply the filter actions.
-		storm::storage::BitVector result;
+		Result result;
 
 		try {
-			result = evaluate(modelchecker, child);
+			result = evaluate(modelchecker);
 		} 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.");
@@ -69,41 +80,54 @@ public:
 			return;
 		}
 
-		// Now write out the result.
+		writeOut(result, modelchecker);
 
-		if(this->actions.empty()) {
+	}
 
-			// There is no filter action given. So provide legacy support:
-			// Return the results for all states labeled with "init".
-			LOG4CPLUS_INFO(logger, "Result for initial states:");
-			std::cout << "Result for initial states:" << std::endl;
-			for (auto initialState : modelchecker.getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
-				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied"));
-				std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl;
-			}
+	std::string toString() const override {
+		std::string desc = "";
+
+		if(this->actions.empty()){
+			// There are no filter actions but only the raw state formula. So just print that.
+			return child->toString();
 		}
 
-		std::cout << std::endl << "-------------------------------------------" << std::endl;
-	}
+		desc = "filter[";
+
+		switch(this->opt) {
+			case MINIMIZE:
+				desc += " min, ";
+				break;
+			case MAXIMIZE:
+				desc += " max, ";
+				break;
+			default:
+				break;
+		}
 
-	bool validate() const {
-		// Test whether the stored filter actions are consistent in relation to themselves and to the ingoing modelchecking result.
+		for(auto action : this->actions) {
+			desc += action->toString();
+			desc += "; ";
+		}
 
-		//TODO: Actual validation.
+		// Remove the last "; ".
+		desc.pop_back();
+		desc.pop_back();
 
-		return true;
-	}
+		desc += "]";
+
+		desc += "(";
+		desc += child->toString();
+		desc += ")";
 
-	std::string toFormulaString() const {
-		std::string desc = "filter(";
 		return desc;
 	}
 
-	std::string toString() const {
+	virtual std::string toPrettyString() const override {
 		std::string desc = "Filter: ";
 		desc += "\nActions:";
 		for(auto action : this->actions) {
-			desc += "\n\t" + action.toString();
+			desc += "\n\t" + action->toString();
 		}
 		desc += "\nFormula:\n\t" + child->toString();
 		return desc;
@@ -119,17 +143,71 @@ public:
 
 private:
 
-	storm::storage::BitVector evaluate(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker, AbstractLtlFormula<T>* formula) const {
+	Result evaluate(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
 		// First, get the model checking result.
-		storm::storage::BitVector result = formula->check(modelchecker);
+		Result result;
+
+		if(this->opt != UNDEFINED) {
+			// If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker.
+			LOG4CPLUS_ERROR(logger, "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented.");
+			throw storm::exceptions::NotImplementedException() << "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented.";
+		} else {
+			result.stateResult = child->check(modelchecker);
+		}
+
+		// Now apply all filter actions and return the result.
+
+		// 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.stateMap[i] = i;
+		}
 
 		// Now apply all filter actions and return the result.
 		for(auto action : this->actions) {
-			result = action->evaluate(result);
+			result = action->evaluate(result, modelchecker);
 		}
+
 		return result;
 	}
 
+	void writeOut(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
+
+		// Test for the kind of result. Values or states.
+		if(!result.pathResult.empty()) {
+
+			// Write out the selected value results in the order given by the stateMap.
+			if(this->actions.empty()) {
+
+				// There is no filter action given. So provide legacy support:
+				// Return the results for all states labeled with "init".
+				LOG4CPLUS_INFO(logger, "Result for initial states:");
+				std::cout << "Result for initial states:" << std::endl;
+				for (auto initialState : modelchecker.template getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
+					LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result.pathResult[initialState]);
+					std::cout << "\t" << initialState << ": " << result.pathResult[initialState] << std::endl;
+				}
+			} else {
+				LOG4CPLUS_INFO(logger, "Result for " << result.selection.getNumberOfSetBits() << " selected states:");
+				std::cout << "Result for " << result.selection.getNumberOfSetBits() << " selected states:" << std::endl;
+
+				for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
+					if(result.selection.get(result.stateMap[i])) {
+						LOG4CPLUS_INFO(logger, "\t" << result.stateMap[i] << ": " << result.pathResult[result.stateMap[i]]);
+						std::cout << "\t" << result.stateMap[i] << ": " << result.pathResult[result.stateMap[i]] << std::endl;
+					}
+				}
+			}
+
+		} else {
+			LOG4CPLUS_WARN(logger, "No results could be computed.");
+			std::cout << "No results could be computed." << std::endl;
+		}
+
+		std::cout << std::endl << "-------------------------------------------" << std::endl;
+	}
+
 	AbstractLtlFormula<T>* child;
 };
 

src/formula/Prctl/PrctlFilter.h

@@ -15,6 +15,7 @@
 #include "src/modelchecker/prctl/AbstractModelChecker.h"
 #include "src/formula/Actions/AbstractAction.h"
 
+// TODO: Test if this can be can be ommitted.
 namespace storm {
 namespace property {
 namespace action {
@@ -204,6 +205,7 @@ private:
 			result.stateResult = formula->check(modelchecker);
 		}
 
+		// Now apply all filter actions and return the result.
 		return evaluateActions(result, modelchecker);
 	}
 
@@ -218,6 +220,7 @@ private:
 			result.pathResult = formula->check(modelchecker, false);
 		}
 
+		// Now apply all filter actions and return the result.
 		return evaluateActions(result, modelchecker);
 	}
 
@@ -232,6 +235,7 @@ private:
 			result.pathResult = formula->check(modelchecker, false);
 		}
 
+		// Now apply all filter actions and return the result.
 		return evaluateActions(result, modelchecker);
 	}
 

src/parser/CslParser.cpp

@@ -174,7 +174,7 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 				);
 		sortAction.name("sort action");
 
-		abstractAction = (rangeAction) >> (qi::eps | qi::lit(";"));
+		abstractAction = (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (qi::eps | qi::lit(";"));
 		abstractAction.name("filter action");
 
 		filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
@@ -186,7 +186,7 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 
 		filter.name("CSL formula filter");
 
-		start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment ) > qi::eoi;
+		start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = nullptr] ) > qi::eoi;
 		start.name("CSL formula filter start");
 
 	}

src/parser/LtlFileParser.cpp

@@ -15,7 +15,7 @@
 namespace storm {
 namespace parser {
 
-std::list<storm::property::ltl::AbstractLtlFormula<double>*> LtlFileParser(std::string filename) {
+std::list<storm::property::ltl::LtlFilter<double>*> LtlFileParser(std::string filename) {
 	// Open file
 	std::ifstream inputFileStream(filename, std::ios::in);
 
@@ -24,7 +24,7 @@ std::list<storm::property::ltl::AbstractLtlFormula<double>*> LtlFileParser(std::
 		throw storm::exceptions::FileIoException() << message << filename;
 	}
 
-	std::list<storm::property::ltl::AbstractLtlFormula<double>*> result;
+	std::list<storm::property::ltl::LtlFilter<double>*> result;
 
 	while(!inputFileStream.eof()) {
 		std::string line;

src/parser/LtlFileParser.h

@@ -9,6 +9,7 @@
 #define LTLFILEPARSER_H_
 
 #include "formula/Ltl.h"
+#include "src/formula/Ltl/LtlFilter.h"
 
 #include <list>
 
@@ -21,7 +22,7 @@ namespace parser {
  * @param filename
  * @return The list of parsed formulas
  */
-std::list<storm::property::ltl::AbstractLtlFormula<double>*> LtlFileParser(std::string filename);
+std::list<storm::property::ltl::LtlFilter<double>*> LtlFileParser(std::string filename);
 
 } //namespace parser
 } //namespace storm

src/parser/LtlParser.cpp

@@ -10,6 +10,13 @@
 #include "src/utility/OsDetection.h"
 #include "src/utility/constants.h"
 
+// The action class headers.
+#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/Actions/BoundAction.h"
+#include "src/formula/Actions/InvertAction.h"
+#include "src/formula/Actions/RangeAction.h"
+#include "src/formula/Actions/SortAction.h"
+
 // If the parser fails due to ill-formed data, this exception is thrown.
 #include "src/exceptions/WrongFormatException.h"
 
@@ -41,18 +48,27 @@ namespace storm {
 namespace parser {
 
 template<typename Iterator, typename Skipper>
-struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper > {
+struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::LtlFilter<double>*(), Skipper > {
 	LtlGrammar() : LtlGrammar::base_type(start) {
 		//This block contains helper rules that may be used several times
 		freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))];
+		comparisonType = (
+				(qi::lit(">="))[qi::_val = storm::property::GREATER_EQUAL] |
+				(qi::lit(">"))[qi::_val = storm::property::GREATER] |
+				(qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] |
+				(qi::lit("<"))[qi::_val = storm::property::LESS]);
+		sortingCategory = (
+				(qi::lit("index"))[qi::_val = storm::property::action::SortAction<double>::INDEX] |
+				(qi::lit("value"))[qi::_val = storm::property::action::SortAction<double>::VALUE]
+				);
 		//Comment: Empty line or line starting with "//"
 		comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr];
 
 		freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))];
 
 		//This block defines rules for parsing state formulas
-		ltlFormula %= orFormula;
-		ltlFormula.name("LTL formula");
+		formula %= orFormula;
+		formula.name("LTL formula");
 		orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
 				phoenix::new_<storm::property::ltl::Or<double>>(qi::_val, qi::_1)];
 		orFormula.name("LTL formula");
@@ -68,7 +84,7 @@ struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormu
 
 		//This block defines rules for "atomic" state formulas
 		//(Propositions, probabilistic/reward formulas, and state formulas in brackets)
-		atomicLtlFormula %= pathFormula | atomicProposition | qi::lit("(") >> ltlFormula >> qi::lit(")");
+		atomicLtlFormula %= pathFormula | atomicProposition | qi::lit("(") >> formula >> qi::lit(")");
 		atomicLtlFormula.name("LTL formula");
 		atomicProposition = (freeIdentifierName)[qi::_val =
 				phoenix::new_<storm::property::ltl::Ap<double>>(qi::_1)];
@@ -77,29 +93,73 @@ struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormu
 		//This block defines rules for parsing probabilistic path formulas
 		pathFormula = (boundedEventually | eventually | globally | next);
 		pathFormula.name("LTL formula");
-		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val =
+		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > formula)[qi::_val =
 				phoenix::new_<storm::property::ltl::BoundedEventually<double>>(qi::_2, qi::_1)];
 		boundedEventually.name("LTL formula");
-		eventually = (qi::lit("F") >> ltlFormula)[qi::_val =
+		eventually = (qi::lit("F") >> formula)[qi::_val =
 				phoenix::new_<storm::property::ltl::Eventually<double> >(qi::_1)];
 		eventually.name("LTL formula");
-		globally = (qi::lit("G") >> ltlFormula)[qi::_val =
+		globally = (qi::lit("G") >> formula)[qi::_val =
 				phoenix::new_<storm::property::ltl::Globally<double> >(qi::_1)];
 		globally.name("LTL formula");
-		next = (qi::lit("X") >> ltlFormula)[qi::_val =
+		next = (qi::lit("X") >> formula)[qi::_val =
 				phoenix::new_<storm::property::ltl::Next<double> >(qi::_1)];
 		next.name("LTL formula");
 
-		start = (((ltlFormula) > (comment | qi::eps))[qi::_val = qi::_1] |
-				 comment
-				 ) > qi::eoi;
+		// This block defines rules for parsing filter actions.
+		boundAction = (qi::lit("bound") > qi::lit("(") >> comparisonType >> qi::lit(",") >> qi::double_ >> qi::lit(")"))[qi::_val =
+				        phoenix::new_<storm::property::action::BoundAction<double>>(qi::_1, qi::_2)];
+		boundAction.name("bound action");
+
+		invertAction = qi::lit("invert")[qi::_val = phoenix::new_<storm::property::action::InvertAction<double>>()];
+		invertAction.name("invert action");
+
+		rangeAction = (
+				(qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(",") > qi::uint_ >> qi::lit(")"))[qi::_val =
+						phoenix::new_<storm::property::action::RangeAction<double>>(qi::_1, qi::_2)] |
+				(qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(")"))[qi::_val =
+						phoenix::new_<storm::property::action::RangeAction<double>>(qi::_1, qi::_1 + 1)]
+				);
+		rangeAction.name("range action");
+
+		sortAction = (
+				(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 =
+						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 =
+						phoenix::new_<storm::property::action::SortAction<double>>(qi::_1, false)]
+				);
+		sortAction.name("sort action");
+
+		abstractAction = (boundAction | invertAction | rangeAction | sortAction) >> (qi::eps | qi::lit(";"));
+		abstractAction.name("filter action");
+
+		filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
+					phoenix::new_<storm::property::ltl::LtlFilter<double>>(qi::_2, qi::_1)] |
+				 (qi::lit("filter") >> qi::lit("[") >> qi::lit("max") > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
+					phoenix::new_<storm::property::ltl::LtlFilter<double>>(qi::_2, qi::_1, storm::property::MAXIMIZE)] |
+				 (qi::lit("filter") >> qi::lit("[") >> qi::lit("min") > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
+					phoenix::new_<storm::property::ltl::LtlFilter<double>>(qi::_2, qi::_1, storm::property::MINIMIZE)] |
+				 (formula)[qi::_val =
+					phoenix::new_<storm::property::ltl::LtlFilter<double>>(qi::_1)];
+		filter.name("PRCTL formula filter");
+
+		start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = nullptr] ) > qi::eoi;
 		start.name("LTL formula");
 	}
 
-	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> start;
-	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> comment;
+	qi::rule<Iterator, storm::property::ltl::LtlFilter<double>*(), Skipper> start;
+	qi::rule<Iterator, storm::property::ltl::LtlFilter<double>*(), Skipper> filter;
+
+	qi::rule<Iterator, storm::property::action::AbstractAction<double>*(), Skipper> abstractAction;
+	qi::rule<Iterator, storm::property::action::BoundAction<double>*(), Skipper> boundAction;
+	qi::rule<Iterator, storm::property::action::InvertAction<double>*(), Skipper> invertAction;
+	qi::rule<Iterator, storm::property::action::RangeAction<double>*(), Skipper> rangeAction;
+	qi::rule<Iterator, storm::property::action::SortAction<double>*(), Skipper> sortAction;
 
-	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> ltlFormula;
+	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> comment;
+	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> formula;
 	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> atomicLtlFormula;
 
 	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> andFormula;
@@ -107,10 +167,6 @@ struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormu
 	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> atomicProposition;
 	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> orFormula;
 	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> notFormula;
-	//qi::rule<Iterator, storm::property::ltl::ProbabilisticBoundOperator<double>*(), Skipper> probabilisticBoundOperator;
-
-	//qi::rule<Iterator, storm::property::ltl::AbstractNoBoundOperator<double>*(), Skipper> noBoundOperator;
-	//qi::rule<Iterator, storm::property::ltl::AbstractNoBoundOperator<double>*(), Skipper> probabilisticNoBoundOperator;
 
 	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> pathFormula;
 	qi::rule<Iterator, storm::property::ltl::BoundedEventually<double>*(), Skipper> boundedEventually;
@@ -121,6 +177,8 @@ struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormu
 	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), qi::locals< std::shared_ptr<storm::property::ltl::AbstractLtlFormula<double>>>, Skipper> until;
 
 	qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
+	qi::rule<Iterator, storm::property::ComparisonType(), Skipper> comparisonType;
+	qi::rule<Iterator, storm::property::action::SortAction<double>::SortingCategory(), Skipper> sortingCategory;
 
 };
 
@@ -128,7 +186,7 @@ struct LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormu
 } //namespace parser
 
 
-storm::property::ltl::AbstractLtlFormula<double>* storm::parser::LtlParser(std::string formulaString) {
+storm::property::ltl::LtlFilter<double>* storm::parser::LtlParser(std::string formulaString) {
 	// Prepare iterators to input.
 	BaseIteratorType stringIteratorBegin = formulaString.begin();
 	BaseIteratorType stringIteratorEnd = formulaString.end();
@@ -137,7 +195,7 @@ storm::property::ltl::AbstractLtlFormula<double>* storm::parser::LtlParser(std::
 
 
 	// Prepare resulting intermediate representation of input.
-	storm::property::ltl::AbstractLtlFormula<double>* result_pointer = nullptr;
+	storm::property::ltl::LtlFilter<double>* result_pointer = nullptr;
 
 	LtlGrammar<PositionIteratorType,  BOOST_TYPEOF(boost::spirit::ascii::space)> grammar;
 

src/parser/LtlParser.h

@@ -9,6 +9,7 @@
 #define STORM_PARSER_LTLPARSER_H_
 
 #include "src/formula/Ltl.h"
+#include "src/formula/Ltl/LtlFilter.h"
 
 namespace storm {
 namespace parser {
@@ -22,7 +23,7 @@ namespace parser {
 	* @param formulaString The string representation of the formula
 	* @throw wrongFormatException If the input could not be parsed successfully
 	*/
-storm::property::ltl::AbstractLtlFormula<double>* LtlParser(std::string formulaString);
+storm::property::ltl::LtlFilter<double>* LtlParser(std::string formulaString);
 
 /*!
  * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas.

src/parser/PrctlParser.cpp

@@ -180,7 +180,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 				);
 		sortAction.name("sort action");
 
-		abstractAction = (rangeAction) >> (qi::eps | qi::lit(";"));
+		abstractAction = (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (qi::eps | qi::lit(";"));
 		abstractAction.name("filter action");
 
 		filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =