diff --git a/src/formula/AbstractFilter.h b/src/formula/AbstractFilter.h
index fe9798fca..ba95d5524 100644
--- a/src/formula/AbstractFilter.h
+++ b/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"
diff --git a/src/formula/Actions/AbstractAction.h b/src/formula/Actions/AbstractAction.h
index c58ad6be0..77d2089ea 100644
--- a/src/formula/Actions/AbstractAction.h
+++ b/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
diff --git a/src/formula/Actions/BoundAction.h b/src/formula/Actions/BoundAction.h
new file mode 100644
index 000000000..4b7f77cc0
--- /dev/null
+++ b/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_ */
diff --git a/src/formula/Actions/InvertAction.h b/src/formula/Actions/InvertAction.h
new file mode 100644
index 000000000..90192020c
--- /dev/null
+++ b/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_ */
diff --git a/src/formula/Actions/RangeAction.h b/src/formula/Actions/RangeAction.h
index 3952419ae..ce8b0e2ae 100644
--- a/src/formula/Actions/RangeAction.h
+++ b/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;
diff --git a/src/formula/Actions/SortAction.h b/src/formula/Actions/SortAction.h
new file mode 100644
index 000000000..5a4c1c622
--- /dev/null
+++ b/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_ */
diff --git a/src/formula/Csl/CslFilter.h b/src/formula/Csl/CslFilter.h
index 14c578be7..ae5c256d9 100644
--- a/src/formula/Csl/CslFilter.h
+++ b/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 = "";
diff --git a/src/formula/Prctl/PrctlFilter.h b/src/formula/Prctl/PrctlFilter.h
index 407b4f6c3..77a8c35f7 100644
--- a/src/formula/Prctl/PrctlFilter.h
+++ b/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;
};
diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp
index 296deecc0..9e38a9c59 100644
--- a/src/parser/CslParser.cpp
+++ b/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;
};
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 49bfe281b..0fb8b538a 100644
--- a/src/parser/PrctlParser.cpp
+++ b/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;
};