Added some filter actions.

- Also major cleanup of the filter.
- Implementation clompleted for pctl.

Next up: Wrap up the Csl and Ltl filter and then testing.


Former-commit-id: 8189f8462c

src/formula/AbstractFilter.h

@@ -9,6 +9,7 @@
 #define STORM_FORMULA_ABSTRACTFILTER_H_
 
 #include <vector>
+#include <string>
 #include "src/formula/AbstractFormula.h"
 #include "src/formula/Actions/AbstractAction.h"
 

src/formula/Actions/AbstractAction.h

@@ -9,7 +9,11 @@
 #define STORM_FORMULA_ACTION_ABSTRACTACTION_H_
 
 #include <vector>
+#include <utility>
 #include "src/storage/BitVector.h"
+#include "src/modelchecker/prctl/AbstractModelChecker.h"
+#include "src/modelchecker/csl/AbstractModelChecker.h"
+#include "src/modelchecker/ltl/AbstractModelChecker.h"
 
 namespace storm {
 namespace property {
@@ -20,6 +24,42 @@ class AbstractAction {
 
 public:
 
+	struct Result {
+
+		/*!
+		 *
+		 */
+		Result() : selection(), stateMap(), pathResult(), stateResult(){
+			// Intentionally left empty.
+		}
+
+		/*!
+		 *
+		 */
+		Result(Result const & other) : selection(other.selection), stateMap(other.stateMap), pathResult(other.pathResult), stateResult(other.stateResult) {
+			// Intentionally left empty.
+		}
+
+		/*!
+		 *
+		 */
+		Result(storm::storage::BitVector const & selection, std::vector<uint_fast64_t> const & stateMap, std::vector<T> const & pathResult, storm::storage::BitVector const & stateResult) : selection(selection), stateMap(stateMap), pathResult(pathResult), stateResult(stateResult) {
+			// Intentionally left empty.
+		}
+
+		//!
+		storm::storage::BitVector selection;
+
+		//!
+		std::vector<uint_fast64_t> stateMap;
+
+		//!
+		std::vector<T> pathResult;
+
+		//!
+		storm::storage::BitVector stateResult;
+	};
+
 	/*!
 	 * Virtual destructor
 	 * To ensure that the right destructor is called
@@ -28,29 +68,32 @@ public:
 		//Intentionally left empty
 	}
 
-	/*!
+	/*
 	 *
 	 */
-	virtual std::vector<T> evaluate(std::vector<T> input) const {
-		return input;
+	virtual Result evaluate(Result const & filterResult, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const {
+		return Result();
 	}
 
-	/*!
+	/*
 	 *
 	 */
-	virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const {
-		return input;
+	virtual Result evaluate(Result const & filterResult, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const {
+		return Result();
 	}
 
-	/*!
+	/*
 	 *
 	 */
-	virtual std::string toString() const = 0;
+	virtual Result evaluate(Result const & filterResult, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const {
+		return Result();
+	}
 
 	/*!
 	 *
 	 */
-	virtual std::string toFormulaString() const = 0;
+	virtual std::string toString() const = 0;
+
 };
 
 } //namespace action

src/formula/Actions/BoundAction.h

@@ -0,0 +1,167 @@
+/*
+ * BoundAction.h
+ *
+ *  Created on: Jun 22, 2014
+ *      Author: Manuel Sascha Weiand
+ */
+
+#ifndef STORM_FORMULA_ACTION_BOUNDACTION_H_
+#define STORM_FORMULA_ACTION_BOUNDACTION_H_
+
+#include "src/formula/Actions/AbstractAction.h"
+#include "src/formula/ComparisonType.h"
+
+namespace storm {
+namespace property {
+namespace action {
+
+template <class T>
+class BoundAction : public AbstractAction<T> {
+
+	typedef typename AbstractAction<T>::Result Result;
+
+public:
+
+	BoundAction() : comparisonOperator(storm::property::GREATER_EQUAL), bound(0) {
+		//Intentionally left empty.
+	}
+
+	BoundAction(storm::property::ComparisonType comparisonOperator, T bound) : comparisonOperator(comparisonOperator), bound(bound) {
+		//Intentionally left empty.
+	}
+
+	/*!
+	 * Virtual destructor
+	 * To ensure that the right destructor is called
+	 */
+	virtual ~BoundAction() {
+		//Intentionally left empty
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
+	}
+
+	/*!
+	 *
+	 */
+	virtual std::string toString() const override {
+		std::string out = "bound(";
+		switch (comparisonOperator) {
+			case LESS:
+				out += "<";
+				break;
+			case LESS_EQUAL:
+				out += "<=";
+				break;
+			case GREATER:
+				out += ">";
+				break;
+			case GREATER_EQUAL:
+				out += ">=";
+				break;
+			default:
+				LOG4CPLUS_INFO(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
+				std::cout << "Unknown comparison operator of value " << comparisonOperator << "." << std::endl;
+				break;
+		}
+		out += ", ";
+		out += std::to_string(bound);
+		out += ")";
+		return out;
+	}
+
+private:
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result) const {
+
+		//Initialize the new selection vector.
+		storm::storage::BitVector out(result.selection.size());
+
+		if(result.pathResult.size() != 0) {
+
+			//Fill the selction by comapring the values for all previously selected states with theegiven bound using the comparison operator.
+			for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
+				if(result.selection[result.stateMap[i]]) {
+					switch(comparisonOperator) {
+						case storm::property::GREATER_EQUAL:
+							out.set(result.pathResult[result.stateMap[i]] >= bound);
+							break;
+						case storm::property::GREATER:
+							out.set(result.pathResult[result.stateMap[i]] > bound);
+							break;
+						case storm::property::LESS_EQUAL:
+							out.set(result.pathResult[result.stateMap[i]] <= bound);
+							break;
+						case storm::property::LESS:
+							out.set(result.pathResult[result.stateMap[i]] < bound);
+							break;
+						default:
+							LOG4CPLUS_INFO(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
+							std::cout << "Unknown comparison operator of value " << comparisonOperator << "." << std::endl;
+							break;
+					}
+				}
+			}
+		} else {
+
+			//Fill the selction by comapring the values for all previously selected states with theegiven bound using the comparison operator.
+			for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
+				if(result.selection[result.stateMap[i]]) {
+					switch(comparisonOperator) {
+						case storm::property::GREATER_EQUAL:
+							out.set(result.stateResult[result.stateMap[i]] >= bound);
+							break;
+						case storm::property::GREATER:
+							out.set(result.stateResult[result.stateMap[i]] > bound);
+							break;
+						case storm::property::LESS_EQUAL:
+							out.set(result.stateResult[result.stateMap[i]] <= bound);
+							break;
+						case storm::property::LESS:
+							out.set(result.stateResult[result.stateMap[i]] < bound);
+							break;
+						default:
+							LOG4CPLUS_INFO(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
+							std::cout << "Unknown comparison operator of value " << comparisonOperator << "." << std::endl;
+							break;
+					}
+				}
+			}
+		}
+
+		return Result(out, result.stateMap, result.pathResult, result.stateResult);
+	}
+
+	storm::property::ComparisonType comparisonOperator;
+	T bound;
+
+};
+
+
+}
+}
+}
+
+
+#endif /* STORM_FORMULA_ACTION_BOUNDACTION_H_ */

src/formula/Actions/InvertAction.h

@@ -0,0 +1,80 @@
+/*
+ * InvertAction.h
+ *
+ *  Created on: Jun 22, 2014
+ *      Author: Manuel Sascha Weiand
+ */
+
+#ifndef STORM_FORMULA_ACTION_INVERTACTION_H_
+#define STORM_FORMULA_ACTION_INVERTACTION_H_
+
+#include "src/formula/Actions/AbstractAction.h"
+
+namespace storm {
+namespace property {
+namespace action {
+
+template <class T>
+class InvertAction : public AbstractAction<T> {
+
+	typedef typename AbstractAction<T>::Result Result;
+
+public:
+
+	InvertAction() {
+		//Intentionally left empty.
+	}
+
+	/*!
+	 * Virtual destructor
+	 * To ensure that the right destructor is called
+	 */
+	virtual ~InvertAction() {
+		//Intentionally left empty
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
+	}
+
+	/*!
+	 *
+	 */
+	virtual std::string toString() const override {
+		return "invert";
+	}
+
+private:
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result) const {
+		storm::storage::BitVector out(result.selection);
+		return Result(~out, result.stateMap, result.pathResult, result.stateResult);
+	}
+};
+
+} //namespace action
+} //namespace property
+} //namespace storm
+
+
+#endif /* STORM_FORMULA_ACTION_INVERTACTION_H_ */

src/formula/Actions/RangeAction.h

@@ -10,8 +10,6 @@
 
 #include "src/formula/Actions/AbstractAction.h"
 
-#include <string>
-
 namespace storm {
 namespace property {
 namespace action {
@@ -19,14 +17,21 @@ namespace action {
 template <class T>
 class RangeAction : public AbstractAction<T> {
 
+	typedef typename AbstractAction<T>::Result Result;
+
 public:
 
 	RangeAction() : from(0), to(0) {
 		//Intentionally left empty.
 	}
 
+	/*!
+	 *	Excluding the state with position to.
+	 */
 	RangeAction(uint_fast64_t from, uint_fast64_t to) : from(from), to(to) {
-		//Intentionally left empty.
+		if(from > to) {
+			throw storm::exceptions::IllegalArgumentException() << "The end of the range is lower than its beginning";
+		}
 	}
 
 	/*!
@@ -40,56 +45,71 @@ public:
 	/*!
 	 *
 	 */
-	virtual std::vector<T> evaluate(std::vector<T> input) const override {
-		// The range constructor is used here instead of manipulating the incoming vector.
-		// While deleting the element at the end of the vector is efficient, deleting elements at any position but the end is not.
-		// Also this leaves the incoming vector unchanged.
-		std::vector<T> out(input.begin() + from, input.begin() + to);
-		return out;
+	virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
 	}
 
 	/*!
 	 *
 	 */
-	virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const override {
-		//Initialize the output vector.
-		storm::storage::BitVector out(to - from  + 1);
-
-		storm::storage::BitVector::const_iterator it = input.begin();
-
-		//Proceed the set index iterator to the first set bit within the range.
-		for(; *it < from; ++it);
+	virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
+	}
 
-		//Fill the output vector.
-		for(; *it <= to; ++it) {
-			out.set(*it-from);
-		}
-		return out;
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
 	}
 
 	/*!
 	 *
 	 */
 	virtual std::string toString() const override {
-		std::string out = "range, ";
+		std::string out = "range(";
 		out += std::to_string(from);
 		out += ", ";
 		out += std::to_string(to);
+		out += ")";
 		return out;
 	}
 
+private:
+
 	/*!
 	 *
 	 */
-	virtual std::string toFormulaString() const override {
-		std::string out = "\"range\", ";
-		out += std::to_string(from);
-		out += ", ";
-		out += std::to_string(to);
-		return out;
+	virtual Result evaluate(Result const & result) const {
+		//Initialize the output vector.
+		storm::storage::BitVector out(result.selection.size());
+
+		uint_fast64_t end = to - from;
+
+		// Safety check for access bounds.
+		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()) {
+
+			end = result.selection.size() - from;
+
+			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;
+		}
+
+		//Fill the output vector.
+		for(uint_fast64_t i=0; i < end; i++) {
+			out.set(result.stateMap[from + i], result.selection[result.stateMap[from + i]]);
+		}
+
+		return Result(out, result.stateMap, result.pathResult, result.stateResult);
 	}
 
-private:
 	uint_fast64_t from;
 	uint_fast64_t to;
 

src/formula/Actions/SortAction.h

@@ -0,0 +1,174 @@
+/*
+ * SortAction.h
+ *
+ *  Created on: Jun 22, 2014
+ *      Author: Manuel Sascha Weiand
+ */
+
+#ifndef STORM_FORMULA_ACTION_SORTACTION_H_
+#define STORM_FORMULA_ACTION_SORTACTION_H_
+
+#include "src/formula/Actions/AbstractAction.h"
+#include <cctype>
+
+namespace storm {
+namespace property {
+namespace action {
+
+template <class T>
+class SortAction : public AbstractAction<T> {
+
+	typedef typename AbstractAction<T>::Result Result;
+
+public:
+
+	enum SortingCategory {INDEX, VALUE};
+
+	SortAction() : category(INDEX), ascending(true) {
+		//Intentionally left empty.
+	}
+
+	SortAction(SortingCategory category, bool ascending = true) : category(category), ascending(ascending) {
+		//Intentionally left empty.
+	}
+
+	/*!
+	 * Virtual destructor
+	 * To ensure that the right destructor is called
+	 */
+	virtual ~SortAction() {
+		//Intentionally left empty
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
+	}
+
+	/*!
+	 *
+	 */
+	virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
+		return evaluate(result);
+	}
+
+	/*!
+	 *
+	 */
+	virtual std::string toString() const override {
+		std::string out = "sort, ";
+		switch (category) {
+			case INDEX:
+				out += "index";
+				break;
+			case VALUE:
+				out += "value";
+				break;
+			default:
+				LOG4CPLUS_INFO(logger, "Unknown sorting category of value " << category << ".");
+				std::cout << "Unknown sorting category of value " << category << "." << std::endl;
+				break;
+		}
+		out += ", ";
+		out += ascending ? "ascending" : "descending";
+		return out;
+	}
+
+
+private:
+
+	/*!
+	 *
+	 */
+	Result evaluate(Result const & result) const {
+
+		if(category == VALUE) {
+			//TODO
+
+			if(result.pathResult.size() != 0) {
+				return Result(result.selection, sort(result.stateMap, result.pathResult), result.pathResult, result.stateResult);
+			} else {
+				return Result(result.selection, sort(result.stateMap, result.stateResult), result.pathResult, result.stateResult);
+			}
+
+		} else {
+			return Result(result.selection, sort(result.stateMap.size()), result.pathResult, result.stateResult);
+		}
+	}
+
+	/*!
+	 *
+	 */
+	std::vector<uint_fast64_t> sort(uint_fast64_t length) const {
+
+		// Project the vector down to its first component.
+		std::vector<uint_fast64_t> outMap(length);
+
+		// Sort the combined vector.
+		if(ascending) {
+			for(uint_fast64_t i = 0; i < length; i++) {
+				outMap[i] = i;
+			}
+		} else {
+			for(uint_fast64_t i = 0; i < length; i++) {
+				outMap[i] = length - i - 1;
+			}
+		}
+
+		return outMap;
+	}
+
+	/*!
+	 *
+	 */
+	std::vector<uint_fast64_t> sort(std::vector<uint_fast64_t> const & stateMap, std::vector<T> const & values) const {
+
+		// Prepare the new state map.
+		std::vector<uint_fast64_t> outMap(stateMap);
+
+		// Sort the state map.
+		if(ascending) {
+			std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] <= values[b]; });
+		} else {
+			std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] >= values[b]; });
+		}
+
+		return outMap;
+	}
+
+	/*!
+	 *
+	 */
+	std::vector<uint_fast64_t> sort(std::vector<uint_fast64_t> const & stateMap, storm::storage::BitVector const & values) const {
+
+		// Prepare the new state map.
+		std::vector<uint_fast64_t> outMap(stateMap);
+
+		// Sort the state map.
+		if(ascending) {
+			std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] <= values[b]; });
+		} else {
+			std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] >= values[b]; });
+		}
+
+		return outMap;
+	}
+
+	SortingCategory category;
+	bool ascending;
+};
+
+} //namespace action
+} //namespace property
+} //namespace storm
+
+#endif /* STORM_FORMULA_ACTION_SORTACTION_H_ */

