Started on the filters.

- Got the general structure down.
- Now writing the output functions.

Next up: Finish the basic filter functionality.


Former-commit-id: 91daa0a9f7

src/formula/AbstractFilter.h

@@ -0,0 +1,79 @@
+/*
+ * Filter.h
+ *
+ *  Created on: Apr 26, 2014
+ *      Author: Manuel Sascha Weiand
+ */
+
+#ifndef STORM_FORMULA_ABSTRACTFILTER_H_
+#define STORM_FORMULA_ABSTRACTFILTER_H_
+
+#include <vector>
+#include "src/formula/AbstractFormula.h"
+#include "src/formula/Actions/Action.h"
+
+namespace storm {
+namespace property {
+
+template <class T>
+class AbstractFilter {
+
+public:
+
+	AbstractFilter() {
+		// Intentionally left empty.
+	}
+
+	AbstractFilter(action::Action<T>* action) {
+		actions.push_back(action);
+	}
+
+	AbstractFilter(std::vector<action::Action<T>*> actions) : actions(actions) {
+		// Intentionally left empty.
+	}
+
+	virtual ~AbstractFilter() {
+		actions.clear();
+	}
+
+	std::string toFormulaString() const {
+		std::string desc = "filter(";
+		return desc;
+	}
+
+	std::string toString() const {
+		std::string desc = "Filter: ";
+		desc += "\nActions:";
+		for(auto action : actions) {
+			desc += "\n\t" + action.toString();
+		}
+		return desc;
+	}
+
+	void addAction(action::Action<T>* action) {
+		actions.push_back(action);
+	}
+
+	void removeAction() {
+		actions.pop_back();
+	}
+
+	action::Action<T>* getAction(uint_fast64_t pos) const {
+		return actions[pos];
+	}
+
+	uint_fast64_t getActionCount() const {
+		return actions.size();
+	}
+
+protected:
+
+	std::vector<action::Action<T>*> actions;
+};
+
+} //namespace property
+} //namespace storm
+
+
+
+#endif /* STORM_FORMULA_ABSTRACTFILTER_H_ */

src/formula/Actions/Action.h

@@ -0,0 +1,52 @@
+/*
+ * Action.h
+ *
+ *  Created on: Apr 26, 2014
+ *      Author: Manuel Sascha Weiand
+ */
+
+#ifndef STORM_FORMULA_ACTION_ACTION_H_
+#define STORM_FORMULA_ACTION_ACTION_H_
+
+#include <vector>
+#include "src/storage/BitVector.h"
+
+namespace storm {
+namespace property {
+namespace action {
+
+template <class T>
+class Action {
+
+public:
+
+	/*!
+	 * Virtual destructor
+	 * To ensure that the right destructor is called
+	 */
+	virtual ~Action() {
+		//Intentionally left empty
+	}
+
+	/*!
+	 *
+	 */
+	virtual std::vector<T> evaluate(std::vector<T> input) const = 0;
+
+	/*!
+	 *
+	 */
+	virtual storm::storage::BitVector<T> evaluate(storm::storage::BitVector<T> input) const = 0;
+
+	/*!
+	 *
+	 */
+	virtual std::string toString() const = 0;
+};
+
+} //namespace action
+} //namespace property
+} //namespace storm
+
+
+#endif /* STORM_FORMULA_ACTION_ACTION_H_ */

src/formula/Actions/RangeAction.h

@@ -0,0 +1,74 @@
+/*
+ * RangeAction.h
+ *
+ *  Created on: Apr 26, 2014
+ *      Author: Manuel Sascha Weiand
+ */
+
+#ifndef STORM_FORMULA_ACTION_RANGEACTION_H_
+#define STORM_FORMULA_ACTION_RANGEACTION_H_
+
+#include "src/formula/Actions/Action.h"
+
+namespace storm {
+namespace property {
+namespace action {
+
+template <class T>
+class RangeAction : Action<T> {
+
+public:
+
+	RangeAction() : from(0), to(0) {
+		//Intentionally left empty.
+	}
+
+	RangeAction(uint_fast64_t from, uint_fast64_t to) : from(from), to(to) {
+		//Intentionally left empty.
+	}
+
+	/*!
+	 * Virtual destructor
+	 * To ensure that the right destructor is called
+	 */
+	virtual ~RangeAction() {
+		//Intentionally left empty
+	}
+
+	/*!
+	 *
+	 */
+	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 storm::storage::BitVector<T> evaluate(storm::storage::BitVector<T> input) const override {
+		storm::storage::BitVector<T> out(to - from  + 1, input.begin() + from, input.begin() + to);
+		return out;
+	}
+
+	/*!
+	 *
+	 */
+	virtual std::string toString() const override {
+		return "range, " + from + ", " + to;
+	}
+
+private:
+	uint_fast64_t from;
+	uint_fast64_t to;
+
+};
+
+} //namespace action
+} //namespace property
+} //namespace storm
+
+#endif /* STORM_FORMULA_ACTION_RANGEACTION_H_ */

