edits

[cdsspec-compiler.git] / notes / nondeterm-spec.txt

diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
index 7eee23d17497ee52919ecd8703f837f7da910778..f86c661393a7b19a1b6df06c6cfb2afc204f4e6d 100644 (file)
--- a/notes/nondeterm-spec.txt
+++ b/notes/nondeterm-spec.txt
@@ -241,6 +241,55 @@ inline vector<MethodCall*>* Subset(vector<MethodCall*> *set, string name) {
        }
        return _subset;
 }
+
+// 1.2 Size(set) --> to get the size of a method set
+#define Size(set) set->size()
+
+// 1.3 Belong(set, method) --> whether method belongs to set
+#define Belong(set, method) std::find(set->begin(), set->end(), method) != set->end()
+
+// 1.4 Intersect(set1, set2) --> the intersection of two method sets
+inline MethodSet Intersect(MethodSet set1, MethodSet set2) {
+       MethodSet res = NewSet;
+       ForEach (m, set1) {
+               if (Belong(set2, m))
+                       res->push_back(m);
+       }
+       return res;
+}
+
+// 1.5 Union(set1, set2) --> the union of two method sets
+inline MethodSet Union(MethodSet set1, MethodSet set2) {
+       MethodSet res = NewSet(set1);
+       ForEach (m, set2) {
+               if (!Belong(set1, m))
+                       res->push_back(m);
+       }
+       return res;
+}
+
+// 1.6 Insert(set, method) --> add a method to the set
+inline bool Insert(MethodSet set, Method m) {
+       if (Belong(set, m))
+               return false;
+       else {
+               set->push_back(m);
+               return true;
+       }
+}
+
+// 1.7 Subtract(set1, set2) --> subtract set2 from set1 
+inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
+       MethodSet res = NewSet;
+       ForEach (m, set1) {
+               if (!Belong(set2, m))
+                       res->push_back(m);
+       }
+       return res;
+}
+
+// 1.8 MakeSet(count, ...) --> Make a set from the arguments
+
        
 // 2. Local(method, field)
 #define Local(method, field) ((StateStruct*) method->localState)->field
@@ -264,16 +313,13 @@ inline vector<MethodCall*>* Subset(vector<MethodCall*> *set, string name) {
 @PreCondition:
        // Auto generated code
        // MethodCall *ME = ((SomeTypeConversion) info)->method;
-       // vector<MethodCall*> PREV = Me->prev;
-       // vector<MethodCall*> NEXT = Me->next;
-       // vector<MethodCall*> CONCURRENT = Me->concurrent;
 
        IntegerSet prevSet, concurSet;
        ForEach(m, PREV) {
-               prevSet.add(LOCAL(m, x));
+               prevSet->insert(LOCAL(m, x));
        }
-       ForEach (m, CONCURRENT("STORE")) {
-               concurSet->add(m.val);
+       ForEach (m, Subset(CONCURRENT, "STORE")) {
+               concurSet->insert(Value(m, STORE, val));
        }
        return prevSet->contains(RET) || concurSet->contains(RET);
 @SideEffect:
@@ -317,17 +363,15 @@ void enq(queue_t *q, int val);
        // dequeue them
        if (!RET) {
                // Local state is empty
-               if (Local.q->size() == 0)
-                       return true;
+               if (Local.q->size() == 0) return true;
                // Otherwise check there must be other concurrent dequeuers
                for (int i = 0; i < Local.q->size(); i++) {
                        int item = (*Local.q)[i];
                        // Check there's some concurrent dequeuer for this item
                        bool flag = false;
-                       for (m in CONCURRENT("Deq")) {
-                               if (m.RET) {
-                                       if (*m.res == item) flag = true;
-                               }
+                       ForEach (m, Subset(CONCURRENT, "Deq")) {
+                               if (Value(m, Deq, RET) && *Value(m, Deq, res) == item)
+                                       flag = true;
                        }
                        if (!flag) return false;
                }