src/formula/Csl/CslFilter.h

@@ -122,24 +122,6 @@ public:
 		}
 	}
 
-	bool validate() const {
-		// Test whether the stored filter actions are consistent in relation to themselves and to the ingoing modelchecking result.
-
-		// Do a dynamic cast to test for the actual formula type.
-		if(dynamic_cast<AbstractStateFormula<T>*>(child) != nullptr) {
-			//TODO: Actual validation.
-		}
-		else if (dynamic_cast<AbstractPathFormula<T>*>(child) != nullptr) {
-			//TODO: Actual validation.
-		}
-		else {
-			// This branch should be unreachable. If you ended up here, something strange has happened.
-			//TODO: Error here.
-		}
-
-		return true;
-	}
-
 	virtual std::string toString() const override {
 		std::string desc = "";
 

src/formula/Prctl/PrctlFilter.h

@@ -13,6 +13,17 @@
 #include "src/formula/Prctl/AbstractPathFormula.h"
 #include "src/formula/Prctl/AbstractStateFormula.h"
 #include "src/modelchecker/prctl/AbstractModelChecker.h"
+#include "src/formula/Actions/AbstractAction.h"
+
+namespace storm {
+namespace property {
+namespace action {
+ template <typename T> class AbstractAction;
+}
+}
+}
+
+#include <algorithm>
 
 namespace storm {
 namespace property {
@@ -21,6 +32,8 @@ namespace prctl {
 template <class T>
 class PrctlFilter : public storm::property::AbstractFilter<T> {
 
+	typedef typename storm::property::action::AbstractAction<T>::Result Result;
+
 public:
 
 	PrctlFilter() : AbstractFilter<T>(UNDEFINED), child(nullptr) {
@@ -51,125 +64,26 @@ public:
 		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) {
-
-			// Check the formula and apply the filter actions.
-			storm::storage::BitVector result;
-
-			try {
-				result = evaluate(modelchecker, dynamic_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;
+		Result result;
 
-				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.template 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;
-				}
+		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));
+			} else if (dynamic_cast<AbstractRewardPathFormula<T> *>(child) != nullptr) {
+				result = evaluate(modelchecker, dynamic_cast<AbstractRewardPathFormula<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;
 		}
-		else if (dynamic_cast<AbstractPathFormula<T>*>(child) != nullptr) {
-
-			// Check the formula and apply the filter actions.
-			std::vector<T> result;
-
-			try {
-				result = evaluate(modelchecker, dynamic_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;
 
-				return;
-			}
-
-			// Now write out the result.
-
-			if(this->actions.empty()) {
+		writeOut(result, modelchecker);
 
-				// 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[initialState]);
-					std::cout << "\t" << initialState << ": " << result[initialState] << std::endl;
-				}
-			}
-
-			std::cout << std::endl << "-------------------------------------------" << std::endl;
-
-		}
-		else if (dynamic_cast<AbstractRewardPathFormula<T>*>(child) != nullptr) {
-
-			// Check the formula and apply the filter actions.
-			std::vector<T> result;
-
-			try {
-				result = evaluate(modelchecker, dynamic_cast<AbstractRewardPathFormula<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;
-			}
-
-			// 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.template getModel<storm::models::AbstractModel<T>>().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.
-		}
-	}
-
-	bool validate() const {
-		// Test whether the stored filter actions are consistent in relation to themselves and to the ingoing modelchecking result.
-
-		// Do a dynamic cast to test for the actual formula type.
-		if(dynamic_cast<AbstractStateFormula<T>*>(child) != nullptr) {
-			//TODO: Actual validation.
-		}
-		else if (dynamic_cast<AbstractPathFormula<T>*>(child) != nullptr) {
-			//TODO: Actual validation.
-		}
-		else {
-			// This branch should be unreachable. If you ended up here, something strange has happened.
-			//TODO: Error here.
-		}
-
-		return true;
 	}
 
 	virtual std::string toString() const override {
@@ -220,10 +134,10 @@ public:
 
 				for(auto action : this->actions) {
 					desc += action->toString();
-					desc += ", ";
+					desc += "; ";
 				}
 
-				// Remove the last ", ".
+				// Remove the last "; ".
 				desc.pop_back();
 				desc.pop_back();
 
@@ -242,10 +156,10 @@ public:
 
 			for(auto action : this->actions) {
 				desc += action->toString();
-				desc += ", ";
+				desc += "; ";
 			}
 
-			// Remove the last ", ".
+			// Remove the last "; ".
 			desc.pop_back();
 			desc.pop_back();
 
@@ -259,7 +173,7 @@ public:
 		return desc;
 	}
 
-	virtual std::string toPrettyString() const override{
+	virtual std::string toPrettyString() const override {
 		std::string desc = "Filter: ";
 		desc += "\nActions:";
 		for(auto action : this->actions) {
@@ -279,61 +193,122 @@ public:
 
 private:
 
-	storm::storage::BitVector evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker, AbstractStateFormula<T>* formula) const {
+	Result evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker, AbstractStateFormula<T> * formula) const {
 		// First, get the model checking result.
-		storm::storage::BitVector result;
+		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.
-			result = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false);
+			result.stateResult = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false);
 		} else {
-			result = formula->check(modelchecker);
+			result.stateResult = formula->check(modelchecker);
 		}
 
-
-		// 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::prctl::AbstractModelChecker<T> const & modelchecker, AbstractPathFormula<T>* formula) const {
+	Result evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker, AbstractPathFormula<T> * formula) const {
 		// First, get the model checking result.
-		std::vector<T> result;
+		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.
-			result = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false);
+			result.pathResult = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false);
 		} else {
-			result = formula->check(modelchecker, false);
+			result.pathResult = formula->check(modelchecker, false);
 		}
 
-		// 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::prctl::AbstractModelChecker<T> const & modelchecker, AbstractRewardPathFormula<T>* formula) const {
+	Result evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker, AbstractRewardPathFormula<T> * formula) const {
 		// First, get the model checking result.
-		std::vector<T> result;
+		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.
-			result = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false);
+			result.pathResult = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false);
 		} else {
-			result = formula->check(modelchecker, false);
+			result.pathResult = formula->check(modelchecker, false);
+		}
+
+		return evaluateActions(result, modelchecker);
+	}
+
+	Result evaluateActions(Result result, 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.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;
+	}
+
 	AbstractPrctlFormula<T>* child;
 };
 