src/formula/Prctl/PrctlFilter.h

@@ -0,0 +1,142 @@
+/*
+ * PrctlFilter.h
+ *
+ *  Created on: Apr 26, 2014
+ *      Author: Manuel Sascha Weiand
+ */
+
+#ifndef STORM_FORMULA_PRCTL_PRCTLFILTER_H_
+#define STORM_FORMULA_PRCTL_PRCTLFILTER_H_
+
+#include "src/formula/AbstractFilter.h"
+#include "src/formula/Prctl/AbstractPrctlFormula.h"
+#include "src/formula/Prctl/AbstractPathFormula.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
+
+namespace storm {
+namespace property {
+namespace prctl {
+
+template <class T>
+class PrctlFilter : storm::property::AbstractFilter<T> {
+
+public:
+
+	PrctlFilter() : child(nullptr) {
+		// Intentionally left empty.
+	}
+
+	PrctlFilter(AbstractFormula* child) : child(child) {
+		// Intentionally left empty.
+	}
+
+	PrctlFilter(AbstractFormula* child, action::Action<T>* action) : child(child) {
+		actions.push_back(action);
+	}
+
+	PrctlFilter(AbstractFormula* child, std::vector<action::Action<T>*> actions) : child(child), actions(actions) {
+		// Intentionally left empty.
+	}
+
+	virtual ~PrctlFilter() {
+		actions.clear();
+		delete child;
+	}
+
+	void check(AbstractModelChecker& modelchecker) const {
+
+		// 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 = evaluate(modelchecker, static_cast<AbstractStateFormula<T>*>(child));
+
+			// Now write out the result.
+
+		}
+		else if (dynamic_cast<AbstractPathFormula<T>*>(child) != nullptr) {
+			// Check the formula and apply the filter actions.
+			std::vector<T> result = evaluate(modelchecker, static_cast<AbstractPathFormula<T>*>(child));
+
+			// Now write out the result.
+		}
+		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;
+	}
+
+	std::string toFormulaString() const {
+		std::string desc = "filter(";
+		return desc;
+	}
+
+	std::string toString() const {
+		std::string desc = "Filter: ";
+		desc += "\nActions:";
+		for(auto action : actions) {
+			desc += "\n\t" + action.toString();
+		}
+		desc += "\nFormula:\n\t" + child->toString();
+		return desc;
+	}
+
+	void setChild(AbstractFormula* child) {
+		this->child = child;
+	}
+
+	AbstractFormula* getChild() const {
+		return child;
+	}
+
+private:
+
+	BitVector<T> evaluate(AbstractModelChecker& modelchecker, AbstractStateFormula<T>* formula) const {
+		// First, get the model checking result.
+		BitVector result = formula->check(modelchecker);
+
+		// Now apply all filter actions and return the result.
+		for(auto action : actions) {
+			result = action->evaluate(result);
+		}
+		return result;
+	}
+
+	std::vector<T> evaluate(AbstractModelChecker& modelchecker, AbstractPathFormula<T>* formula) const {
+		// First, get the model checking result.
+		std::vector<T> result = formula->check(modelchecker);
+
+		// Now apply all filter actions and return the result.
+		for(auto action : actions) {
+			result = action->evaluate(result);
+		}
+		return result;
+	}
+
+	AbstractPrctlFormula* child;
+};
+
+} //namespace prctl
+} //namespace property
+} //namespace storm
+
+
+
+#endif /* STORM_FORMULA_PRCTL_PRCTLFILTER_H_ */