using namespace std;
-typedef struct MethodCall {
+struct MethodCall;
+
+typedef MethodCall *Method;
+typedef set<Method> *MethodSet;
+
+struct MethodCall {
string interfaceName; // The interface label name
void *value; // The pointer that points to the struct that have the return
// value and the arguments
void *state; // The pointer that points to the struct that represents
// the state
- set<MethodCall*> *prev; // Method calls that are hb right before me
- set<MethodCall*> *next; // Method calls that are hb right after me
- set<MethodCall*> *concurrent; // Method calls that are concurrent with me
-} MethodCall;
+ MethodSet prev; // Method calls that are hb right before me
+ MethodSet next; // Method calls that are hb right after me
+ MethodSet concurrent; // Method calls that are concurrent with me
+
+ MethodCall(string name) : MethodCall() { interfaceName = name; }
+
+ MethodCall() : interfaceName(""), prev(new set<Method>),
+ next(new set<Method>), concurrent(new set<Method>) { }
+
+ void addPrev(Method m) { prev->insert(m); }
+
+ void addNext(Method m) { next->insert(m); }
+
+ void addConcurrent(Method m) { concurrent->insert(m); }
+
+};
-typedef MethodCall *Method;
-typedef set<Method> *MethodSet;
typedef vector<int> IntVector;
typedef list<int> IntList;
typedef set<int> IntSet;
+typedef vector<double> DoubleVector;
+typedef list<double> DoubleList;
+typedef set<double> DoubleSet;
+
/********** More general specification-related types and operations **********/
-#define NewSet new set<Method>
+#define NewMethodSet new set<Method>
#define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
#define CAT_HELPER(a, b) a ## b
/*
#define Subset(s, subset, condition) \
MethodSet original = s; \
- MethodSet subset = NewSet; \
+ MethodSet subset = NewMethodSet; \
ForEach (_M, original) { \
if ((condition)) \
subset->insert(_M); \
/**
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,
+ 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);}) \
+ [&](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 state "x" is
- equal to "val" would be "Subset(PREV, Guard(STATE(x) == val))"
+ extract the subset of method calls in the PREV set whose state "x" is equal
+ to "val" would be "Subset(PREV, Guard(STATE(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>;
+inline MethodSet Subset(MethodSet original, std::function<bool(Method)> condition) {
+ MethodSet res = new SnapSet<Method>;
ForEach (_M, original) {
if (condition(_M))
res->insert(_M);
return res;
}
+/**
+ A general set operation that takes a condition and returns if there exists
+ any item for which the boolean guard holds.
+*/
+template <class T>
+inline bool HasItem(set<T> *original, std::function<bool(T)> condition) {
+ ForEach (_M, original) {
+ if (condition(_M))
+ return true;
+ }
+ return false;
+}
+
+
+
/**
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.
MethodSet res;
va_start (ap, count);
- res = NewSet;
+ res = NewMethodSet;
for (int i = 0; i < count; i++) {
Method item = va_arg (ap, Method);
res->insert(item);
is2->insert(5);
- MethodSet ms = NewSet;
+ MethodSet ms = NewMethodSet;
Method m = new MethodCall;
m->interfaceName = "Store";
StateStruct *ss = new StateStruct;
m->value = ld;
ms->insert(m);
- MakeSet(int, ms, newis, STATE(x));
- cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
- ForEach (i, newis) {
- cout << "elem: " << i << endl;
- }
+ //MakeSet(int, ms, newis, STATE(x));
+ //cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
+
+ int x = 2;
+ int y = 2;
+ cout << "HasItem=" << HasItem(ms, Guard(STATE(x) == x && y == 0)) << endl;
+
+ //ForEach (i, newis) {
+ //cout << "elem: " << i << endl;
+ //}
//Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);