src/parser/CslParser.cpp

@@ -11,7 +11,11 @@
 
 // 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/FormulaAction.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"
@@ -50,6 +54,10 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 				(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];
 
@@ -136,11 +144,37 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 				phoenix::new_<storm::property::csl::CslFilter<double>>(qi::_1, storm::property::UNDEFINED, true)];
 		steadyStateNoBoundOperator.name("steady state no bound operator");
 
-		rangeAction = (qi::lit("range") >> qi::lit(",") >> qi::uint_ >> qi::lit(",") >> qi::uint_)[qi::_val =
-				phoenix::new_<storm::property::action::RangeAction<double>>(qi::_1, qi::_2)];
-		rangeAction.name("range action for the formula filter");
+		// 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");
+
+		formulaAction = (qi::lit("formula") > qi::lit("(") >> stateFormula >> qi::lit(")"))[qi::_val =
+						phoenix::new_<storm::property::action::FormulaAction<double>>(qi::_1)];
+		formulaAction.name("formula 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 = (rangeAction) >> (qi::eps | qi::lit(","));
+		abstractAction = (rangeAction) >> (qi::eps | qi::lit(";"));
 		abstractAction.name("filter action");
 
 		filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
@@ -165,7 +199,11 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 	qi::rule<Iterator, storm::property::csl::CslFilter<double>*(), Skipper> steadyStateNoBoundOperator;
 
 	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::FormulaAction<double>*(), Skipper> formulaAction;
 	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::csl::AbstractCslFormula<double>*(), Skipper> formula;
 	qi::rule<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper> comment;
@@ -191,6 +229,7 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFi
 
 	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;
 
 };
 

