+*/
+
+
+/**
+ This operation is specifically for Method set. For example, when we want to
+ construct an integer set from the local state field "x" (which is an
+ integer) of the previous set of method calls (PREV), and the new set goes to
+ "readSet", we would call "MakeSet(int, PREV, readSet, LOCAL(x));". Then users
+ can use the "readSet" as an integer set (set<int>)
+*/
+#define MakeSet(type, oldset, newset, field) \
+ auto newset = new set<type>; \
+ ForEach (_M, oldset) \
+ newset->insert(field); \
+
+/**
+ We provide a more general subset operation that takes a plain boolean
+ expression on each item (access by the name "ITEM") of the set, and put it
+ into a new set if the boolean expression (Guard) on that item holds. This is
+ used as the second arguments of the Subset operation. An example to extract
+ a subset of positive elements on an IntSet "s" would be "Subset(s,
+ GeneralGuard(int, ITEM > 0))"
+*/
+#define GeneralGuard(type, expression) std::function<bool(type)> ( \
+ [](type ITEM) -> bool { return (expression);}) \
+
+/**
+ This is a more specific guard designed for the Method (MethodCall*). It
+ basically wrap around the GeneralGuard with the type Method. An example to
+ extract the subset of method calls in the PREV set whose local state "x" is
+ equal to "val" would be "Subset(PREV, Guard(Local(x) == val))"
+*/
+#define Guard(expression) GeneralGuard(Method, expression)
+
+/**
+ A general subset operation that takes a condition and returns all the item
+ for which the boolean guard holds.
+*/
+template <class T>
+inline set<T>* Subset(set<T> *original, std::function<bool(T)> condition) {
+ set<T> *res = new set<T>;
+ ForEach (_M, original) {
+ if (condition(_M))
+ res->insert(_M);
+ }
+ return res;
+}
+
+/**
+ A general sublist operation that takes a condition and returns all the item
+ for which the boolean guard holds in the same order as in the old list.
+*/
+template <class T>
+inline list<T>* Sublist(list<T> *original, std::function<bool(T)> condition) {
+ list<T> *res = new list<T>;
+ ForEach (_M, original) {
+ if (condition(_M))
+ res->push_back(_M);
+ }
+ return res;
+}
+
+/**
+ A general subvector operation that takes a condition and returns all the item
+ for which the boolean guard holds in the same order as in the old vector.
+*/
+template <class T>
+inline vector<T>* Subvector(vector<T> *original, std::function<bool(T)> condition) {
+ vector<T> *res = new vector<T>;
+ ForEach (_M, original) {
+ if (condition(_M))
+ res->push_back(_M);
+ }
+ return res;
+}