diff --git a/src/formula/AbstractFilter.h b/src/formula/AbstractFilter.h new file mode 100644 index 000000000..6e73913c8 --- /dev/null +++ b/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 +#include "src/formula/AbstractFormula.h" +#include "src/formula/Actions/Action.h" + +namespace storm { +namespace property { + +template +class AbstractFilter { + +public: + + AbstractFilter() { + // Intentionally left empty. + } + + AbstractFilter(action::Action* action) { + actions.push_back(action); + } + + AbstractFilter(std::vector*> 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* action) { + actions.push_back(action); + } + + void removeAction() { + actions.pop_back(); + } + + action::Action* getAction(uint_fast64_t pos) const { + return actions[pos]; + } + + uint_fast64_t getActionCount() const { + return actions.size(); + } + +protected: + + std::vector*> actions; +}; + +} //namespace property +} //namespace storm + + + +#endif /* STORM_FORMULA_ABSTRACTFILTER_H_ */ diff --git a/src/formula/Actions/Action.h b/src/formula/Actions/Action.h new file mode 100644 index 000000000..f435859b9 --- /dev/null +++ b/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 +#include "src/storage/BitVector.h" + +namespace storm { +namespace property { +namespace action { + +template +class Action { + +public: + + /*! + * Virtual destructor + * To ensure that the right destructor is called + */ + virtual ~Action() { + //Intentionally left empty + } + + /*! + * + */ + virtual std::vector evaluate(std::vector input) const = 0; + + /*! + * + */ + virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const = 0; + + /*! + * + */ + virtual std::string toString() const = 0; +}; + +} //namespace action +} //namespace property +} //namespace storm + + +#endif /* STORM_FORMULA_ACTION_ACTION_H_ */ diff --git a/src/formula/Actions/RangeAction.h b/src/formula/Actions/RangeAction.h new file mode 100644 index 000000000..183ad6a13 --- /dev/null +++ b/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 RangeAction : Action { + +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 evaluate(std::vector 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 out(input.begin() + from, input.begin() + to); + return out; + } + + /*! + * + */ + virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const override { + storm::storage::BitVector 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_ */ diff --git a/src/formula/Prctl/PrctlFilter.h b/src/formula/Prctl/PrctlFilter.h new file mode 100644 index 000000000..5cf154e6f --- /dev/null +++ b/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 PrctlFilter : storm::property::AbstractFilter { + +public: + + PrctlFilter() : child(nullptr) { + // Intentionally left empty. + } + + PrctlFilter(AbstractFormula* child) : child(child) { + // Intentionally left empty. + } + + PrctlFilter(AbstractFormula* child, action::Action* action) : child(child) { + actions.push_back(action); + } + + PrctlFilter(AbstractFormula* child, std::vector*> 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*>(child) != nullptr) { + // Check the formula and apply the filter actions. + storm::storage::BitVector result = evaluate(modelchecker, static_cast*>(child)); + + // Now write out the result. + + } + else if (dynamic_cast*>(child) != nullptr) { + // Check the formula and apply the filter actions. + std::vector result = evaluate(modelchecker, static_cast*>(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*>(child) != nullptr) { + //TODO: Actual validation. + } + else if (dynamic_cast*>(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 evaluate(AbstractModelChecker& modelchecker, AbstractStateFormula* 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 evaluate(AbstractModelChecker& modelchecker, AbstractPathFormula* formula) const { + // First, get the model checking result. + std::vector 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_ */