src/parser/PrctlParser.cpp

@@ -4,7 +4,11 @@
 
 // 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/FormulaAction.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"
@@ -38,17 +42,21 @@ namespace parser {
 template<typename Iterator, typename Skipper>
 struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl::PrctlFilter<double>*(), Skipper > {
 	PrctlGrammar() : PrctlGrammar::base_type(start) {
-		//This block contains helper rules that may be used several times
+		// 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]);
-		//Comment: Empty line or line starting with "//"
+		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];
 
-		//This block defines rules for parsing state formulas
+		// This block defines rules for parsing state formulas
 		stateFormula %= orFormula;
 		stateFormula.name("state formula");
 		orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
@@ -61,8 +69,8 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 				phoenix::new_<storm::property::prctl::Not<double>>(qi::_1)];
 		notFormula.name("not formula");
 
-		//This block defines rules for "atomic" state formulas
-		//(Propositions, probabilistic/reward formulas, and state formulas in brackets)
+		// This block defines rules for "atomic" state formulas
+		// (Propositions, probabilistic/reward formulas, and state formulas in brackets)
 		atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")") | qi::lit("[") >> stateFormula >> qi::lit("]");
 		atomicStateFormula.name("atomic state formula");
 		atomicProposition = (freeIdentifierName)[qi::_val =
@@ -76,7 +84,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 				phoenix::new_<storm::property::prctl::RewardBoundOperator<double> >(qi::_1, qi::_2, qi::_3)]);
 		rewardBoundOperator.name("reward bound operator");
 
-		//This block defines rules for parsing probabilistic path formulas
+		// This block defines rules for parsing probabilistic path formulas
 		pathFormula = (boundedEventually | eventually | next | globally | boundedUntil | until | qi::lit("(") >> pathFormula >> qi::lit(")") | qi::lit("[") >> pathFormula >> qi::lit("]"));
 		pathFormula.name("path formula");
 		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
@@ -98,7 +106,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 				phoenix::new_<storm::property::prctl::Until<double>>(phoenix::bind(&storm::property::prctl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::property::prctl::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
 		until.name("path formula (for probabilistic operator)");
 
-		//This block defines rules for parsing reward path formulas
+		// This block defines rules for parsing reward path formulas.
 		rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward | qi::lit("(") >> rewardPathFormula >> qi::lit(")") | qi::lit("[") >> rewardPathFormula >> qi::lit("]"));
 		rewardPathFormula.name("path formula (for reward operator)");
 		cumulativeReward = (qi::lit("C") > qi::lit("<=") > qi::double_)[qi::_val =
@@ -115,9 +123,9 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		formula = (pathFormula | stateFormula);
 		formula.name("PRCTL formula");
 
-		//This block defines rules for parsing formulas with noBoundOperators
-		//Note that this is purely for legacy support.
-		//NoBoundOperators are no longer part of the formula tree and are therefore deprecated.
+		// This block defines rules for parsing formulas with noBoundOperators.
+		// Note that this is purely for legacy support.
+		// NoBoundOperators are no longer part of the formula tree and are therefore deprecated.
 		noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator);
 		noBoundOperator.name("no bound operator");
 		probabilisticNoBoundOperator = (
@@ -141,15 +149,46 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 				);
 		rewardNoBoundOperator.name("no bound operator");
 
-		rangeAction = (qi::lit("range") >> qi::lit(",") >> qi::uint_ >> qi::lit(",") >> qi::uint_)[qi::_val =
-				phoenix::new_<storm::property::action::RangeAction<double>>(qi::_1, qi::_2)];
-		rangeAction.name("range action for the formula filter");
 
-		abstractAction = (rangeAction) >> (qi::eps | qi::lit(","));
+		// 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");
+
+		formulaAction = (qi::lit("formula") > qi::lit("(") >> stateFormula >> qi::lit(")"))[qi::_val =
+						phoenix::new_<storm::property::action::FormulaAction<double>>(qi::_1)];
+		formulaAction.name("formula 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 = (rangeAction) >> (qi::eps | qi::lit(";"));
 		abstractAction.name("filter action");
 
-		filter = (qi::lit("filter") > qi::lit("[") >> +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
+		filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
 					phoenix::new_<storm::property::prctl::PrctlFilter<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::prctl::PrctlFilter<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::prctl::PrctlFilter<double>>(qi::_2, qi::_1, storm::property::MINIMIZE)] |
 				 (noBoundOperator)[qi::_val =
 					qi::_1] |
 				 (formula)[qi::_val =
@@ -169,7 +208,11 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 	qi::rule<Iterator, storm::property::prctl::PrctlFilter<double>*(), Skipper> rewardNoBoundOperator;
 
 	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::FormulaAction<double>*(), Skipper> formulaAction;
 	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::prctl::AbstractPrctlFormula<double>*(), Skipper> formula;
 	qi::rule<Iterator, storm::property::prctl::AbstractPrctlFormula<double>*(), Skipper> comment;
@@ -201,6 +244,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 
 	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;
 
 };